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 to formally reason about them in a simple way. Its properties, s...

Full description

Saved in:
Bibliographic Details
Published in:Journal of the ACM 2006-11, Vol.53 (6), p.937-977
Main Authors: NIEUWENHUIS, Robert, OLIVERAS, Albert, TINELLI, Cesare
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Algorithms
Applied sciences
Cleaning
Computer programming
Computer science
control theory
systems
Cooperation
Design engineering
Exact sciences and technology
Mathematical models
Modular
Propagation
Solvers
State of the art
Strategy
Studies
Theoretical computing
Theory
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0004-5411
1557-735X
DOI:10.1145/1217856.1217859