Beispiele zur SAT-Modellierung

• Hausaufgabe (leicht): N-Damen-Problem
• Hausaufgabe (schwer): Rösselsprung (= Hamiltonkreis)
• von n Variablen sind genau k wahr (bei Formelgröße ∼n⋅k)
• Puzzles aus Logisch (Dt. Rätselverlag)
• Puzzles von http://www.janko.at/

Vorgehen bei Modellierung:

• welches sind die Variablen, was ist deren Bedeutung?

  (Wie rekonstruiert man eine Lösung aus der Belegung, die der Solver liefert?)

• welches sind die Constraints?
  wie stellt man sie in CNF dar?