www.wikidata.de-de.nina.az

Erfüllbarkeitsproblem für quantifizierte boolesche Formeln Das ist eine Verallgemeinerung des Erfüllbarkeitsproblems der

Erfüllbarkeitsproblem für quantifizierte boolesche Formeln

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.

Syntax Bearbeiten

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. 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

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

so gilt für alle :

  • ist -vollständig und
  • ist -vollständig.

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.
wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Das Erfullbarkeitsproblem fur quantifizierte boolesche Formeln ist eine Verallgemeinerung des Erfullbarkeitsproblems der Aussagenlogik Es gehort zur Komplexitatstheorie und wird oft nur kurz QBF oder QSAT genannt Dieses Entscheidungsproblem untersucht ob eine aussagenlogische Formel die mit Quantoren versehen ist erfullbar oder wahr ist QBF ist das kanonische PSPACE vollstandige Problem also das klassische Beispiel eines PSPACE vollstandigen Problems Wird die Erfullbarkeit von booleschen Formeln ohne freie Variable betrachtet ist Erfullbarkeit aquivalent zu Wahrheit Das so entstehende Problem True Quantified Boolean Formula kurz TQBF ist ebenfalls PSPACE vollstandig Inhaltsverzeichnis 1 Quantifizierte boolesche Formeln 1 1 Syntax 1 2 Semantik 1 3 Pranexe Normalform 2 Das Erfullbarkeitsproblem 2 1 Quantorenwechsel und Polynomialzeithierarchie 3 Einzelnachweise und QuellenQuantifizierte boolesche Formeln BearbeitenJede aussagenlogische Formel kann durch Hinzufugen von All und Existenzquantoren erweitert werden Die Semantik einer so gebildeten Formel ahnelt der Semantik pradikatenlogischer Formeln Syntax Bearbeiten Die Menge der quantifizierten booleschen Formeln kann wie folgt induktiv definiert werden Jede Aussagenvariable x displaystyle x nbsp ist eine quantifizierte boolesche Formel x displaystyle x nbsp tritt in der Formel x displaystyle x nbsp frei auf Sind f displaystyle varphi nbsp und ps displaystyle psi nbsp quantifizierte boolesche Formeln so auch f f ps displaystyle neg varphi varphi wedge psi nbsp und f ps displaystyle varphi vee psi nbsp Eine Aussagenvariable x displaystyle x nbsp aus f displaystyle varphi nbsp oder ps displaystyle psi nbsp ist frei in den Formeln falls x displaystyle x nbsp in f displaystyle varphi nbsp oder ps displaystyle psi nbsp frei ist Ist f displaystyle varphi nbsp eine quantifizierte boolesche Formel und x displaystyle x nbsp eine Aussagenvariable so sind auch x f displaystyle forall x varphi nbsp und x f displaystyle exists x varphi nbsp quantifizierte boolesche Formeln Der Gultigkeitsbereich von x displaystyle forall x nbsp beziehungsweise x displaystyle exists x nbsp erstreckt sich auf jedes freies Vorkommen von x displaystyle x nbsp in f displaystyle varphi nbsp Jede andere nicht gebundene Aussagenvariable ist frei in x f displaystyle forall x varphi nbsp und x f displaystyle exists x varphi nbsp Semantik Bearbeiten Die Semantik quantifizierter boolescher Formeln orientiert sich eng an der Semantik der Pradikatenlogik Der Wert einer quantifizierten booleschen Formel der Form x f displaystyle forall x varphi nbsp wird bestimmt indem f displaystyle varphi nbsp durch f x 0 f x 1 displaystyle varphi x 0 wedge varphi x 1 nbsp ersetzt wird wobei f x 0 displaystyle varphi x 0 nbsp und f x 1 displaystyle varphi x 1 nbsp dadurch entstehen dass jedes Auftreten von x displaystyle x nbsp durch 0 beziehungsweise 1 ersetzt wird Analog dazu wird jedes Aufkommen von x f displaystyle exists x varphi nbsp durch f x 0 f x 1 displaystyle varphi x 0 vee varphi x 1 nbsp ersetzt Eine Formel die keine freie Variablen enthalt ist damit entweder wahr oder falsch Pranexe Normalform Bearbeiten Hauptartikel Pranexform Eine quantifizierte boolesche Formel ist in pranexer Normalform falls sie von der Form Q 1 x 1 Q 2 x 2 Q n x n f displaystyle Q 1 x 1 Q 2 x 2 ldots Q n x n varphi nbsp ist wobei Q 1 Q n displaystyle Q 1 ldots Q n in forall exists nbsp und x 1 x n displaystyle x 1 ldots x n nbsp Variablen einer aussagenlogischen Formel f displaystyle varphi nbsp ohne Quantoren sind Der Ausdruck Q 1 x 1 Q n x n displaystyle Q 1 x 1 ldots Q n x n nbsp heisst Quantorenblock Da fur jede quantifizierte boolesche Formel eine aquivalente Formel in pranexer Normalform existiert und diese in Polynomialzeit konstruiert werden kann wird haufig in Beweisen von dieser Form ausgegangen Das Erfullbarkeitsproblem BearbeitenDas Erfullbarkeitsproblem fur 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 fur quantifizierte boolesche Formeln lasst sich ein einfacher rekursiver Algorithmus ableiten der das Erfullbarkeitsproblem fur quantifizierte boolesche Formeln in pranexer Normalform lost Bei Eingabe einer Formel der Form Q 1 x 1 Q 2 x 2 Q n x n f displaystyle Q 1 x 1 Q 2 x 2 cdots Q n x n varphi nbsp fur eine aussagenlogische Formel f displaystyle varphi nbsp und Quantoren Q 1 Q n displaystyle Q 1 ldots Q n in forall exists nbsp wird der Wert von f displaystyle varphi nbsp berechnet falls keine Quantoren vorhanden sind Andernfalls wird im Fall Q 1 displaystyle Q 1 forall nbsp der Wert von Q 2 x 2 Q n x n f x 1 0 f x 1 1 displaystyle Q 2 x 2 ldots Q n x n varphi x 1 0 wedge varphi x 1 1 nbsp und im Fall Q 1 displaystyle Q 1 exists nbsp der Wert von Q 2 x 2 Q n x n f x 1 0 f x 1 1 displaystyle Q 2 x 2 ldots Q n x n varphi x 1 0 vee varphi x 1 1 nbsp berechnet Bei einer quantifizierten booleschen Formel mit n displaystyle n nbsp Quantoren benotigt der Algorithmus also O 2 n displaystyle O 2 n nbsp Schritte Allerdings ist der benotigte Speicherplatz quadratisch in der Lange der Formel das Problem liegt also in PSPACE Weiterhin konnte gezeigt werden dass das Entscheidungsproblem PSPACE schwer ist 1 Dieses Problem ist damit vollstandig fur die Klasse PSPACE Quantorenwechsel und Polynomialzeithierarchie Bearbeiten Aus der Struktur des Quantorenblocks einer quantifizierten booleschen Formel in Prafix Normalform lassen sich Ruckschlusse auf komplexitatstheoretische Eigenschaften ziehen Die Klassen der wahren quantifizierten booleschen Formeln in Prafix Normalform sind je nach Anzahl der Alternationen von All und Existenzquantoren und deren Reihenfolge vollstandig fur eine Stufe der Polynomialzeithierarchie Im Folgenden ist fur einen Quantor Q displaystyle Q in forall exists nbsp Q X i displaystyle QX i nbsp die Schreibweise fur Q x i 1 Q x i 2 Q x i k displaystyle Qx i1 Qx i2 Qx ik nbsp fur eine beliebige Zahl k displaystyle k nbsp Ist S k displaystyle Sigma k nbsp die Klasse aller wahren quantifizierten booleschen Formeln ohne freie Variablen der Form X 1 X 2 X 3 Q k X k displaystyle exists X 1 forall X 2 exists X 3 ldots Q k X k nbsp mit Q k displaystyle Q k forall nbsp falls k displaystyle k nbsp gerade ist und andernfalls Q k displaystyle Q k exists nbsp und P k displaystyle Pi k nbsp die Klasse aller wahren quantifizierten booleschen Formeln ohne freie Variablen der Form X 1 X 2 X 3 Q k X k displaystyle forall X 1 exists X 2 forall X 3 ldots Q k X k nbsp mit Q k displaystyle Q k exists nbsp falls k displaystyle k nbsp gerade ist und andernfalls Q k displaystyle Q k forall nbsp so gilt fur alle k 0 displaystyle k geq 0 nbsp S k displaystyle Sigma k nbsp ist S k P displaystyle Sigma k rm P nbsp vollstandig und P k displaystyle Pi k nbsp ist P k P displaystyle Pi k rm P nbsp vollstandig 2 Einzelnachweise und Quellen Bearbeiten 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 Larry J Stockmeyer The polynomial time hierarchy In Theoretical Computer Science Band 3 1976 Heft 1 S 1 22 ISSN 0304 3975 Abgerufen von https de wikipedia org w index php title Erfullbarkeitsproblem fur quantifizierte boolesche Formeln amp oldid 221319250