\begin{slide}{Automatische Hilfsvariablen}

im Quelltext: Haskell-Namen (\verb|x|), 
für Solver: Nummern (\verb|1|)

\begin{verbatim}
import Satchmo.Boolean 
import Satchmo.Solve
test :: IO ( Maybe Bool )
test = solve $ do 
    x <- boolean -- Allokation einer Variablen
    assert [ not x ]
    return $ decode x
\end{verbatim}

Realisierung:
  \begin{itemize}\itemsep 0pt\parskip 0pt
\item \verb|boolean :: SAT Boolean| (ist Aktion)
  \item automatisches Weiterzählen
    (StateMonad für Nummer)
  \item WriterMonad für CNF (Klauseln)
  \item ReaderMonad für Resultat (Belegung)
  \end{itemize}

\end{slide}

\begin{slide}{Realisierung logischer Funktionen}
\begin{verbatim}
and :: [ Boolean ] -> SAT Boolean
and xs = do
  y <- boolean -- Hilfsvariable lt. Tseitin
  forM xs $ \ x -> do
      assert [ not y, x ]
  assert $ y : map not xs
  return y
\end{verbatim}
  
Übung:
\begin{itemize}\itemsep 0pt
\item Typ von \verb|forM| (benutze 
\verb|:i forM| in \verb|ghci|
oder \url{http://haskell.org/hoogle/})
\item  \verb|or|
\item \verb|xor|  (Anzahl der \verb|True| ist ungerade)
\end{itemize}


\end{slide}
