Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. (English) Zbl 1148.68466

Krstić, Sava; Goel, Amit

Konev, Boris (ed.) et al., Frontiers of combining systems. 6th international symposium, FroCoS 2007, Liverpool, UK, September 10–12, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74620-1/pbk). Lecture Notes in Computer Science 4720. Lecture Notes in Artificial Intelligence, 1-27 (2007).

Summary: We offer a transition system representing a high-level but detailed architecture for SMT solvers that combine a propositional SAT engine with solvers for multiple disjoint theories. The system captures succintly and accurately all the major aspects of the solver’s global operation: Boolean search with across-the-board backjumping, communication of theory-specific facts and equalities between shared variables, and cooperative conflict analysis. Provably correct and prudently underspecified, our system is a usable ground for high-quality implementations of comprehensive SMT solvers.
For the entire collection see [Zbl 1143.68008].

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20	Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

Chaff; MiniSat; Yices