\begin{slide}{DPLL: Heuristiken, Modifikationen}

  \begin{itemize}
  \item Wahl der nächsten Entscheidungsvariablen

    (am häufigsten in aktuellen Konflikten)
  \item Lernen von Konflikt-Klauseln 
    (erlaubt Backjump)

  \item Vorverarbeitung (Variablen und Klauseln eliminieren) 

  \end{itemize}

alles vorbildlich implementiert und dokumentiert in
Minisat \url{http://minisat.se/} 
(seit ca. 2005 sehr starker Solver)

\end{slide}
