Davis-Putnam-Verfahren

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

Das Davis-Putnam-Verfahren stellt Regeln für die Transformation von Blöcken in Blöcke, 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.

• Klausel: eine Menge von Literalen verbunden durch Disjunktion
• Formel: eine Menge von Klauseln verbunden durch Konjunktion
• Block: eine Menge von Formeln verbunden durch Disjunktion

Regeln

• Splitting Regel
  Sei F eine nichtleere Formel mit mindestens einer nichtleeren Klausel. Ersetze F durch zwei Formeln F[L] und $F[\bar L]$.
• One-Literal-Regel
  Sei F eine Formel der Form $F=F'\cup{L}$ (Das heißt L kommt in der Klausel alleine vor.) Ersetze F durch F[L].
• Pure-Literal-Regel
  Sei F eine Formel, die mindestens eine Klausel mit einem Literal L und keine Klausel mit dem Literal $\bar L$ enthält. Ersetze F durch F[L].
• Subsumption Regel
  Wenn eine Formel zwei Klauseln K₁,K₂ enthält mit $K_1 \subseteq K_2$, dann streiche K₂ aus F.
• Bereinigungsregel
  Streiche alle Klauseln, die eine atomare Formel A und Ihre Negation $\neg A$ enthalten

Hinweis:
F[L] wird aus F gewonnen, indem man

• alle L enthaltenden Klauseln streicht, und
• alle Vorkommnisse von $\neg L$ in den übrigen Klauseln streicht.

$F[\bar L]$ wird aus F in analoger Weise gewonnen, indem man

• alle $\neg L$ enthaltenden Klauseln streicht, und
• alle Vorkommnisse von L in den übrigen Klauseln streicht.

Herleitung

• Eine Herleitung aus der Formel F ist eine Sequenz F,B₁,B₂... 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

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.

Quellen

• Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. In: Journal of the ACM. 7, Nr. 3, 1960, S. 201–215.

Weblinks

• Interaktives Java-Applet zur Demonstration