Modellierung durch SAT

gesucht ist Kanten-2-Färbung des K₅ mathend000# ohne einfarbigen K₃ mathend000#.

• Aussagenvariablen f_{i, j} = mathend000# Kante (i, j) mathend000# ist rot (sonst blau).

• Constraints:

  ∀p : ∀q : ∀r : (p < q∧q < r)⇒((f_{p, q}∨f_{q, r}∨f_{p, r})∧...) mathend000#

das ist ein Beispiel für ein Ramsey-Problem

(F. P. Ramsey, 1903-1930) http://www-groups.dcs.st-and.ac.uk/~history/Biographies/Ramsey.html

diese sind schwer, z. B. ist bis heute unbekannt: gibt es eine Kanten-2-Färbung des K₄₃ mathend000# ohne einfarbigen K₅ mathend000#?

http://www1.combinatorics.org/Surveys/ds1/sur.pdf