Davis–Putnam algorithm: Difference between revisions

Revision as of 12:44, 19 November 2021

Latest revision as of 20:59, 5 August 2024

(17 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 14 ⟶ 15:

** 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 ofthat occur only onepositively or only polaritynegatively 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}}

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

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 Φ ← ''{l}remove-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''' 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'', Φ);

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

Φ ← ''remove-from-formula'return'('' c''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 56 ⟶ 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 81 ⟶ 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 86 ⟶ 101:

[[Category:Constraint programming]]

[[Category:Automated theorem proving]]

{{formalmethods-stub}}