SAT als IP

gesucht ist Funktion T : CNF→IP mathend000# mit

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

Lösungsidee:

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