Davis–Putnam algorithm: Difference between revisions

Revision as of 13:42, 6 December 2020

Revision as of 23:20, 23 June 2021

Line 1:

The '''Davis–Putnam algorithm''' was developed by [[Martin Davis (mathematician)|Martin Davis]] and [[Hilary Putnam]] for checking the validity of a [[first-order logic]] formula using a [[Resolution (logic)|resolution]]-based decision procedure for [[propositional logic]]. Since the set of valid first-order formulas is [[recursively enumerable]] but not [[Recursive set|recursive]], there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure ('''Davis-Putnam procedure''') that is actually only one of the steps of the original algorithm.

==Overview==

[[File:Resolution.png|thumb|400px|Two runs of the [[:en:Davis-Putnam procedure|Davis-Putnam procedure]] on example propositional ground instances.

''Top to bottom, Left:'' Starting from the formula <math>(a \lor b \lor c) \land (b \lor \lnot c \lor \lnot f) \land (\lnot b \lor e)</math>, the algorithm resolves on <math>b</math>, and then on <math>c</math>. Since no further resolution is possible, the algorithm stops; since the [[empty clause]] couldn't be derived, the result is "''satisfiable''".

''Right:'' Resolving the given formula on <math>b</math>, then on <math>a</math>, then on <math>c</math> yields the empty clause; hence the algorithm returns "''unsatisfiable''".]]

Line 8:

The procedure is based on [[Herbrand's theorem]], which implies that an [[satisfiable|unsatisfiable]] formula has an unsatisfiable [[ground instance]], and on the fact that a formula is valid if and only if its negation is unsatisfiable. Taken together, these facts imply that to prove the validity of ''φ'' it is enough to prove that a ground instance of ''¬φ'' is unsatisfiable. If ''φ'' is not valid, then the search for an unsatisfiable ground instance will not terminate.

The procedure for checking validity of a formula ''φ'' roughly consists of these three parts:

* put the formula ''¬φ'' in [[prenex]] form and eliminate quantifiers

* generate all propositional ground instances, one by one

* check if each instance is satisfiable.

** If some instance is unsatisfiable, then return that ''φ'' is valid. Else continue checking.

The last part is a [[SAT solver]] based on [[Resolution (logic)|resolution]] (as seen on the ilustration), with an eager use of [[unit propagation]] and pure literal elimination (elimination of clauses with variables of only one polarity in the formula).

The last part is probably the most innovative one, and works as follows (cf. picture):

) for optimalization (with both optimalizations included already in the original paper by Davis and Putnam). It follows:

{{Algorithm-begin|name=DP SAT solver}}

* for every variable in the formula

Input: A set of clauses Φ.

** for every clause <math>c</math> containing the variable and every clause <math>n</math> containing the negation of the variable

Output: A Truth Value.

*** [[Resolution (logic)|resolve]] ''c'' and ''n'' and add the resolvent to the formula

** remove all original clauses containing the variable or its negation

'''function''' DP-SAT(Φ)

At each step, the intermediate formula generated is [[equisatisfiable]], but possibly not [[Logical equivalence|equivalent]], to the original formula. The resolution step leads to a worst-case exponential blow-up in the size of the formula.

'''if''' Φ is a consistent set of literals '''then'''

'''return''' true;

'''if''' Φ contains an empty clause '''then'''

'''return''' false;

'''for every''' unit clause ''{l}'' '''in''' Φ '''do'''

Φ ← ''unit-propagate''(''l'', Φ);

'''for every''' literal ''l'' that occurs pure '''in''' Φ '''do'''

Φ ← ''pure-literal-assign''(''l'', Φ);

// ''Davis-Putnam procedure:''

'''for every''' literal ''l'' that occurs in both polarities '''in''' Φ '''do'''

** '''for every''' clause <math>''c</math>'' containing the variable''l'' and every clause <math>''n</math>'' containing the negation of the''l'' '''in''' Φ variable'''do'''

''r'' ← ''resolve''(''c'', ''n'');

Φ ← ''add-to-formula''(''r'', Φ);

Φ ← ''remove-from-formula''(''c'', ''n'', Φ);

'''return''' ''DP-SAT''(Φ)

{{Algorithm-end}}

At each step of the SAT solver, the intermediate formula generated is [[equisatisfiable]], but possibly not [[Logical equivalence|equivalent]], to the original formula. The resolution step leads to a worst-case exponential blow-up in the size of the formula.

The [[Davis–Putnam–Logemann–Loveland algorithm]] is a 1962 refinement of the propositional satisfiability step of the Davis–Putnam procedure which requires only a linear amount of memory in the worst case. It still forms the basis for today's (as of 2015) most efficient complete [[SAT solver]]s.

The [[Davis–Putnam–Logemann–Loveland algorithm]] is a 1962 refinement of the propositional satisfiability step of the Davis–Putnam procedure which requires only a linear amount of memory in the worst case. It eschews the resolution for ''the splitting rule'': a backtracking algorithm that chooses a literal ''l'', and then recursively checks if a simplified formula with ''l'' assigned a true value is satisfiable or if a simplified formula with ''l'' assigned false is. It still forms the basis for today's (as of 2015) most efficient complete [[SAT solver]]s.

==See also==