antom is a C++ library for solving
  • SAT,
  • Unweighted MaxSAT,
  • Partial MaxSAT, and
  • #SAT problems.
It incorporates many features of modern SAT/MaxSAT/#SAT solving:
  • Various activity-based decision heuristics,
  • Fast unit propagation via watched literals,
  • Conflict-driven learning,
  • Non-chronological backtracking,
  • Restarts (luby, glucose-like),
  • Lazy hyper binary resolution,
  • Conflict clause deletion (literals blocks distance),
  • Phase saving,
  • Special data structures to handle binary clauses more efficiently,
  • Incremental SAT solving interface,
  • Powerful solver state management (hard vs. soft reset),
  • Formula caching & component analysis (#SAT),
  • Various strategies for MaxSAT (e.g., satisfiability-based, unsatisfiability-based, ...), and
  • Well-documented source code.
Furthermore, antom can be executed as a parallel SAT/MaxSAT/#SAT solver, supporting two different modes of parallelism:
  • Algorithm portfolio and
  • Divide-and-conquer based on dynamic work stealing.

Both parallel modes of operation have been carried out using OpenMP and provide a deterministic behavior.

antom has served as the backend solver in several projects:
  • M. Sauer, A. Czutro, T. Schubert, S. Hillebrecht, I. Polian, B. Becker. SAT-based Analysis of Sensitisable Paths. IEEE Design & Test of Computers, 2013.
  • M. Sauer, S. Reimer, T. Schubert, I. Polian, B. Becker. Efficient SAT-Based Dynamic Compaction and Relaxation for Longest Sensitizable Paths. DATE, 2103.
  • M. Sauer, S. Reimer, I. Polian, T. Schubert, B. Becker. Provably Optimal Test Cube Generation Using Quantified Boolean Formula Solving. ASP-DAC, 2013.
  • S. Hillebrecht, M. Kochte, H.-J. Wunderlich, B. Becker. Exact Stuck-at Fault Classification in Presence of Unknowns. ETS, 2012.
  • A. Czutro, M. Imhof, J. Jang, A. Mumtaz, M. Sauer, B. Becker, I. Polian, H.-J. Wunderlich. Variation-Aware Fault Grading. ATS, 2012.
  • M. Sauer, A. Czutro, I. Polian, B. Becker. Small-Delay-Fault ATPG with Waveform Accuracy. ICCAD, 2012.
  • M. Sauer, A. Czutro, B. Becker, I. Polian. On the Quality of Test Vectors for Post-Silicon Characterization. ETS, 2012.
  • A. Czutro, M. Sauer, I. Polian, B. Becker. Multi-Conditional SAT-ATPG for Power-Droop Testing. ETS, 2012.
  • L. Feiten, M. Sauer, T. Schubert, A. Czutro, E. Boehl, I. Polian, B. Becker. #SAT-Based Vulnerability Analysis of Security Components -- A Case Study. DFT, 2012.
  • A. Czutro, M. Sauer, T. Schubert, I. Polian, B. Becker. SAT-ATPG Using Preferences for Improved Detection of Complex Defect Mechanisms. VLSI Test Symp., 2012.
  • J. Jang, M. Sauer, A. Czutro, B. Becker, I. Polian. On the Optimality of K Longest Path Generation Algorithm Under Memory Constraints. DATE, 2011.


Dr. Tobias Schubert
Institute of Computer Science
Faculty of Engineering
Albert-Ludwigs-University Freiburg
Georges-Koehler-Allee 51
D-79110 Freiburg im Breisgau
Phone: +49 (0)761 203-8153
Fax: +49 (0)761 203-8142