Davis–Putnam algorithm: Difference between revisions

Revision as of 11:16, 12 February 2022

Latest revision as of 20:59, 5 August 2024

(12 intermediate revisions by 10 users not shown)

Line 1:

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

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

Line 21 ⟶ 22:

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

'''if''' Φ is empty '''thenrepeat'''

// ''unit propagation:'return''' true;

'''ifwhile''' Φ contains ana emptyunit clause {''l''} '''thendo'''

'''returnfor every''' false;clause ''c'' in Φ that contains ''l'' '''do'''

Φ ← ''addremove-tofrom-formula''(''c'' \ {¬''l''}, Φ);

// ''unit propagation:''

'''whilefor every''' Φclause contains''c'' ain unitΦ clausethat contains {¬''l''} '''do'''

Φ ← ''remove-from-formula''({''lc''}, Φ);

Φ ← ''add-to-formula'for every''' clause (''c'' in Φ that contains\ {¬''l''}, '''do'''Φ);

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

'''for every''' clause ''c'' in Φ containingthat ''l''contains andboth everya clauseliteral ''nl'' in Φ containingand its negation ¬''l'' '''do'''

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

// ''pure literal elimination:''

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

'''for every ''' clause while''c'' in Φ that containsthere bothis a literal ''l'' andall itsof negationwhich ¬''l''occurrences in Φ have the same polarity '''do'''

Φ ← ''remove-from-formula'for every'('' clause ''c'', in Φ); that contains ''l'' '''do'''

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

// ''pure literal elimination:''

// ''stopping conditions:''

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

'''for everyif''' clause ''c'' in Φ thatis contains ''l''empty '''dothen'''

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

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

// ''Davis-Putnam procedure:''

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

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

// ''Davis-Putnam procedure:''

'''for every''' clause ''c'' in Φ containing ''l'' and every clause ''n'' in Φ containing its negation ¬''l'' '''do'''

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

'''for every''' clause ''c'' in Φ containing ''l'' and every clause ''n'' in Φ containing its negation ¬''l'' '''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'', Φ);

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

Line 66 ⟶ 70:

| pages = 201–215

| year = 1960

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

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

}}

| doi=10.1145/321033.321034}}

*{{cite journal

| last=Davis

Line 91 ⟶ 95:

}}

* {{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}}

Line 96 ⟶ 101:

[[Category:Constraint programming]]

[[Category:Automated theorem proving]]

{{formalmethods-stub}}