\begin{slide}{SAT-Kodierungen}

Weil SAT NP-vollständig ist (Ü: Definition)
kann man jedes Problem aus NP 
nach SAT übersetzen,

d.h. in Polynomialzeit eine Formel konstruieren,
die genau dann erfüllbar ist, wenn das Problem
eine Lösung hat --- und man kann aus der erfüllenden
Belegung eine Lösung rekonstruieren.

Beispiele:
\begin{itemize}\itemsep 0pt
\item Independent Set (Schach: $n$-Damen-Problem)
\item Vertex Cover (Variante $n$-Damen-Problem)
\item Hamiltonkreis (Schach: Rösselsprung)
\end{itemize}

\end{slide}

\begin{slide}{SAT-Kodierung: Independent Set}
  Def: Graph $G=(V,E)$, Menge $M\subseteq V$ heißt unabhängig,
  falls $\forall x,y\in M: xy\notin E$.
  
  Entscheidungsproblem: 
  \begin{itemize}
  \item Eingabe: $(G, k)$
  \item Frage: existiert unabhängige Menge $M$ in $G$ mit $|M|\ge k$?
  \end{itemize}

  Optimierungsproblem:
  \begin{itemize}
  \item Eingabe: $G$
  \item Ausgabe: möglichst große unabhängige Menge in $G$
  \end{itemize}

  Ist das Optimierungsproblem schwieriger
  (aufwendiger)
  als das Entscheidungsproblem? (Hier: nein.)
\end{slide}

\newcommand{\countEQ}[1]{\operatorname{count}_{={#1}}}
\newcommand{\countLE}[1]{\operatorname{count}_{\le{#1}}}
\newcommand{\countGE}[1]{\operatorname{count}_{\ge{#1}}}

\begin{slide}{SAT-Kodierung: Anzahl-Constraints}

$\countGE{k}(p_1,\ldots,p_n) =$ wenigstens $k$ der $n$ Variablen sind wahr.

\begin{itemize}\itemsep 0pt
\item 
  Fallunterscheidung nach der ersten Variable:
\begin{alignat*}{2}
 & \countGE{k+1}(p_1,p_2,\ldots,p_n) \\
  = & p_1 \wedge \countGE{k}(p_2,\ldots,p_n) \vee
  \countGE{k+1}(p_2,\ldots,p_n).
\end{alignat*}
\item Induktionsanfänge?
\item Implementierung mit Hilfsvariablen für jeden Teilausdruck
  (entspricht Tseitin-Transformation),
  insgesamt $k\cdot n$ viele.
\end{itemize}

(Übung: definiere $\countEQ{k}, \countLE{k}$)

Anwendung: größte unabh. Menge von Springern?
\end{slide}

\begin{slide}{SAT-Kodierung: Vertex Cover}
  \begin{itemize}
  \item 
  Def: Graph $G=(V,E)$, 

  Menge $M\subseteq V$ heißt Knotenüberdeckung,

  falls $\forall x\in V\setminus M:\exists y\in M: xy\in E$.
\item
  Entscheidungsproblem: $(G,k)$, Frage: \dots $|M| \le k$
\item
  \glqq Anwendung\grqq: 
  kleinstes Vertex Cover von Damen auf Schachbrett
\item
  Anwendung: 
  Plazierung von Versorgungs- oder
  Überwachungsknoten in einem Netzwerk
  \end{itemize}
\end{slide}

\begin{slide}{SAT-Kodierung: Hamiltonkreis}
  \begin{itemize}
  \item 
  Def: Graph $G=(V,E)$ mit $V=\{v_1,\ldots,v_n\}$,

  Permutation $\pi:\{1,\ldots,n\}\to\{1,\ldots,n\}$
  bestimmt Hamiltonkreis, wenn 
  und  $v_{\pi(1)} v_{\pi(2)} \in E, \ldots, 
  v_{\pi(n-1)} v_{\pi(n)} \in E, v_{\pi(n)} v_{\pi(1)} \in E$.

\item
  SAT-Kodierung: benutzt Variablen $p(i,j) \leftrightarrow \pi(i)=j$.

  Welche Constraints sind dafür nötig?
\item
  Anwendung: Rösselsprung auf Schachbrett
  \end{itemize}
\end{slide}

\begin{slide}{SAT-Kodierung: Färbung von Graphen}
  \begin{itemize}\itemsep 0pt
  \item 
    Knotenfärbung

    Übung: Definiere \emph{chromatische Zahl} $\chi(G)$ 

    Übung: welche Aussage kann man (mit polynomiellem
    Aufwand in $|G|$ und $c$) SAT-kodieren, 
    welche nicht:

    $\chi(G)\le c, \chi(G)\ge c$
  \item 
    Kantenfärbung (Ramsey-Probleme)

    Def: $R(s_1,\ldots,s_c):= \min \{ n \mid$
    jede Kanten-$c$-Färbung des $K_n$
    enthält einen $K_{s_1}$ der Farbe $1$
    oder \dots oder
    einen $K_{s_c}$ der Farbe $c$ $\}$.

    Ü: beweise mittels SAT-Kodierung:
    $R(4,4)\ge 18$, $R(3,3,3)\ge 17$
    (und Gleichheit durch Nachdenken)

  \end{itemize}
\end{slide}
