antom

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.

Contact:

Dr. Tobias Schubert
Institute of Computer Science
Faculty of Engineering
Albert-Ludwigs-University Freiburg
Georges-Koehler-Allee 51
D-79110 Freiburg im Breisgau
Germany
Phone: +49 (0)761 203-8153
Fax: +49 (0)761 203-8142
E-mail: schubert@informatik.uni-freiburg.de
URL: http://ira.informatik.uni-freiburg.de/~schubert/