> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/terms/sat-solvers.md).

# DPLL algorithm

<https://en.wikipedia.org/wiki/DPLL_algorithm>

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.

**Related**

<https://en.wikipedia.org/wiki/Conjunctive_normal_form> <https://en.wikipedia.org/wiki/Herbrandization> <https://en.wikipedia.org/wiki/Chaff_algorithm> <https://en.wikipedia.org/wiki/Propositional_variable> <https://en.wikipedia.org/wiki/Automated_theorem_proving> <https://en.wikipedia.org/wiki/Propositional_calculus> <https://en.wikipedia.org/wiki/Boolean_satisfiability_problem> <https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem>

Wikimedia Commons has media related to DPLL algorithm:

* <https://www.wikiwand.com//upload.wikimedia.org/wikipedia/en/thumb/4/4a/Commons-logo.svg/30px-Commons-logo.svg.png>
* <https://commons.wikimedia.org/wiki/Category:Davis-Putnam-Logemann-Loveland_algorithm>

**Online Tools**

Online SAT solvers <https://en.wikipedia.org/w/index.php?title=Boolean_satisfiability_problem&action=edit%C2%A7ion=19>

Offline SAT solvers <https://en.wikipedia.org/w/index.php?title=Boolean_satisfiability_problem&action=edit%C2%A7ion=20>

<http://logictools.org/propositional.html> <http://www.cs.man.ac.uk/~schmidt/tools/> <http://www.phil.cmu.edu/projects/apros/index.php>

**General**

Category:SAT solvers <https://en.wikipedia.org/wiki/Category:SAT_solvers?oldformat=true>

Category: Automated theorem proving <https://en.wikipedia.org/wiki/Category:Automated_theorem_proving?oldformat=true>

**Books**

* "A Computing Procedure for Quantification Theory"

  Martin Davis, Hilary Putnam
* "A Machine Program for Theorem Proving"

  Martin Davis, George Logemann, Donald Loveland (1962)
* "How Good Are Branching Rules in DPLL?"

  Ouyang, Ming (1998)
* "Handbook of practical logic and automated reasoning"

  John Harrison (2009)

**Specific**

"Abstract DPLL and Abstract DPLL Modulo Theories" (PDF) <http://www.lsi.upc.edu/~roberto/papers/lpar04.pdf> Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesar (2004),

The international SAT Competitions web page <http://www.satcompetition.org/>

zChaff website <http://www.princeton.edu/~chaff/zchaff.html>

Minisat website <http://minisat.se/>

"The Impact of Branching Heuristics in Propositional Satisfiability Algorithms" Marques-Silva, João P. (1999)

"Backtracking search algorithms" Van Beek, Peter (2006)