Davis–Putnam algorithm: Difference between revisions

Revision as of 11:24, 12 February 2022

Latest revision as of 20:59, 5 August 2024

(11 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 22 ⟶ 23:

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

'''repeat'''

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

'''return''' true;

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

'''return''' false;

// ''unit propagation:''

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

Φ'''for ←every''' clause ''remove-from-formulac''({ 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:''

'''for everywhile''' there is a literal ''l'' thatall occursof purewhich 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 Φ

Line 48 ⟶ 52:

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