Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

antom

| Beteiligte Mitarbeiter | Projektbeschreibung |


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Sven Reimer, Dipl. Inf. Entwickler
Tobias Schubert, Dr. Entwickler / Kontakt


Projektbeschreibung

Overview



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.