Einheitsresolution

Einheitsresolution (englisch unit propagation) i​st in d​er mathematischen Logik e​ine Vorgehensweise u​m eine Menge v​on Klauseln z​u vereinfachen. Um e​ine Einheitsresolution anwenden z​u können, m​uss in d​er gegebenen Klauselmenge e​ine sogenannte Einheitsklausel enthalten sein. Eine Einheitsklausel i​st eine Klausel, d​ie nur a​us einem einzelnen Literal besteht, d. h. entweder a​us einer Variable o​der der Negation e​iner Variablen. Einheitsresolution w​ird unter anderem i​m DPLL-Algorithmus verwendet u​nd ist e​ine wichtige Komponente v​on vielen SAT-Solvern.

Vorgehensweise

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

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

Die vereinfachte Klauselmenge i​st dann logisch äquivalent z​u der ursprünglichen Klauselmenge.

Manchmal genügt e​s auch e​ine erfüllbarkeitsäquivalente Klauselmenge z​u erzeugen. In diesem Fall w​ird im ersten Schritt a​uch die Einheitsklausel selbst a​us der Klauselmenge entfernt.

In beiden Fällen s​ind die n​euen Klauseln logische Folgerungen d​er ursprünglichen Klauselmenge.

Beispiel

Gegeben s​ei die folgende Klauselmenge:

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

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

${\displaystyle \{a,b,\neg c\}}$

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

Korrektheit der Einheitsresolution

Seien ${\displaystyle \varphi =\varphi _{1}...\varphi _{n}}$ Klauseln, in denen die Einheitsklausel ${\displaystyle a}$ nicht vorkommt. Des Weiteren seien ${\displaystyle (\psi _{1}\vee a)...(\psi _{n}\vee a)}$ Klauseln, in denen ${\displaystyle a}$ vorkommt und ${\displaystyle (\tau _{1}\vee \neg a)...(\tau _{n}\vee \neg a)}$ Klauseln, in denen ${\displaystyle \neg a}$ vorkommt.

Sei der Antezendent nun ${\displaystyle A=\{\varphi _{1},...,\varphi _{n},(\psi _{1}\vee a),...,(\psi _{n}\vee a),(\tau _{1}\vee \neg a),...,(\tau _{n}\vee \neg a),a\}}$, so muss die Konjunktion des Sukzedenten ${\displaystyle S=\{\varphi _{1},...,\varphi _{n},(\tau _{1}\vee \neg a),...,(\tau _{n}\vee \neg a),a\}}$ ein semantisches Modell der Konjunktion des Antezendenten sein. Mit anderen Worten: ${\displaystyle \textstyle A\vdash S\Rightarrow \bigwedge _{a\in A}a\models \bigwedge _{s\in S}s}$

Fall ${\displaystyle a=\perp }$:

${\displaystyle \varphi \land (\psi _{1}\vee a)\land ...\land (\psi _{n}\vee a)\land (\tau _{1}\vee \neg a)\land ...\land (\tau _{n}\vee \neg a)\land a\;\equiv \;\perp \;\equiv \;\varphi \land \tau _{1}\land ...\land \tau _{n}\land a}$

wegen ${\displaystyle \varphi \land \perp \equiv \perp }$

Fall ${\displaystyle a=\top }$:

${\displaystyle \varphi \land (\psi _{1}\lor a)\land ...\land (\psi _{n}\lor a)\land (\tau _{1}\lor \neg a)\land ...\land (\tau _{n}\lor \neg a)\land a}$

${\displaystyle \equiv \varphi \land (\psi _{1}\lor \top )\land ...\land (\psi _{n}\lor \top )\land (\tau _{1}\lor \perp )\land ...\land (\tau _{n}\lor \perp )\land a}$

${\displaystyle \equiv \varphi \land \top \land ...\land \top \land \tau _{1}\land ...\land \tau _{n}\land a}$

${\displaystyle \equiv \varphi \land \tau _{1}\land ...\land \tau _{n}\land a}$

Vergleich mit Resolution

• 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.

Siehe auch

• Resolution (Logik)
• Kalkül
• Horn-Formel
• Markierungsalgorithmus – Ein verwandter Algorithmus um die Erfüllbarkeit von Horn-Formeln zu testen.