Erfüllbarkeitsproblem für quantifizierte boolesche Formeln

(Weitergeleitet von Quantifizierte boolesche Formel)

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

QBF ist das kanonische PSPACE-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

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.

Die Menge der quantifizierten booleschen 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

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

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

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

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
  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, Band 3, 1976, Heft 1, S. 1–22, ISSN 0304-3975.