Solving SAT and SAT Modulo Theories
Top Cited Papers
- 1 November 2006
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 53 (6), 937-977
- https://doi.org/10.1145/1217856.1217859
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( X ) engine, whose parameter X can be instantiated with a specialized solver Solver T for a given theory T , thus producing a DPLL( T ) system. We describe the high-level design of DPLL( X ) and its cooperation with Solver T , discuss the role of theory propagation , and describe different DPLL( T ) strategies for some theories arising in industrial applications.Our extensive experimental evidence, summarized in this article, shows that DPLL( T ) systems can significantly outperform the other state-of-the-art tools, frequently even in orders of magnitude, and have better scaling properties.Keywords
This publication has 19 references indexed in Scilit:
- Proof-Producing Congruence ClosureLecture Notes in Computer Science, 2005
- An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic LogicLecture Notes in Computer Science, 2005
- Range Allocation for Separation LogicLecture Notes in Computer Science, 2004
- Boolean satisfiability with transitivity constraintsACM Transactions on Computational Logic, 2002
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logicACM Transactions on Computational Logic, 2001
- On the Relative Complexity of Resolution Refinements and Cutting Planes Proof SystemsSIAM Journal on Computing, 2000
- GRASP: a search algorithm for propositional satisfiabilityIEEE Transactions on Computers, 1999
- Constraint logic programming: a surveyThe Journal of Logic Programming, 1994
- Variations on the Common Subexpression ProblemJournal of the ACM, 1980
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960