Erfüllbarkeitsäquivalenz

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

Erfüllbarkeitsäquivalenz ist eine Eigenschaft, die zwischen zwei prädikatenlogischen Formeln gelten kann.

Zwei Formeln F und G sind genau dann erfüllbarkeitsäquivalent, wenn gilt:

F ist erfüllbar \Leftrightarrow G ist erfüllbar

Oder umgekehrt:

F ist unerfüllbar \Leftrightarrow G ist unerfüllbar

Die beiden Formeln brauchen nicht äquivalent zu sein und brauchen auch nicht durch dieselben Interpretationen erfüllt zu werden. Erfüllbarkeitsäquivalenz ist somit eine recht schwache Eigenschaft.

Relevant ist die Erfüllbarkeitsäquivalenz bei Nachweis der Unerfüllbarkeit einer prädikatenlogischen Formel mittels der Herbrand-Theorie. Dazu muss die Formel erst in die Skolemform umgeformt werden, die zur Ausgangsformel lediglich erfüllbarkeitsäquivalent ist.

Beispiel[Bearbeiten]

Es sei X eine Formel (mit der Bedingung, dass sie weder eine Tautologie noch unerfüllbar ist). Dann sind die Formeln X und \neg X erfüllbarkeitsäquivalent, aber nicht äquivalent.

Umformung in erfüllbarkeitsäquivalente 3-KNF Formel[Bearbeiten]

Zu jeder Formel in m-KNF, d.h. der Form \bigwedge_i \left(Y_{i,1} \vee ... \vee Y_{i,k_i} \right) mit k_i \leq m also höchstens m Literalen pro Disjunktion, kann in Polynomialzeit eine erfüllbarkeitsäquivalente Formel in 3-KNF konstruiert werden.

Sei dazu \Psi = C_1 \wedge ... \wedge C_n mit C_i = Y_{i,1} \vee ... \vee Y_{i,m_i}. Solange \Psi noch eine Klausel m_i \ge 3 besitzt, ersetze dieses C_i durch C_i = C'_i \wedge C''_i mit

C'_i = Y_{i,1} \vee Y_{i,2} \vee X
C''_i = \neg X \vee Y_{i,3} \vee ... \vee Y_{i,m_i}

X ist dabei eine neue Variable. Jede Interpretation, die C'_i und C''_i erfüllt, erfüllt auch C_i. Jede Interpretation, die C_i erfüllt, kann zu einer Interpretation, welche C'_i und C''_i erfüllt umgeformt werden.