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

Access Restriction
Subscribed

 Author Nieuwenhuis, Robert ♦ Oliveras, Albert ♦ Tinelli, Cesare Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2006 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Subject Keyword SAT solvers ♦ Satisfiability Modulo Theories Abstract 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 to formally reason about them in a simple way. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as backjumping or clause learning.We then extend the framework to Satisfiability Modulo background Theories (SMT) and use it to model several variants of the so-called lazy approach for SMT. In particular, we use it to introduce a few variants of a new, efficient and modular approach for SMT based on a general $DPLL(\textit{X})$ engine, whose parameter $\textit{X}$ can be instantiated with a specialized solver $Solver_{T}$ for a given theory $\textit{T},$ thus producing a $DPLL(\textit{T})$ system. We describe the high-level design of $DPLL(\textit{X})$ and its cooperation with $Solver_{T},$ discuss the role of theory propagation, and describe different $DPLL(\textit{T})$ strategies for some theories arising in industrial applications.Our extensive experimental evidence, summarized in this article, shows that $DPLL(\textit{T})$ systems can significantly outperform the other state-of-the-art tools, frequently even in orders of magnitude, and have better scaling properties. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2006-11-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 53 Issue Number 6 Page Count 41 Starting Page 937 Ending Page 977

#### Open content in new tab

Source: ACM Digital Library