Davis–Putnam algorithm: Difference between revisions

Revision as of 10:28, 12 February 2022

Latest revision as of 20:59, 5 August 2024

(16 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(Φ)

'''repeat'''

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

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

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

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

'''for every''' unit clause { Φ ← ''lremove-from-formula''} ('''in'c'', Φ '''do''');

Φ ← ''unit-propagate'for every'(''l clause ''c'', in Φ); that contains ¬''l'' '''do'''

'''for every''' literal ''l'' that occurs pure '''in''' Φ ← ''remove-from-formula'do'(''c'', Φ);

Φ ← ''pureadd-literalto-assignformula''(''c'' \ {¬''l''}, Φ);

// ''Davis-Putnameliminate clauses not in normal procedureform:''

'''for every''' literalclause ''lc'' thatin occursΦ inthat contains both polaritiesa literal ''l'in' and its negation ¬''l'' Φ '''do'''

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

'''for every''' clause ''c'' containing ''l'' and every clause ''n'' containing the negation of ''l'' '''in''' Φ '''do'''

// ''r''pure ←literal elimination:''resolve''(''c'', ''n'');

'''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 a consistent set of literalsempty '''then'''

'''return''' ''DP-SAT''(Φ)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 ''c'' in Φ containing ''l'' and every clause ''n'' in Φ containing theits negation of ¬''l'' '''in''' Φ '''do'''

// ''resolve c with n:''

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

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

'''for every''' clause ''c'' that contains ''l'' or its negation¬''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 57 ⟶ 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 82 ⟶ 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 87 ⟶ 101:

[[Category:Constraint programming]]

[[Category:Automated theorem proving]]

{{formalmethods-stub}}