Davis–Putnam algorithm: Difference between revisions

Revision as of 12:31, 26 May 2008

Latest revision as of 20:59, 5 August 2024

(89 intermediate revisions by 62 users not shown)

Line 1:

{{Short description|Check the validity of a logic formula}}

The '''Davis-Putnam algorithm''' was developed by [[Martin Davis]] and [[Hilary Putnam]] for checking the validity of a [[first-order logic]] formula. It is known that there exist no [[decision procedure]] for this task. Therefore the Davis-Putnam ''procedure'' does not terminate on some inputs so, strictly speaking, it is not an [[algorithm]].

In [[logic]] and [[computer science]], 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==

The procedure is based on [[Herbrand's theorem]], which implies that an un[[satisfiable]] formula has is un[[satisfiable]] [[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 <math>\phi</math> it is enough to prove that a ground instance of <math>\lnot\phi</math> is unsatisfiable. If <math>\phi</math> isn't valid, then the search for an unsatisfiable ground instance will not terminate.

[[File:Resolution.png|thumb|400px|Two runs of the 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''".]]

The procedure is based on [[Herbrand's theorem]], which implies that an un[[satisfiable|unsatisfiable]] formula has isan un[[satisfiable]]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 <math>\phi</math>''φ'' it is enough to prove that a ground instance of <math>\lnot\phi</math>''¬φ'' is unsatisfiable. If <math>\phi</math> isn't'φ'' is not valid, then the search for an unsatisfiable ground instance will not terminate.

The procedure roughly consists of these three parts:

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

* generate one by one all ground instances

* ...and check for each if it is satisfiable

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

The last part is probably the most innovative one, and works as follows:

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

* generate one by one all propositional ground instances, one by one

* ...and check forif each if itinstance 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 illustration), with an eager use of [[unit propagation]] and pure literal elimination (elimination of clauses with variables that occur only positively or only negatively in the formula).{{clarify|reason=In the algorithm below, adding to and removing from a formula should be defined. I guess the formula has to be in clausal normal form (this should be explained then), and adding and removing is achieved by set operations? Moreover, the 'consistent set of literals' test, and the concepts 'polarity', 'pure literal' and 'unit propagation' should be briefly explained.|date=June 2021}}

* for every variable in the formula

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

*** resolve <math>c</math> and <math>n</math> and add the resolvent to the formula

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

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

The step done for each variable preserve satisfiability, while not preserving the models; in other words, the generated formula is [[equisatisfiable]] but not [[equivalent]] with the original one.

Input: A set of clauses Φ.

Output: A Truth Value: true if Φ can be satisfied, false otherwise.

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

The [[DPLL algorithm]] is a refinement of the Davis-Putnam procedure that stemmed from its first implementation.

'''repeat'''

// ''unit propagation:''

'''while''' Φ contains a unit clause {''l''} '''do'''

'''for every''' clause ''c'' in Φ that contains ''l'' '''do'''

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

'''for every''' clause ''c'' in Φ that contains ¬''l'' '''do'''

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

Φ ← ''add-to-formula''(''c'' \ {¬''l''}, Φ);

// ''eliminate clauses not in normal form:''

'''for every''' clause ''c'' in Φ that contains both a literal ''l'' and its negation ¬''l'' '''do'''

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

// ''pure literal elimination:''

'''while''' there is a literal ''l'' all of which occurrences in Φ have the same polarity '''do'''

'''for every''' clause ''c'' in Φ that contains ''l'' '''do'''

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

// ''stopping conditions:''

'''if''' Φ is empty '''then'''

'''return''' true;

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

'''return''' false;

// ''Davis-Putnam procedure:''

pick a literal ''l'' that occurs with both polarities in Φ

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

// ''resolve c with n:''

''r'' ← (''c'' \ {''l''}) ∪ (''n'' \ {¬''l''});

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

'''for every''' clause ''c'' that contains ''l'' or ¬''l'' '''do'''

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

{{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.

{{Comp-sci-stub}}

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==

==See also==

*[[DPLL algorithm]]

*[[Herbrandization]]

==References==

Line 29 ⟶ 63:

|last=Davis

|first=Martin

|author2=Putnam, Hilary

| authorlink= Martin Davis

| coauthors= [[Hillary Putnam|Putnam, Hillary]]

| title=A Computing Procedure for Quantification Theory

| journal =[[Journal of the ACM]]

Line 36 ⟶ 69:

| issue = 3

| pages = 201–215

| dateyear = 1960

| doi=10.1145/321033.321034| doi-access =free

| url = http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=321034}}

}}

*{{cite journal

| last=Davis

| first=Martin |author2=Logemann, George |author3=Loveland, Donald

| coauthors=Logemann, George, and Loveland, Donald

| title=A Machine Program for Theorem Proving

| journal =[[Communications of the ACM]]

Line 48 ⟶ 80:

| issue=7

| pages = 394–397

| dateyear=1962

| url=http://portal.acm.org/citation.cfm?doid=368273.368557}}

| doi=10.1145/368273.368557| hdl=2027/mdp.39015095248095

| hdl-access=free

}}

* {{cite conference

| author = R. Dechter

| coauthors author2= I. Rish

| editor = J. Doyle and E. Sandewall and P. Torasso

| title = Directional Resolution: The Davis-PutnamDavis–Putnam Procedure, Revisited

| year =

| booktitlebook-title = Principles of Knowledge Representation and Reasoning: Proc. of the Fourth International Conference (KR'94)

| title = Directional Resolution: The Davis-Putnam Procedure, Revisited

| conferencepages = 134–145

| booktitle = Principles of Knowledge Representation and Reasoning: Proc. of the Fourth International Conference (KR'94)

| pages = 134-145

| publisher = Kaufmann

| url =

| conferenceurl =

}}

* {{cite book|author=John Harrison|title=Handbook of practical logic and automated reasoning|url=https://archive.org/details/handbookpractica00harr|url-access=limited|year=2009|publisher=Cambridge University Press|isbn=978-0-521-89957-4|pages=[https://archive.org/details/handbookpractica00harr/page/n100 79]–90}}

{{DEFAULTSORT:Davis-Putnam algorithm}}

[[Category:Boolean algebra]]

[[Category:Constraint satisfactionprogramming]]

[[Category:Automated theorem proving]]

[[de:Davis-Putnam-Verfahren]]

[[es:Algoritmo de Davis-Putnam]]

[[fr:Algorithme de Davis-Putnam]]

[[it:Davis-Putnam (Algoritmo)]]

[[pl:Procedura Davisa-Putnama]]

[[pt:Algoritmo de Davis-Putnam]]