DPLL: Heuristiken, Modifikationen

• Wahl der nächsten Entscheidungsvariablen

  (am häufigsten in aktuellen Konflikten)

• Lernen von Konflikt-Klauseln (erlaubt Backjump)

• Vorverarbeitung (Variablen und Klauseln eliminieren)

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