SAT als IP

gesucht ist Funktion T : CNF→IP mit

• T ist in Polynomialzeit berechenbar
• ∀F∈CNF : F erfüllbar$\iff$T(F) lösbar

Lösungsidee:

• Variablen von T(F) = Variablen von F
• Wertebereich der Variablen ist {0, 1}
• Negation durch Subtraktion, Oder durch Addition, Wahrheit durch ≥1