Erfüllbarkeitsproblem für quantifizierte boolesche Formeln

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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.

Wird die Erfüllbarkeit von booleschen Formeln ohne freie Variablen 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[Bearbeiten | Quelltext bearbeiten]

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[Bearbeiten | Quelltext bearbeiten]

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

  • Jede Aussagenvariable ist eine quantifizierte boolesche Formel. tritt in der Formel frei auf
  • Sind und quantifizierte boolesche Formeln, so auch und . Eine Aussagenvariable aus oder ist frei in den Formeln, falls in oder frei ist.
  • Ist eine quantifizierte boolesche Formel und eine Aussagenvariable, so sind auch und quantifizierte boolesche Formeln. Der Gültigkeitsbereich von beziehungsweise erstreckt sich auf jedes freies Vorkommen von in . Jede andere nicht gebundene Aussagenvariable ist frei in und .

Semantik[Bearbeiten | Quelltext bearbeiten]

Die Semantik quantifizierter boolescher Formeln orientiert sich eng an der Semantik der Prädikatenlogik: Der Wert einer quantifizierten booleschen Formel der Form wird bestimmt, indem durch ersetzt wird, wobei und dadurch entstehen, dass jedes Auftreten von durch 0 beziehungsweise 1 ersetzt wird. Analog dazu wird jedes Aufkommen von durch ersetzt.

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

Pränexe Normalform[Bearbeiten | Quelltext bearbeiten]

Eine quantifizierte boolesche Formel ist in pränexer Normalform, falls sie von der Form ist, wobei und Variablen einer aussagenlogischen Formel ohne Quantoren sind. Der Ausdruck 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[Bearbeiten | Quelltext bearbeiten]

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

für eine aussagenlogische Formel und Quantoren wird der Wert von berechnet, falls keine Quantoren vorhanden sind. Andernfalls wird im Fall der Wert von und im Fall der Wert von berechnet.

Bei einer quantifizierten booleschen Formel mit Quantoren benötigt der Algorithmus also 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[Bearbeiten | Quelltext bearbeiten]

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 die Schreibweise für für eine beliebige Zahl .

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

mit , falls gerade ist und andernfalls

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

mit , falls gerade ist und andernfalls ,

so gilt für alle :

  • ist -vollständig und
  • ist -vollständig.[2]

Einzelnachweise und Quellen[Bearbeiten | Quelltext bearbeiten]

  1. 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.
  2. Larry J. Stockmeyer. The polynomial-time hierarchy. In: Theoretical Computer Science, Bd 3 (1976), Heft 1, S. 1–22, ISSN 0304-3979.