DPLL: The Core of Modern Satisfiability Solvers
Donald Loveland, Ashish Sabharwal and Bart Selman
Abstract Propositional theorem provers have become a core technology in a range of areas, such as in hardware and software verification, AI planning, and mathematical discovery. The theorem provers rely on fast Boolean satisfiabilty (SAT) solving procedures, whose roots can be traced back to the work by Martin Davis and colleagues in the late 1950s. We review the history of this work with recent advances and applications.
Keywords Boolean satisfiability • SAT solvers • Davis-Putnamprocedure • DPLL • Theorem proving
For practical reasons there is considerable interest in Boolean satisfiability (SAT) solvers. This interest extends to complete SAT solvers, many based on the Davis- Putnam-Logemann-Loveland (DPLL) procedure, a variant of the Davis-Putnam (DP) procedure. Complete solvers determine both satisfiability and unsatisfiability. The DPLL procedure focuses on one-literal clauses, branches on truth assignments, and performs a backtrack search in the space of partial truth assignments. Since its introduction in 1962, the major improvements to DPLL have been smart branch selection
This paper is dedicated to Martin Davis, in recognition of his foundational contributions to the area of automated reasoning.
D. Loveland (B)
© Springer International Publishing Switzerland 2016 315
E. G. Omodeo and A. Policriti (eds.), Martin Davis on Computability,
Computational Logic, and Mathematical Foundations,
Outstanding Contributions to Logic 10, DOI 10.1007/978-3-319-41842-1_12
heuristics, extensions like clause learning and randomized restarts, and well-crafted data structures. The DP and DPLL procedures, and the major improvements that followed, will be reviewed in this paper.
The DPLL procedure, even half a century after its introduction, remains a foundational component of modern day SAT solvers. Through SAT solvers , as well as through satisfiability modulo theory (SMT)  and answer set programming (ASP)  solvers that build upon SAT techniques, the DPLL procedure has had a tremendous practical impact on the field with applications in a variety of areas such as formal verification, AI planning, and mathematical discovery.
The DP and DPLL programs were among the earliest propositional provers. It happens that all these earliest algorithms or programs were formulated in 1958 (excepting DPLL), in independent efforts. It is instructive to briefly consider these earliest programs for they collectively contain all the major features of the DPLL procedure except the most basic feature, introduced with the DP procedure.