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)