Überblick

Spezifikation:

• Eingabe: eine Formel in CNF
• Ausgabe:
  • eine erfüllende Belegung
  • oder ein Beweis für Nichterfüllbarkeit

Verfahren:

• evolutionär (Genotyp = mathend000# Belegung)
• lokale Suche (Walksat)
• DPLL (Davis, Putnam, Logeman, Loveland)