Einheitsresolution

aus Wikipedia, der freien Enzyklopädie
Zur Navigation springen Zur Suche springen

Einheitsresolution (englisch unit propagation) ist in der mathematischen Logik eine Vorgehensweise um eine Menge von Klauseln zu vereinfachen. Um eine Einheitsresolution anwenden zu können, muss in der gegebenen Klauselmenge eine sogenannte Einheitsklausel enthalten sein. Eine Einheitsklausel ist eine Klausel, die nur aus einem einzelnen Literal besteht, d. h. entweder aus einer Variable oder der Negation einer Variablen. Einheitsresolution wird unter anderem im DPLL-Algorithmus verwendet und ist eine wichtige Komponente von vielen SAT-Solvern.

Sei eine Klauselmenge mit Einheitsklausel gegeben. Dann vereinfacht man die anderen Klauseln aus der gegebenen Klauselmenge durch zwei Regeln:

  1. Entferne alle Klauseln, die enthalten (die Einheitsklausel selbst wird nicht entfernt).
  2. Wenn eine Klausel enthält, dann entferne dieses Literal aus der Klausel.

Die vereinfachte Klauselmenge ist dann logisch äquivalent zu der ursprünglichen Klauselmenge.

Manchmal genügt es auch eine erfüllbarkeitsäquivalente Klauselmenge zu erzeugen. In diesem Fall wird im ersten Schritt auch die Einheitsklausel selbst aus der Klauselmenge entfernt.

In beiden Fällen sind die neuen Klauseln logische Folgerungen der ursprünglichen Klauselmenge.

Gegeben sei die folgende Klauselmenge:

In dieser Klauselmenge ist eine Einheitsklausel. Wäre die Klausel in der Klauselmenge enthalten, so wäre diese ebenfalls eine Einheitsklausel. Diese Klauselmenge kann man durch Anwendung dieser zwei Regeln vereinfachen, wobei die Einheitsklausel ist. Das Ergebnis ist die Klauselmenge:

Alle Klauseln, die enthielten, wurden komplett aus der Klauselmenge entfernt. Dies war die Klausel . Außerdem wurde das Literal aus allen Klauseln entfernt. Dies geschah in den verbleibenden zwei Klauseln und . Die Einheitsklausel muss dabei behalten bleiben, da sich sonst der Wahrheitsgehalt der Aussage ändern würde.

Korrektheit der Einheitsresolution

[Bearbeiten | Quelltext bearbeiten]

Seien Klauseln, in denen die Einheitsklausel nicht vorkommt. Des Weiteren seien Klauseln, in denen vorkommt und Klauseln, in denen vorkommt.

Sei der Antezendent nun , so muss die Konjunktion des Sukzedenten ein semantisches Modell der Konjunktion des Antezendenten sein. Mit anderen Worten:

Fall :

wegen

Fall :

Vergleich mit Resolution

[Bearbeiten | Quelltext bearbeiten]
  • Der zweite Schritt der Einheitsresolution kann als Spezialfall von Resolution interpretiert werden. Hier betrachtet man eine Einheitsklausel und berechnet alle möglichen Resolventen von dieser Einheitsklausel. Bei der Einheitsresolution werden aber, im Gegensatz zum Resolutionsverfahren, die ursprünglichen Klauseln verworfen sobald eine vereinfachte Klausel gebildet wird.
  • Der erste Schritt der Einheitsresolution hat kein Äquivalent im Resolutionsverfahren. Insbesondere werden im Resolutionsverfahren nur Klauseln hinzugefügt aber nie Klauseln verworfen.
  • Das Resolutionsverfahren ist vollständig in dem Sinne, dass es für jede aussagenlogische Formel die Erfüllbarkeit entweder zeigt oder widerlegt. Für Einheitresolution gilt das im Allgemeinen nicht. Jedoch ist die Einheitsresolution ein vollständiges Verfahren für die Erfüllbarkeit von Horn-Formeln wenn sie iterativ für neue Einheitsklauseln angewendet wird.