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.