Thumbnail
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

   Open content in new tab
Source: ACM Digital Library