\begin{slide}{Schwierige Fälle für die SAT-Kodierung}

  \begin{itemize}
  \item 
wenn das Problem nicht in NP ist,
dann hat es keine polynomiell große Kodierung.
\item
wahrscheinliche Beispiele:
Suchprobleme mit (exponentiell) tiefen Bäumen,
z. B. Verschiebepuzzles 
(Rushhour, Atomix, Lunar Lockout (?))
\item
Markus Holzer, Stefan Schwoon: 
\emph{Assembling Molecules in Atomix in Hard},
TCS 2003, \url{http://dblp.uni-trier.de/rec/bibtex/journals/tcs/HolzerS04}
\item PSPACE-hardness ist offen für Lunar Lockout
  \end{itemize}



\end{slide}
