Davis–Putnam algorithm

The Davis-Putnam algorithm is an algorithm for checking the satisfiability of formulae in conjunctive normal form, i.e., set of clauses. It is a form of resolution in which variables are iteratively chosen and removed by resolving every clause in which the variable is contained with a variable in which the variable is negated.

The algorithm works as follows:

• for every variable in the formula
  • for every clause $c$ containing the variable and every clause $n$ containig the negation of the variable
    • resolve $c$ and $n$
  • remove all original clauses containing the variable or its negation

The name Davis-Putnam algorithm or DP algorithm is sometimes incorrecty used to refer to the Davis-Logemann-Loveland algorithm.

See also

• Martin Davis
• Hilary Putnam