Davis-Putnam process
The Davis-Putnam method (after Martin Davis and Hilary Putnam ) decides whether a propositional formula in conjunctive normal form cannot be fulfilled . The procedure should not be confused with the further development, the DPLL ( Davis-Putnam-Logemann-Loveland ) algorithm.
definition
- Clause: a set of literals connected by disjunction
- Formula: a set of clauses connected by conjunction
- Block: a set of formulas connected by disjunction
The Davis-Putnam method provides rules for the transformation of blocks into blocks, of the form "replace a clause with a (possibly empty) set of clauses". If B is transformed into B ', then B is unsatisfiable if and only if B' is unsatisfiable. A block is unsatisfiable if all the formulas it contains are unsatisfiable.
A sequence of blocks (a derivation) is generated with the help of rules. The formula is unsatisfiable if a "syntactically unsatisfiable block" is generated, and satisfiable if a "syntactically unsatisfiable block" is generated.
regulate
- Splitting rule
Let be a non-empty formula with at least one non-empty clause , be a literal in . Replace with two formulas and . - One-literal rule
Be a formula of the form (that is, appear in a clause by itself.) Replace with . - Pure literal rule
Be a formula that contains at least one clause with a literal and no clause with the literal . Replace with . - Subsumption rule
If a formula contains two clauses with , then cross out . - Cleansing Rule
Delete all clauses that contain a literal and its negation .
Note: is obtained from by one
- delete all containing clauses, and
- deletes all occurrences of in the remaining clauses.
is obtained from in an analogous manner by one
- delete all containing clauses, and
- deletes all occurrences of in the remaining clauses.
Derivation
- A derivation from the formula F is a sequence of blocks that is constructed with the help of the rules.
- A derivation is maximum if it cannot be expanded.
- A derivation is successful when it ends with a block that contains the empty clause in every formula.
- A derivation is unsuccessful if it ends with a block containing an empty formula.
correctness
Let F be an unsatisfiable formula. Then every maximal derivation from F is successful. Let F be a satisfiable formula. Then any maximal derivation from F is unsuccessful.
swell
- Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory . In: Journal of the ACM . 7, No. 3, 1960, pp. 201-215.