imported>Graph Pixel: Tippfehler korrigiert.

2025-10-12T10:02:56Z

Tippfehler korrigiert.

Neue Seite

'''Einheitsresolution''' ({{EnS|''unit propagation''}}) ist in der [[Mathematische Logik|mathematischen Logik]] eine Vorgehensweise um eine Menge von [[Disjunktionsterm|Klausel]]n 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-Solver]]n.

== Vorgehensweise ==

Sei eine Klauselmenge mit Einheitsklausel <math>\psi</math> gegeben. Dann vereinfacht man die anderen Klauseln aus der gegebenen Klauselmenge durch zwei Regeln:

# Entferne alle Klauseln, die <math>\psi</math> enthalten (die Einheitsklausel selbst wird nicht entfernt).
# Wenn eine Klausel <math>\neg \psi</math> enthält, dann entferne dieses Literal aus der Klausel.

Die vereinfachte Klauselmenge ist dann [[Logische Äquivalenz|logisch äquivalent]] zu der ursprünglichen Klauselmenge.

Manchmal genügt es auch eine [[Erfüllbarkeitsäquivalenz|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.

== Beispiel ==

Gegeben sei die folgende Klauselmenge:

: <math>\{a \vee c, \neg c, b \vee c, a \vee \neg c\}</math>

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

: <math>\{a, b, \neg c\}</math>

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

== Korrektheit der Einheitsresolution ==

Seien <math>\varphi = \varphi_{1} ... \varphi_{n}</math> Klauseln, in denen die Einheitsklausel <math>a</math> nicht vorkommt. Des Weiteren seien <math>(\psi_{1} \vee a) ... (\psi_{n} \vee a)</math> Klauseln, in denen <math>a</math> vorkommt und <math>(\tau_{1} \vee \neg a) ... (\tau_{n} \vee \neg a)</math> Klauseln, in denen <math>\neg a</math> vorkommt.

Sei der Antezendent nun <math>A = \{\varphi_{1}, ..., \varphi_{n}, (\psi_{1} \vee a), ..., (\psi_{n} \vee a), (\tau_{1} \vee \neg a), ..., (\tau_{n} \vee \neg a), a\}</math>, so muss die Konjunktion des Sukzedenten <math>S = \{\varphi_{1}, ..., \varphi_{n}, (\tau_{1} \vee \neg a), ..., (\tau_{n} \vee \neg a), a\}</math> ein semantisches Modell der Konjunktion des Antezendenten sein.
Mit anderen Worten: <math>\textstyle A \vdash S \Rightarrow \bigwedge_{a \in A} a \models \bigwedge_{s \in S} s</math>

Fall <math>a = \perp</math>:
:<math>\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</math>
wegen <math>\varphi \land \perp \equiv \perp</math>

Fall <math>a = \top</math>:
: <math>\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</math>
: <math>\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</math>
: <math>\equiv \varphi \land \top \land ... \land \top \land \tau_{1} \land ... \land \tau_{n} \land a</math>
: <math>\equiv \varphi \land \tau_{1} \land ... \land \tau_{n} \land a</math>

== Vergleich mit Resolution ==
* Der zweite Schritt der Einheitsresolution kann als Spezialfall von [[Resolution (Logik)|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 Einheitsresolution gilt das im Allgemeinen nicht. Jedoch ist die Einheitsresolution ein vollständiges Verfahren für die Erfüllbarkeit von [[Horn-Formel]]n 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.

[[Kategorie:Mathematische Logik]]
[[Kategorie:Angewandte Informatik]]

Einheitsresolution - Versionsgeschichte

imported>Graph Pixel: Tippfehler korrigiert.