\begin{slide}{Quantifizierte Boolesche Formeln}

\emph{Syntax}: eine QBF hat die Form 
$\underbrace{Q_1 v_1 \ldots Q_n v_n }_{\text{Präfix}} \underbrace{M}_{\text{Matrix}}$,

wobei $Q_1,\ldots,Q_n\in\{\forall,\exists\}$
und $M$ eine aussagenlogische Formel ist
(die die Variablen $v_1,\ldots,v_n$ enthalten kann)

\bigskip

\emph{Semantik}: $\val(M) = \val(M,\emptyset)$ mit

$\val(\forall x M, b)=\val(M,b\cup\{(x,0)\}) \wedge \val(M,b\cup\{(x,1)\})$

$\val(\exists x M, b)=\val(M,b\cup\{(x,0)\}) \vee \val(M,b\cup\{(x,1)\})$

\end{slide}


\begin{slide}{QBF-Beispiele mit fester Quantortiefe}

  \begin{itemize}
  \item chromatische Zahl
  \item kleinstes Vertex Cover
  \item minimales Sudoku
  \item kleinster Schaltkreis
  \item \dots
  \end{itemize}

Schema: $\exists z : P(z) \wedge \forall z': z'<z \Rightarrow \neg P(z')$ 


\end{slide}


\begin{slide}{Zweipersonenspiele}  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Satz: PSPACE $=$ APTIME (alternierend)

Anwendung (Projekt!): Zweipersonenspiele (mit polynomieller Länge)

$\exists s_1 \forall w_2 \dots \forall w_n:$ 
$(s_1,w_2,\ldots,w_n)$ ist gültige Zugfolge und Resultat ist verloren für Weiß.

\end{slide}

\begin{slide}{Komplexität} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Dieses Problem QBF-SAT ist PSPACE-vollständig:
  \begin{itemize}
  \item Eingabe: eine QBF $F$
  \item Frage: ist $\val(F)=1$
  \end{itemize}

Bemerkung: $\text{QBF} \in \text{PSPACE}$ (alle Belegungen durchprobieren).

\emph{Aufgabe:} es ist ein (Polynomialzeit-)Verfahren anzugeben,
das zu jeder polynomiell platzbeschränkten Maschine $M$
und Eingabewort $w$ eine QBF $F$ konstruiert, so daß
$w \to_M^*$ \verb|OK|  $\iff$ $\models F$.

\emph{Problem:} $F$ darf nur polynomiell groß sein,
die Rechnungen von $M$ können aber exponentiell lang sein!

\end{slide}

\begin{slide}{Lösung}

Beweis: kodiere $F_k(p,q) \iff p \to^{\leq 2^k} q$,
es gibt einen Pfad der Länge $\leq 2^k$ von $p$ nach $q$,
durch QBF der Größe $O(k)$.

$F_0(p,q) := (p=q) \vee (p\to^1 q)$

$F_{k+1} (p,q) := $ 
$\exists m \forall x \forall y 
(((x=p\wedge y=m) \vee (x=m \wedge y=q)) \Rightarrow F_k(x,y))$

\bigskip


Anwendung (Projekte!): (lange) Ableitungen (Schleifen) 
in  längenerhaltenden Ersetzungssystemen,
in Verschiebepuzzles (Lunar Lockout, Sokoban,\ldots)


\end{slide}

\begin{slide}{Satz von Savitch}

Satz (Savitch): NPSPACE($f$) $\subseteq$ DPSPACE($f^2$).


(N: nichtdeterministisch, D: deterministisch)


Beweis: für $M \in \text{NPSPACE}$ konstruiere Formel $F$
wie vorhin (Größe?)

dann teste $F\in\text{QBF-SAT}$ mit einer DPSPACE-Maschine.

\end{slide}


