imported>Rosenfalter: Tippfehler

2024-12-28T13:52:46Z

Tippfehler

Neue Seite

Das '''Erfüllbarkeitsproblem für quantifizierte boolesche Formeln''' ist eine Verallgemeinerung des [[Erfüllbarkeitsproblem der Aussagenlogik|Erfüllbarkeitsproblems der Aussagenlogik]]. Es gehört zur [[Komplexitätstheorie]] und wird oft nur kurz '''QBF''' oder '''QSAT''' genannt. Dieses [[Entscheidungsproblem]] untersucht, ob eine [[Aussagenlogik|aussagenlogische]] [[logische Formel|Formel]], die mit [[Quantor]]en versehen ist, [[erfüllbar]] oder [[Wahrheitswert|''wahr'']] ist.

QBF ist das kanonische [[PSPACE]]-[[Vollständigkeit (Komplexitätstheorie)|vollständige]] Problem (also das klassische Beispiel eines PSPACE-vollständigen Problems).

Wird die Erfüllbarkeit von booleschen Formeln ohne [[freie Variable]] betrachtet, ist Erfüllbarkeit äquivalent zu Wahrheit. Das so entstehende Problem '''True Quantified Boolean Formula''', kurz '''TQBF''', ist ebenfalls PSPACE-vollständig.

== Quantifizierte boolesche Formeln ==

Jede aussagenlogische Formel kann durch Hinzufügen von All- und Existenzquantoren erweitert werden. Die [[Semantik (Logik)|Semantik]] einer so gebildeten Formel ähnelt der Semantik [[Prädikatenlogik|prädikatenlogischer Formeln]].

=== Syntax ===
Die Menge der quantifizierten booleschen Formeln kann wie folgt induktiv definiert werden:
* Jede [[Aussagenvariable]] <math>x</math> ist eine quantifizierte boolesche Formel. <math>x</math> tritt in der Formel <math>x</math> ''frei'' auf.
* Sind <math>\varphi</math> und <math>\psi</math> quantifizierte boolesche Formeln, so auch <math>\neg\varphi, (\varphi\wedge\psi)</math> und <math>(\varphi\vee\psi)</math>. Eine Aussagenvariable <math>x</math> aus <math>\varphi</math> oder <math>\psi</math> ist frei in den Formeln, falls <math>x</math> in <math>\varphi</math> oder <math>\psi</math> frei ist.
* Ist <math>\varphi</math> eine quantifizierte boolesche Formel und <math>x</math> eine Aussagenvariable, so sind auch <math>\forall x\varphi</math> und <math>\exists x\varphi</math> quantifizierte boolesche Formeln. Der Gültigkeitsbereich von <math>\forall x</math> beziehungsweise <math>\exists x</math> erstreckt sich auf jedes freies Vorkommen von <math>x</math> in <math>\varphi</math>. Jede andere nicht gebundene Aussagenvariable ist frei in <math>\forall x\varphi</math> und <math>\exists x\varphi</math>.

=== Semantik ===

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

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

=== Pränexe Normalform ===
{{Hauptartikel|Pränexform}}

Eine quantifizierte boolesche Formel ist in ''pränexer [[Normalform]]'', falls sie von der Form <math>Q_1 x_1 Q_2 x_2\ldots Q_n x_n \varphi</math> ist, wobei <math>Q_1,\ldots,Q_n\in\{\forall,\exists\}</math> und <math>x_1,\ldots,x_n</math> Variablen einer aussagenlogischen Formel <math>\varphi</math> ohne Quantoren sind. Der Ausdruck <math>Q_1x_1\ldots Q_nx_n</math> 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 [[entscheidbar|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 [[rekursiv]]er [[Algorithmus]] ableiten, der das Erfüllbarkeitsproblem für quantifizierte boolesche Formeln in pränexer Normalform löst: Bei Eingabe einer Formel der Form

:<math>Q_1 x_1 Q_2 x_2 \cdots Q_n x_n \varphi</math>

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

Bei einer quantifizierten booleschen Formel mit <math>n</math> Quantoren benötigt der Algorithmus also <math>O(2^n)</math> [[Laufzeit (Informatik)|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.<ref>Michael R. Garey, [[David Stifler Johnson]]: ''Computers and intractability. A guide to the theory of NP-completeness''. 24. Pr. Freeman Press, New York 2003, ISBN 0-7167-1044-7.</ref> 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 <math>Q\in\{\forall,\exists\}</math> <math>Q X_i</math> die Schreibweise für <math>Q x_{i1},Q x_{i2},...,Q x_{ik}</math> für eine beliebige Zahl <math>k</math>.

Ist <math>\Sigma_k</math> die Klasse aller wahren quantifizierten booleschen Formeln ohne freie Variablen der Form
: <math>\exists X_1\forall X_2\exists X_3,\ldots,Q_kX_k</math> mit <math>Q_k=\forall</math>, falls <math>k</math> gerade ist und andernfalls <math>Q_k=\exists</math>
und <math>\Pi_k</math> die Klasse aller wahren quantifizierten booleschen Formeln ohne freie Variablen der Form
: <math>\forall X_1\exists X_2\forall X_3,\ldots,Q_kX_k</math> mit <math>Q_k=\exists</math>, falls <math>k</math> gerade ist und andernfalls <math>Q_k=\forall</math>,

so gilt für alle <math>k\geq 0</math>:

* <math>\Sigma_k</math> ist <math>\Sigma_{k}^{\rm{P}}</math>-vollständig und
* <math>\Pi_k</math> ist <math>\Pi_{k}^{\rm{P}}</math>-vollständig.<ref>Larry J. Stockmeyer: ''The polynomial-time hierarchy''. In: ''Theoretical Computer Science'', Band 3, 1976, Heft 1, S. 1–22, {{ISSN|0304-3975}}.</ref>

== Einzelnachweise und Quellen ==
<references />

{{SORTIERUNG:Erfullbarkeitsproblem fur quantifizierte boolesche Formeln}}
[[Kategorie:Komplexitätstheorie]]
[[Kategorie:Mathematische Logik]]

Erfüllbarkeitsproblem für quantifizierte boolesche Formeln - Versionsgeschichte

imported>Rosenfalter: Tippfehler