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

Introduction

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)

Duke University, Durham, USA e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

A. Sabharwal

Allen Institute for AI, Seattle, USA e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

B. Selman

Cornell University, Ithaca, USA e-mail: This email address is being protected from spam bots, you need Javascript enabled to view it

© 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.[1]

The DPLL procedure, even half a century after its introduction, remains a foundational component of modern day SAT solvers. Through SAT solvers [4], as well as through satisfiability modulo theory (SMT) [40] and answer set programming (ASP) [19] 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.[2] 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.

  • [1] The papers introducing DP [12] and DPLL [11] each have over 3000 citations listed in GoogleScholar (May 2015), which is indicative of their tremendous influence over the years.
  • [2] The Dunham, Fridshal, and Sward project might have begun in 1957.
 
Source
< Prev   CONTENTS   Source   Next >