Erfüllbarkeitsproblem für quantifizierte boolesche Formeln

Erfüllbarkeitsproblem für quantifizierte boolesche Formeln

In der Komplexitätstheorie ist das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln (oft nur kurz QBF oder QSAT) eine Verallgemeinerung des Erfüllbarkeitsproblems der Aussagenlogik. Es untersucht, ob eine mit Quantoren versehene aussagenlogische Formel erfüllbar oder wahr ist. Es ist das kanonische PSPACE-vollständige Problem.

Inhaltsverzeichnis

Quantifizierte boolesche Formeln

Jede aussagenlogische Formel kann durch Hinzufügen von All- und Existenzquantoren erweitert werden. Die Semantik einer so gebildeten Formel ähnelt der Semantik prädikatenlogischer Formeln.

Syntax

Die Menge der quantifizierten boolescher Formeln kann wie folgt induktiv definiert werden:

  • Jede Aussagenvariable x ist eine quantifizierte boolesche Formel. x tritt in der Formel x frei auf
  • Sind φ und ψ quantifizierte boolesche Formeln, so auch \neg\varphi, (\varphi\wedge\psi) und (\varphi\vee\psi). Eine Aussagenvariable x aus φ oder ψ ist frei in den Formeln, falls x in φ oder ψ frei ist.
  • Ist φ eine quantifizierte boolesche Formel und x eine Aussagenvariable, so sind auch \forall x\varphi und \exists x\varphi quantifizierte boolesche Formeln. Der Gültigkeitsbereich von \forall x beziehungsweise \exists x erstreckt sich auf jedes freies Vorkommen von x in φ. Jede andere nicht gebundene Aussagenvariable ist frei in \forall x\varphi und \exists x\varphi.

Semantik

Die Semantik quantifizierter boolescher Formeln orientiert sich eng an der Semantik der Prädikatenlogik: Der Wert einer quantifizierten booleschen Formel der Form \forall x\varphi wird bestimmt, indem φ durch \varphi_{x=0}\wedge\varphi_{x=1} ersetzt wird, wobei φx = 0 und φx = 1 dadurch entstehen, dass jedes Auftreten von x durch 0 beziehungsweise 1 ersetzt wird. Analog dazu wird jedes Aufkommen von \exists x\varphi durch \varphi_{x=0}\vee \varphi_{x=1} ersetzt.

Eine Formel, die keine freie Variablen enthält, ist damit entweder wahr oder falsch.

Pränexe Normalform

Eine quantifizierte boolesche Formel ist in pränexer Normalform, falls sie von der Form Q_1 x_1 Q_2 x_2\ldots Q_n x_n \varphi ist, wobei Q_1,\ldots,Q_n\in\{\forall,\exists\} und x_1,\ldots,x_n Variablen einer aussagenlogischen Formel φ ohne Quantoren sind. Der Ausdruck Q_1x_1\ldots Q_nx_n heißt Quantorenblock.

Da für jede quantifizierte boolesche Formel eine äquivalente Formel in pränexer Normalform existiert und diese in Polynomialzeit konstruiert werden kann, wird häufig in Beweisen von dieser Form ausgegangen.

Das Erfüllbarkeitsproblem

Das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln ist es, zu entscheiden, ob eine gegebene quantifizierte boolesche Formel ohne freie Variablen wahr oder falsch ist.

Aus der Definition der Semantik für quantifizierte boolesche Formeln lässt sich ein einfacher rekursiver Algorithmus ableiten, der das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln in pränexer Normalform löst: Bei Eingabe einer Formel der Form

Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \varphi

für eine aussagenlogische Formel φ und Quantoren Q_1,\ldots,Q_n\in\{\forall,\exists\} wird der Wert von φ berechnet, falls keine Quantoren vorhanden sind. Andernfalls wird im Fall Q_1=\forall der Wert von Q_2x_2\ldots Q_nx_n(\varphi_{x_1=0}\wedge \varphi_{x_1=1}) und im Fall Q_1=\exist der Wert von Q_2x_2\ldots Q_nx_n(\varphi_{x_1=0}\vee\varphi_{x_1=1}) berechnet.

Bei einer quantifizierten booleschen Formel mit n Quantoren benötigt der Algorithmus also O(2n) Schritte. Allerdings ist der benötigte Speicherplatz quadratisch in der Länge der Formel, das Problem liegt also in PSPACE. Weiterhin konnte gezeigt werden, dass das Entscheidungsproblem PSPACE-schwer ist.[1] Dieses Problem ist damit vollständig für die Klasse PSPACE.

Quantorenwechsel und Polynomialzeithierarchie

Aus der Struktur des Quantorenblocks einer quantifizierten booleschen Formel in Präfix-Normalform lassen sich Rückschlüsse auf komplexitätstheoretische Eigenschaften ziehen. Die Klassen der wahren quantifizierten booleschen Formeln in Präfix-Normalform sind je nach Anzahl der Alternationen von All- und Existenzquantoren und deren Reihenfolge vollständig für eine Stufe der Polynomialzeithierarchie. Im folgenden ist für einen Quantor Q\in\{\forall,\exists\} QXi die Schreibweise für Qxi1,Qxi2,...,Qxik für eine beliebige Zahl k.

Ist Σk die Klasse aller wahren quantifizierten booleschen Formeln ohne freie Variablen der Form

\exists X_1\forall X_2\exists X_3,\ldots,Q_kX_k mit Q_k=\forall, falls k gerade ist und andernfalls Q_k=\exists

und Πk die Klasse aller wahren quantifizierten booleschen Formeln ohne freie Variablen der Form

\forall X_1\exists X_2\forall X_3,\ldots,Q_kX_k mit Q_k=\exists, falls k gerade ist und andernfalls Q_k=\forall,

so gilt für alle k\geq 0:

  • Σk ist \Sigma_{k}^{\rm{P}}-vollständig und
  • Πk ist \Pi_{k}^{\rm{P}}-vollständig.[2]

Einzelnachweise und Quellen

  1. Michael R. Garey, David S. Johnson: Computers and intractability: a guide to the theory of NP-completeness. San Francisco, 1979
  2. Larry J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3(1):1–22, Okt. 1976.

Wikimedia Foundation.

Игры ⚽ Нужен реферат?

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

  • Quantifizierte boolesche Formel — In der Komplexitätstheorie ist das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln (oft nur kurz QBF oder QSAT) eine Verallgemeinerung des Erfüllbarkeitsproblems der Aussagenlogik. Es untersucht, ob eine mit Quantoren versehene… …   Deutsch Wikipedia

  • QBF — In der Komplexitätstheorie ist das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln (oft nur kurz QBF oder QSAT) eine Verallgemeinerung des Erfüllbarkeitsproblems der Aussagenlogik. Es untersucht, ob eine mit Quantoren versehene… …   Deutsch Wikipedia

  • QSAT — In der Komplexitätstheorie ist das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln (oft nur kurz QBF oder QSAT) eine Verallgemeinerung des Erfüllbarkeitsproblems der Aussagenlogik. Es untersucht, ob eine mit Quantoren versehene… …   Deutsch Wikipedia

  • NPSPACE — In der Komplexitätstheorie bezeichnet PSPACE die Klasse der Entscheidungsprobleme, die von deterministischen Turingmaschinen mit polynomiellem Platz entschieden werden können. Nach dem Satz von Savitch ist PSPACE gleich der Klasse NPSPACE, der… …   Deutsch Wikipedia

  • PSPACE-Vollständigkeit — In der Komplexitätstheorie bezeichnet PSPACE die Klasse der Entscheidungsprobleme, die von deterministischen Turingmaschinen mit polynomiellem Platz entschieden werden können. Nach dem Satz von Savitch ist PSPACE gleich der Klasse NPSPACE, der… …   Deutsch Wikipedia

  • PSPACE — In der Komplexitätstheorie bezeichnet PSPACE die Klasse der Entscheidungsprobleme, die von deterministischen Turingmaschinen mit polynomiellem Platz entschieden werden können. Nach dem Satz von Savitch ist PSPACE gleich der Klasse NPSPACE, der… …   Deutsch Wikipedia

Share the article and excerpts

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