Davis-Putnam process

from Wikipedia, the free encyclopedia

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

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

Beginning of a - unsuccessful - derivation from the formula (¬ x 1 ) ∧ ( x 1x 2x 4 ) ∧ ( x 3 ∨¬ x 1x 2 ) or as a set of clauses {{¬ x 1 }, { x 1 , x 2 , x 4 }, { x 3 , ¬ x 1 , x 2 }}: the one-literal rule for ¬ x 1 leads in three steps (complete deletion of the 1st and 3rd clauses, since they ¬ x 1 included, deletion of x 1 from the 2nd clause) to ( x 2x 4 ) or {{ x 2 , x 4 }}; from this, x 1 = 0 and, after further rule applications (not shown), ultimately x 2 = 1 is obtained. This assignment fulfills the original formula.
  • 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

Web links