SAT-Kodierungen

Weil SAT NP-vollständig ist (Ü: Definition) kann man jedes Problem aus NP nach SAT übersetzen,

d.h. in Polynomialzeit eine Formel konstruieren, die genau dann erfüllbar ist, wenn das Problem eine Lösung hat -- und man kann aus der erfüllenden Belegung eine Lösung rekonstruieren.

Beispiele:

• Independent Set (Schach: n-Damen-Problem)
• Vertex Cover (Variante n-Damen-Problem)
• Hamiltonkreis (Schach: Rösselsprung)