Satz TQBF ist PSPACE-vollständig

Einfache Sprache

Def. Satz TQBF ist PSPACE-vollständig

TQBF ist PSPACE-vollständig.

Beweisidee: Nach der Definition von PSPACE-Vollständigkeit müssen wir zeigen das $\mathrm{TQBF}$ in PSPACE ist und das alle Sprachen in $\mathbf{PSPACE}$ polynomial reduzierbar auf $\mathrm{TQBF}$ sind.

Ersteres wird gezeigt indem wir einen Algorithmus angeben, der den Variablen werte zuweist und dann rekursiv die Formel vereinfacht. Daraus kann der Algorithmus dann die Erfüllbarkeit der originalen Formel bestimmen.

Um Letzteres zu beweisen, zeigen wir wie man eine beliebige Sprache in $\mathbf{PSPACE}$ auf eine Prädikatenlogische Formel in Polynomialzeit reduziert. Es existiert also ein TM die in polynomiell Raum läuft und $A$ entscheidet. Dann geben wir eine Polynomialzeitreduktion an, die eine Zeichenkette auf eine Prädikatenlogische Formel abbildet, die eine Simulation der der von $A$ auf der Eingabe darstellt. Die Formel ist Wahr gdw. $A$ akzeptiert.

Die Formel kann nicht wie im Satz von Cook und Levin gebaut werden. Denn da $A$ exponentiell lange Laufen kann (Satz Anzahl der Konfiguration einer TM), hätte das Tableau exponentiell viele Zeilen. Aber wir können mit einer Polynomialzeitreduktion keine exponentiell große Ausgabe produzieren.

Also wird eine Technik die dem Ansatz von dem Satz von Savitch ähnelt angewandt. Dazu teilt die Formel das Tableau horizontal in zwei Teile und benutzt Allaussage um beide Hälften mit einer Formel zu repräsentieren. Dadurch wird die Formel entscheidend kleiner.

Beweis: Der Algorihmus $T$, der in polynomischer Platzkomplexität läuft und $\mathrm{TQBF}$ entscheidet, funktioniert wie folgt für die Eingabe $\langle\phi\rangle$, wobei $\phi$ eine voll quantifizierte Prädikatenlogische Formel ist:

1. Falls $\phi$ keine Quantoren enthält, enthält $\phi$ nur Konstanten. $\phi$ kann ausgewertet werden. Falls $\phi$ zu Wahr ausgewertet wird, akzeptiere, sonst verwerfe.
2. Falls $\phi$ die Form $\exists x \psi$ hat, rufe $T$ rekursiv auf $\psi$ auf, wobei einmal $x$ durch Wahr und einmal $x$ durch Falsch ersetzt ist. Falls einer der Aufrufe akzeptiert, akzeptiere, sonst verwerfe.
3. Falls $\phi$ die Form $\forall x\psi$ hat, rufe $T$ rekursiv auf $\psi$ auf, wobei $x$ einmal durch Wahr und einmal Falsch ersetzt ist. Falls beide Aufrufe akzeptieren, akzeptiere, sonst verwerfe.

Es ist offensichtlich das $T$ $\mathrm{TQBF}$ entscheidet. Bleibt zu zeigen das $T$ eine polynomische Platzkomplexität hat. Da in jedem Rekursionsschritt eine Variable gebunden wird, ist die Rekursionstiefe höchstens die Anzahl der Variablen in $\phi$. In jedem Rekursionsschritt wird nur eine Wert für die ersetzte Variable gespeichert. Sei $m$ die Anzahl der Variablen in $\phi$. Dann ist die Platzkomplexität von $T$ $O(m)$. Also linear und daher auch polynomiell.

Jetzt bleibt noch zu zeigen, dass $\mathrm{TQBF}$ PSPACE-Schwere ist. Sei $A$ eine Sprache, die von einer TM $\mathcal M$ in in dem Raum $n^k$, wobei $k$ eine Konstante ist, entschieden wird. Wir geben einen Polynomialzeitreduktion von $A$ nach $\mathrm{TQBF}$.

Die Reduktion bildet eine Zeichenkette $w$ auf eine quantifizierte Prädikatenlogische Formel $\phi$ ab, die wahr ist gdw. $\mathcal M$ $w$ akzeptiert. Um zu zeigen wie $\phi$ konstruiert wird, lösen wir ein generelleres Problem.

Sei $c_1$ und $c_2$ eine Sammlung von Variablen die jeweils eine Konfiguration darstellen und $t\in\mathbb N_{>0}$. Wir konstruieren eine Formel $\phi_{c_1,c_2,t}$, die wahr ist gdw. $\mathcal M$ von $c_1$ zu $c_2$ in höchstens $t$ vielen Schritten gehen kann. Dann können wir $\phi = \phi_{c_\mathrm{start},c_\mathrm{accept},h}$, wobei $h = 2^{df(n)}$. $d$ ist eine Konstante, die gewählt wird so, dass $\mathcal M$ nicht mehr als $2^{df(n)}$ mögliche Konfigurationen hat. $n$ ist die länge der Eingabe. Wir nehmen an das $f(n) = n^k$ und das $t$ eine Zweierpotenz ist.

Die Formel codiert die Konfiguration wie in dem Satz von Cook und Levin. Jede Speicherzelle hat mehrere zugehörige Variablen. Eine für jedes Bandsymbol und Zustand. Also alle möglichen Konfiguration an dieser Stelle. Jede Konfiguration hat $n^k$ Speicherzellen und benötigt damit $O(n^k)$ Variablen.

Jetzt machen wir eine Fallunterscheidung nach $t$. Erst das Rekursionsende mit $t = 1$ und dann für $t>1$.

Sei $t = 1$. Die Formel $\phi_{c_1,c_2,t}$ soll abbilden, dass $c_1$ gleich $c_2$ oder $c_2$ die Folgekonfiguration von $c_1$ ist. Die Gleichheit kann dadurch abgebildet werden das jede Variable in $c_1$ den gleichen Boolescher Wert wie die entsprechend Variable in $c_2$ hat. Also z.B. die Variable die besagt ob an der Stelle $x$ das Symbol $y$ ist und die TM sich im Zustand $z$ befindet, hat in $c_1$ den gleichen Wert wie in $c_2$. Das zeigen der korrekten Folgekonfiguration erfolgt, wie in dem Satz von Cook und Levin, durch eine Formel die für alle Speicherzellen incl. deren Nachbarn (also drei variablen) in $c_1$, die entsprechende Speicherzelle in $c_2$ einen korrekten Wert hat.

Sei t > 1. Wir konstruieren $\phi_{c_1,c_2,t}$ rekursiv ähnlich wie im Satz von Savitch.

Probieren wir zunächst eine Formel, die noch nicht ganz funktioniert: Sei

wobei $m_1$ eine Konfiguration von $\mathcal M$ darstellt. $\exists m_1$ ist eine Abkürzung für $\exists x_1,\ldots,x_l$ mit $l=O(n^k)$ und $x_1,\ldots,x_l$ sind Variablen die $m_1$ codieren. Die Formel besagt also das $\mathcal M$ von $c_1$ nach $c_2$ in höchstens $t$ Schritten kommt, wenn Konfiguration $m_1$ existiert so, dass $\mathcal M$ von $c_1$ nach $m_1$ und von $m_1$ nach $c_2$ in höchstens $\frac{t}{2}$ Schritten kommt. Die Formeln $\phi_{c_1,m_1,\frac{t}{2}}$ und $\phi_{m_1,c_2,\frac{t}{2}}$ werden dann rekursiv erstellt. Die Formel für $\phi_{c_1,c_2,t}$ funktioniert zwar aber sie ist zu groß. Jeder Rekursionsschritt halbiert zwar $t$ aber dafür verdoppelt sich die Größe der Formel. Daher haben wir ein Formel der Größe $O(t)$. Da $t= 2^{df(n)}$ ist die Formel also exponentiell groß.

Beim zweiten Ansatz wird eine zusätzliche Allaussage die Größe reduzieren: Sei

Die Benutzung zweier neuer Variablen $c_3$ und $c_4$ ermöglicht uns die beiden rekursiven Formeln in eine zu “falten”, ohne die Erfüllbarkeit zu verändern. Durch den Allquantor $\forall (c_3,c_4)\in\{(c_1,m_1),(m_1,c_2\}$ wird ausgedrückt, dass $c_3$ und $c_4$ die Werte von $c_1$ und $m_1$ bzw. $m_1$ und $c_2$ annehmen kann. Die resultierende Formel $\phi_{c_3,c_4,\frac{t}{2}}$ muss in beiden Fällen wahr sein. Wir können $\forall x\in\{y,z\}[\ldots]$ durch die äquivalenten Ausdruck $\forall x [(x=y) \lor x = z) \rightarrow \ldots]$ ersetzen, damit wir eine syntaktisch korrekte Prädikatenlogische Formel erhalten. Bemerke das sowohl die Implikation als auch die Äquivalenz durch Negation und Konjunktion dargestellt werden kann. Uns interessiert nun die Größe von $\phi_{c_\mathrm{start},c_\mathrm{accept},h}$, wobei $h = 2^{df(n)}$. Jeder Rekursionsschritt fügt der Formel ein Stück hinzu, dass linear in der Größe der Konfigurationen ist und damit in Größe von $O(f(n))$. Die Rekursionstiefe ist $\log(2^{df(n)})$. Was wiederum in $O(f(n))$ ist. Daher ist die Größe von $\phi$ in $O(f^2(n))$.