Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

摘要: We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and formally reason about them in simple way. Its properties, such as soundness, completeness or termination, immediately carry over modern implementations with features backjumping clause learning.We then extend Satisfiability Modulo background Theories (SMT) use it model several variants so-called lazy approach SMT. In particular, we few new, efficient modular SMT based on general DPLL(X) engine, whose parameter X can be instantiated specialized solver SolverT given theory T, thus producing DPLL(T) system. describe high-level design its cooperation SolverT, discuss role propagation, different strategies some theories arising industrial applications.Our extensive experimental evidence, summarized this article, shows that systems significantly outperform other state-of-the-art tools, frequently even orders magnitude, have better scaling properties.