Erfüllbarkeitsäquivalenz
aus Wikipedia, der freien Enzyklopädie
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
G ist erfüllbar
Oder umgekehrt:
- F ist unerfüllbar G ist unerfüllbar
Die beiden Formeln brauchen nicht äquivalent zu sein und brauchen auch nicht durch die selben 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.
[Bearbeiten] Beispiel
X und 
X sind erfüllbarkeitsäquivalent, aber nicht äquivalent.
[Bearbeiten] Umformung in erfüllbarkeitsäquivalente 3-KNF Formel
Zu jeder Formel in m-KNF, d.h. der Form 
mit 
also höchstens m Literalen pro Konjunktion, kann in Polynomialzeit eine erfüllbarkeitsäquivalente Formel in 3-KNF konstuiert werden.
Sei dazu 
mit 
. Solange Ψ noch eine Klausel 
besitzt, ersetze dieses Ci durch 
mit
X ist dabei eine neue Variable. Jede Interpretation, die C'i und C''i erfüllt, erfüllt auch Ci. Jede Interpretation, die Ci erfüllt, kann zu einer Interpretation, welche C'i und C''i erfüllt umgeformt werden.
