CNF-SAT als FD-Constraint-Problem

• Universum U = {0, 1}
• Funktion N(x) : = (1 - x),
• Relation O(x₁,…, x_k) = (x₁ + … + x_k≥1)

übersetze CNF (p∨¬q)∧(q∨r)

in äquivalentes FD-Problem O(p, N(q))∧O(q, r)

• FD-Constraint-Lösen ist wenigstens so schwer wie SAT-Lösen (also NP-vollständig)
• Algorithmen sind auch ähnlich (zu DPLL), Unterschiede:
  • SAT: CDCL
  • FD: Verfeinerung des Konzeptes Konflikt