Erfüllbarkeitsäquivalenz

Erfüllbarkeitsäquivalenz

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

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

Erläuterung: Für die Erfüllbarkeit der Formel X muss X wahr (1) sein. Für die Erfüllbarkeit der Formel \negX muss X falsch (0) sein.
Es gibt also jeweils eine erfüllende (aber nicht zwangsweise gleiche) Belegung für beide Formeln.

Umformung in erfüllbarkeitsäquivalente 3-KNF Formel

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 Ψ noch eine Klausel m_i \ge 3 besitzt, ersetze dieses Ci 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 Ci. Jede Interpretation, die Ci erfüllt, kann zu einer Interpretation, welche C'i und C''i erfüllt umgeformt werden.


Wikimedia Foundation.

Игры ⚽ Поможем написать курсовую

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Erfüllbarkeit — ist in der Logik und Mathematik ein metasprachliches Prädikat für die Eigenschaft von logischen Aussagen und Aussageformen. Eine Aussage ist erfüllbar, wenn es eine Belegung (Interpretation, Bewertung) der Variablen gibt, für die der… …   Deutsch Wikipedia

  • Herbrand-Theorie — Der nach Jacques Herbrand, einem französischen Logiker, benannte Satz von Herbrand (engl. Herbrand s theorem, was gelegentlich nicht ganz korrekt als Herbrand Theorie übersetzt wird) in der Prädikatenlogik lautet: Sei F eine geschlossene Formel… …   Deutsch Wikipedia

  • Skolem-Normalform — Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Für Formeln in Skolemform existiert ein berechenbarer Test auf Erfüllbarkeit. Dies ist …   Deutsch Wikipedia

  • Skolemformel — Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Für Formeln in Skolemform existiert ein berechenbarer Test auf Erfüllbarkeit. Dies ist …   Deutsch Wikipedia

  • Skolemisierung — Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Für Formeln in Skolemform existiert ein berechenbarer Test auf Erfüllbarkeit. Dies ist …   Deutsch Wikipedia

  • Skolemnormalform — Skolemform ist ein Begriff der Prädikatenlogik und bezeichnet eine prädikatenlogische Formel, die sich in einer Normalform nach Albert Thoralf Skolem befindet. Für Formeln in Skolemform existiert ein berechenbarer Test auf Erfüllbarkeit. Dies ist …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”