Zeitin-Transformation

Die Zeitin-Transformation (auch Zeitin-Verfahren, Tseitin-Transformation, Tseitin-Verfahren) bezeichnet eine Methode, mit der Formeln aus der Aussagenlogik auf eine konjunktive Normalform (KNF) gebracht werden können. Die resultierende konjunktive Normalform ist dabei im Allgemeinen nicht äquivalent, sondern nur erfüllbarkeitsäquivalent. Das Verfahren wurde von Grigori Zeitin entwickelt.

Motivation

Üblicherweise werden Äquivalenzumformungen wie etwa die De Morgan’schen Gesetze, das Distributivgesetz und andere verwendet, um eine beliebige aussagenlogische Formel in eine konjunktive Normalform zu bringen.

Durch die Anwendung des Distributivgesetzes kann es im Allgemeinen zu einem exponentiellen Anstieg der Anzahl der Konjunktionen kommen. Um diesen Anstieg zu begrenzen, wird die Formel in eine nur erfüllbarkeitsäquivalente Form gebracht.

Für ein Beispiel mit 2 Klauseln mit je 4 Variablen, auf die das Distributivgesetz angewandt wird, sieht man den sich dabei ergebenden, exponentiellen Anstieg der Konjunktionen:

<math>

\begin{align} (p_1 \land p_2 \land p_3 \land p_4) \lor (q_1 \land q_2 \land q_3 \land q_4) \equiv \;& (p_1 \lor q_1) \land (p_1 \lor q_2) \land (p_1 \lor q_3) \land (p_1 \lor q_4) \land \\

& (p_2 \lor q_1) \land (p_2 \lor q_2) \land (p_2 \lor q_3) \land (p_2 \lor q_4) \land \\
& (p_3 \lor q_1) \land (p_3 \lor q_2) \land (p_3 \lor q_3) \land (p_3 \lor q_4) \land \\
& (p_4 \lor q_1) \land (p_4 \lor q_2) \land (p_4 \lor q_3) \land (p_4 \lor q_4)

\end{align} </math>

Idee

Durch die Verwendung einer erfüllbarkeitsäquivalenten Umformung ist es möglich, während der Transformation Variablen einzuführen.

Die grundlegende Idee ist dabei, für jede Subformel eine Variable einzuführen. Mithilfe der aussagenlogischen Äquivalenz werden dann diese Subformeln mit den neuen Variablen verbunden und alle resultierenden Bedingungen miteinander konjugiert. Danach wird jede dieser Bedingungen separat in KNF gebracht.

Beispiel

Das Beispiel soll hier an der Formel <math>\phi</math> gezeigt werden.

Zunächst werden alle Teilformeln der Länge nach aufgelistet:

<math>

\begin{align} &\neg s\\ &p \lor q\\ &(p \lor q) \land r\\ &((p \lor q) \land r) \to (\neg s) \end{align} </math>

Nun werden 4 Variablen eingeführt und durch das Bikonditional mit den Subformeln verknüpft. Bei dieser Gelegenheit werden Teilformeln bereits durch entsprechende Variablen substituiert:

<math>

\begin{align} x_1 &\leftrightarrow \neg s\\ x_2 &\leftrightarrow p \lor q\\ x_3 &\leftrightarrow x_2 \land r\\ x_4 &\leftrightarrow x_3 \to x_1 \end{align} </math>

Nun werden alle diese Substitutionen konjugiert. Wichtig dabei ist, dass die Variable, die für die ursprüngliche Formel <math>\phi</math> stand, als eigenes Konjunkt hinzugefügt wird.

Die entsprechende neue Formel sieht wie folgt aus:

<math>

T(\phi) := x_4 \land (x_4 \leftrightarrow x_3 \to x_1) \land (x_3 \leftrightarrow x_2 \land r) \land (x_2 \leftrightarrow p \lor q) \land (x_1 \leftrightarrow \neg s) </math>

Nun muss nur noch jedes Konjunkt separat in eine KNF umgewandelt werden, und zwar mit Hilfe der üblichen Äquivalenzumformungen. Exemplarisch wird dies an einem Konjunkt gezeigt:

<math>

\begin{align} x_2 \leftrightarrow p \lor q &\equiv x_2 \to (p \lor q) \land ((p \lor q) \to x_2) \\ &\equiv (\neg x_2 \lor p \lor q) \land (\neg(p \lor q) \lor x_2) \\ &\equiv (\neg x_2 \lor p \lor q) \land ((\neg p \land \neg q) \lor x_2) \\ &\equiv (\neg x_2 \lor p \lor q) \land (\neg p \lor x_2) \land (\neg q \lor x_2) \end{align} </math>

Man beachte, dass im letzten Schritt wieder das Distributivgesetz angewandt wurde, aber in diesem Schritt gibt es nur noch einen konstanten Zuwachs von Konjunktionen.

Am Ende wird diese Transformation auf allen Konjunkten angewandt und die resultierende KNF ist erfüllbarkeitsäquivalent zur Ausgangsformel und hat im Allgemeinen weniger Klauseln. Es kann vorkommen, dass dies für kleinere Formeln nicht gilt.

Da die Variable, die für die ursprüngliche Formel steht, (hier: <math>x_4</math>) Teil der konstruierten Formel ist, gilt trivialerweise <math>T(\phi) \models \phi</math>. Umgekehrt lässt sich jedes Modell <math> \alpha</math> von <math>\phi</math> so erweitern, dass es ebenfalls ein Modell von <math>T(\phi) </math> ist. Hierzu werden die eingeführten Variablen (hier: <math> x_i </math>) jeweils so gesetzt, dass sie unter der Interpretation <math> \alpha</math> die geforderte Äquivalenz erfüllen.

Somit ist <math>T(\phi)</math> genau dann erfüllbar, wenn <math>\phi</math> erfüllbar ist, und jede erfüllende Belegung von <math>T(\phi)</math> ist ebenfalls eine erfüllende Belegung von <math>\phi</math>. Dies ist von Vorteil, da <math>T(\phi)</math> weniger Klauseln hat und sich deshalb einfacher eine erfüllende Belegung finden lässt als auf der ursprünglichen Formel.

Erweiterung nach Plaisted und Greenbaum

Diese Erweiterung zum klassischen Zeitin-Verfahren benutzt das Konzept der Polarität (N. V. Murray, 1982)<ref>N. V. Murray: Completely Non-Clausal Theorem Proving. In: Artificial Intelligence. Band 18, 1982, S. 67–85. </ref> als wesentlichen Bestandteil.

Polarität

Polarität bezeichnet die Parität der Anzahl der Negationen im Syntaxbaum einer aussagenlogischen Formel vom Wurzelknoten bis zum gewünschten Knoten. Demnach hat ein Knoten, welcher eine ungerade Anzahl an Negationen vom Wurzelsymbol zu ihm besitzt, eine negative Polarität (entsprechend für gerade Anzahl an Negationen und positive Polarität).

Bei der Erweiterung nach Plaisted und Greenbaum gibt es zwei wesentliche Unterschiede zur normalen Zeitin-Transformation:

Die Polarität einer Teilformel hat keine Auswirkung auf die Einführung neuer Variablen.
Anstatt der Biimplikation, wird bei jeder neuen Variable eine Implikation eingeführt.

Die Richtung der eingeführten Implikation hängt von der Polarität ab:

Bei einer Teilformel <math>p \land q</math> mit positiver Polarität wird die neue Variable <math>x</math> wie folgt eingeführt:

<math>

\begin{align} x \rightarrow (p \land q) \end{align} </math>

Dieselbe Teilformel wird bei negativer Polarität so ersetzt:

<math>

\begin{align} (p \land q) \rightarrow x \end{align} </math>

Im Allgemeinen bewirken diese beiden Änderungen, dass die resultierende KNF kleiner als bei der Zeitin-Transformation ist, so lange nicht alle Teilformeln in beiden Polaritäten vorkommen.

Spätere Forschungsarbeiten^[Quelle?] beschäftigen sich mit Heuristiken für die geeignete Einführung neuer Variablen, so dass nicht jede Subformel zu einer Erhöhung der Variablenanzahl führt.

Quellen

G. S. Zeitin: On the complexity of derivation in propositional calculus. Leningrad Seminar on Mathematical Logic, 1970.
D. A. Plaisted, S. Greenbaum: A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation, 1986, doi:10.1016/S0747-7171(86)80028-1

Einzelnachweise