Davis–Putnam algorithm

The Davis-Putnam algorithm is an algorithm for checking the satisfiability of formulae in conjunctive normal form, i.e., sets 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 positively with any clause in which the variable is negated.

The algorithm works as follows:

• for every variable in the formula
  • for every clause ${\displaystyle c}$ containing the variable and every clause ${\displaystyle n}$ containing the negation of the variable
    • resolve ${\displaystyle c}$ and ${\displaystyle n}$ and add the resolvant to the formula
  • 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

• DPLL
• Martin Davis
• Hilary Putnam