Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL

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 readily usable ground for high-quality implementations of comprehensive SMT solvers.

• Type: Conference
• Year: 2007
• Where: FROCOS
• Authors: Sava Krstic, Amit Goel
• Keywords: Comprehensive Smt Solvers, FROCOS 2007, Multiple Disjoint Theories, SMT Solvers