Einheitsresolution

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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 Einheitsklausel enthalten sein, das heißt eine Klausel, die nur aus einem einzelnen Literal besteht. Ein Literal ist eine Variable oder ihre Negation, die für sich alleine in einer Klausel steht. Einheitsresolution wird unter anderem vom DPLL-Algorithmus verwendet und ist eine wichtige Komponente von vielen SAT-Solvern.

Vorgehensweise[Bearbeiten]

Sei eine Einheitsklausel \{\psi\} in der Klauselmenge gegeben. Dann vereinfacht man die anderen Klauseln aus der gegebenen Klauselmenge durch zwei Regeln:

  1. Entferne alle Klauseln, die \psi enthalten.
  2. Wenn eine Klausel \neg \psi enthält, dann entferne dieses Literal aus der Klausel.

Beispiel[Bearbeiten]

Gegeben sei die folgende Klauselmenge:

\{\{a \vee c\}, \{\neg c\}, \{b \vee c\}, \{a \vee \neg c\}\}

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

\{\{a\}, \{b\}\}

Alle Klauseln, die \neg c enthielten, wurden komplett aus der Klauselmenge entfernt. Dies waren die Klauseln \{\neg c\} und \{a \vee \neg c\}. Außerdem wurde das Literal c aus allen Klauseln entfernt. Dies geschah in den verbleibenden zwei Klauseln \{a \vee c\} und \{b \vee c\}.

Siehe auch[Bearbeiten]