\begin{slide}{Modellierung durch SAT}

gesucht ist Kanten-2-Färbung des $K_5$
ohne einfarbigen $K_3$.

\begin{itemize}\itemsep 0pt
\item 
Aussagenvariablen $f_{i,j} =$ Kante $(i,j)$ ist rot (sonst blau).

\item
Constraints:
  
$\forall p: \forall q: \forall r:
(p<q \wedge q<r) \Rightarrow
( (f_{p,q}\vee f_{q,r} \vee f_{p,r}) \wedge \dots)$
\end{itemize}

das ist ein Beispiel für ein Ramsey-Problem

(F. P. Ramsey, 1903--1930)
\url{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_{43}$ ohne einfarbigen $K_{5}$?

\url{http://www1.combinatorics.org/Surveys/ds1/sur.pdf}


\end{slide}
