Erfüllbarkeitsäquivalenz

Eigenschaft aus der Prädikatenlogik

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 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   eine Formel (mit der Bedingung, dass sie weder eine Tautologie noch unerfüllbar ist). Dann sind die Formeln   und   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   mit   also höchstens   Literalen pro Disjunktion, kann in Polynomialzeit eine erfüllbarkeitsäquivalente Formel in 3-KNF konstruiert werden.

Sei dazu   mit  . Solange   noch eine Klausel   besitzt, ersetze dieses   durch   mit

 
 

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