\begin{slide}{Suche nach symmetrischen Lösungen}

falls ein Problem zu groß für den Solver ist:
\begin{itemize}
\item weitere Constraints hinzufügen \dots
\item die effektiv die Anzahl der Variablen verkleinern.
\item d. h.: nur nach symmetrischen Lösungen suchen.
\end{itemize}

Def (allgemein): $f$ ist Symmetrie von $M$,
falls $f(M)\sim M$.

Beispiel: rotationssymmetrische Aufstellungen von Figuren
auf Schachbrett (Vertex Cover, Hamiltonkreis).

\end{slide}

\begin{slide}{Neue Schranke für Van der Waerdens Funktion}

$W(r,k) = $ die größte Zahl $n$, für die es eine $r$-Färbung
von $[1,2,\dots,n]$ gibt ohne einfarbige arithmetische Folge.

Satz (überhaupt nicht trivial): alle diese Zahlen sind endlich.

Einige Schranken erst vor kurzer Zeit verbessert, durch SAT-Kodierung,
siehe Heule, M. J. H:
\emph{Improving the Odds: New Lower Bounds for Van der Waerden Numbers.} 
March 4, 2008.
\url{http://www.st.ewi.tudelft.nl/sat/slides/waerden.pdf}


\end{slide}
