DPLL algorithm
In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.
Class
It was introduced in 1961 by Martin Davis, George Logemann and Donald W. Loveland and is a refinement of the earlier Davis–Putnam algorithm, which is a resolution-based procedure developed by Davis and Hilary Putnam in 1960. Especially in older publications, the Davis–Logemann–Loveland algorithm is often referred to as the "Davis–Putnam method" or the "DP algorithm". Other common names that maintain the distinction are DLL and DPLL.
Implementations and applications[edit]
The SAT problem is important both from theoretical and practical points of view. In complexity theory it was the first problem proved to be NP-complete, and can appear in a broad variety of applications such as model checking, automated planning and scheduling, and diagnosis in artificial intelligence.
As such, writing efficient SAT solvers has been a research topic for many years. GRASP (1996-1999) was an early implementation using DPLL.[1] In the international SAT competitions, implementations based around DPLL such as zChaff[2] and MiniSat[3] were in the first places of the competitions in 2004 and 2005.[4]
Another application that often involves DPLL is automated theorem proving or satisfiability modulo theories (SMT), which is a SAT problem in which propositional variables are replaced with formulas of another mathematical theory.
Related algorithms[edit]
Since 1986, (Reduced ordered) binary decision diagrams have also been used for SAT solving.
In 1989-1990, Stålmarck's method for formula verification was presented and patented. It has found some use in industrial applications.[6]
DPLL has been extended for automated theorem proving for fragments of first-order logic by way of the DPLL(T) algorithm.[1]
In the 2010-2019 decade, work on improving the algorithm has found better policies for choosing the branching literals and new data structures to make the algorithm faster, especially the part on unit propagation. However, the main improvement has been a more powerful algorithm, Conflict-Driven Clause Learning (CDCL), which is similar to DPLL but after reaching a conflict "learns" the root causes (assignments to variables) of the conflict, and uses this information to perform non-chronological backtracking (aka backjumping) in order to avoid reaching the same conflict again. Most state-of-the-art SAT solvers are based on the CDCL framework as of 2019.[7]
Relation to other notions[edit]
Runs of DPLL-based algorithms on unsatisfiable instances correspond to tree resolution refutation proofs.[8]
General
Specific