DPLL: The Core of Modern Satisfiability Solvers

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.