Beispiele zur SAT-Modellierung

• Hausaufgabe (leicht): N mathend000#-Damen-Problem
• Hausaufgabe (schwer): Rösselsprung (= mathend000# Hamiltonkreis)
• von n mathend000# Variablen sind genau k mathend000# wahr (bei Formelgröße ∼n⋅k mathend000#)
• 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?