Modellierung durch SAT

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

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

• Constraints:

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

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₄₃ ohne einfarbigen K₅?

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