Das Davis-Putnam-Verfahren (nach Martin Davis und Hilary Putnam) entscheidet über die Unerfüllbarkeit einer aussagenlogischen Formel in konjunktiver Normalform. Das Verfahren sollte nicht mit der Weiterentwicklung, dem DPLL (Davis-Putnam-Logemann-Loveland)-Algorithmus, verwechselt werden.

Definition

Bearbeiten

Das Davis-Putnam-Verfahren stellt Regeln für die Transformation von Blöcken in Blöcke, von der Form „ersetze eine Klausel durch eine (eventuell leere) Klauselmenge“ zur Verfügung. Wenn B in B' transformiert wird, dann ist B unerfüllbar genau dann, wenn B' unerfüllbar ist. Ein Block ist unerfüllbar, wenn alle Formeln, die er enthält, unerfüllbar sind.

Eine Sequenz von Blöcken (eine Herleitung) wird mit Hilfe von Regeln erzeugt. Die Formel ist unerfüllbar, wenn ein „syntaktisch unerfüllbarer Block“ erzeugt wird, und erfüllbar, wenn ein „syntaktisch erfüllbarer Block“ erzeugt wird.

 
Beginn einer – nicht erfolgreichen – Herleitung aus der Formel (¬x1) ∧ (x1x2x4) ∧ (x3∨¬x1x2) bzw. als Klauselmenge { {¬x1}, {x1,x2,x4}, {x3x1,x2} }: die One-Literal-Regel für ¬x1 führt in drei Schritten (komplettes Streichen der 1. und 3. Klausel, da sie ¬x1 enthalten, Streichen von x1 aus der 2. Klausel) zu (x2x4) bzw. { {x2,x4} }; daraus wird x1=0 und nach weiteren (nicht gezeigten) Regelanwendungen letztlich x2=1 gewonnen. Diese Belegung erfüllt die ursprüngliche Formel.
  • Splitting-Regel
    Sei   eine nichtleere Formel mit mindestens einer nichtleeren Klausel  , sei   ein Literal in  . Ersetze   durch zwei Formeln   und  .
  • One-Literal-Regel
    Sei   eine Formel der Form   (Das heißt   komme in einer Klausel von   alleine vor.) Ersetze   durch  .
  • Pure-Literal-Regel
    Sei   eine Formel, die mindestens eine Klausel mit einem Literal   und keine Klausel mit dem Literal   enthält. Ersetze   durch  .
  • Subsumption-Regel
    Wenn eine Formel zwei Klauseln   enthält mit  , dann streiche   aus  .
  • Bereinigungsregel
    Streiche alle Klauseln, die ein Literal   und seine Negation   enthalten.

Hinweis:
  wird aus   gewonnen, indem man

  • alle   enthaltenden Klauseln streicht, und
  • alle Vorkommnisse von   in den übrigen Klauseln streicht.

  wird aus   in analoger Weise gewonnen, indem man

  • alle   enthaltenden Klauseln streicht, und
  • alle Vorkommnisse von   in den übrigen Klauseln streicht.

Herleitung

Bearbeiten
  • Eine Herleitung aus der Formel F ist eine Sequenz   von Blöcken, die mit Hilfe der Regeln konstruiert wird.
  • Eine Herleitung ist maximal, wenn sie nicht erweitert werden kann.
  • Eine Herleitung ist erfolgreich, wenn sie mit einem Block endet, der in jeder Formel die leere Klausel enthält.
  • Eine Herleitung ist nicht erfolgreich, wenn sie mit einem Block endet, der eine leere Formel enthält.

Korrektheit

Bearbeiten

Sei F eine unerfüllbare Formel. Dann ist jede maximale Herleitung aus F erfolgreich. Sei F eine erfüllbare Formel. Dann ist jede maximale Herleitung aus F nicht erfolgreich.

  • Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. In: Journal of the ACM. Vol. 7, Nr. 3, 1960, S. 201–215, doi:10.1145/321033.321034 (englisch).