\documentclass[a4paper]{article}
\usepackage{entete}
\author{Langages Formels. Calculabilité et complexité. \\Olivier~\textsc{Carton}}
\title{Théorème de Cook}
\date{2011-2012}

\begin{document}
\maketitle

\begin{thm}[de Cook, 1971]
    Le problème \textsc{Sat} est NP-complet.
\end{thm}

\begin{proof}
    Soit $A$ un problème de NP, et soit $\mathcal M$ une machine de Turing non-déterministe qui décide $A$ en temps polynomial.

    Pour chaque entrée $w$, on va construire une formule $\varphi_w$ qui sera satisfiable {\em si et seulement si} $\mathcal M$ accepte $w$.

    On note $n=|w|$. On peut supposer que chaque calcul acceptant sur $w$ est de longueur exactement $n^k$ (quitte à rajouter des transitions inutiles).

    La machine utilise donc au plus $n^k$ cellules de sa bande de travail, et donc les configurations sont de longueur au plus $n^k$~: de même, on les prendra de longueur exactement $n^k$, quitte à rajouter des symboles blancs.

    On les note dans un tableau~:
    $$
    \begin{array}{|c||c|c|c|c|c|c|}
        \hline
        \text{Conf.} & 0 & 1 & 2 & 3 & \cdots & n^k \\
        \hline
        \hline
        C_0= & q_0 & w_1 & w_2 & w_3 & \cdots & \sharp \\
        \hline
        C_1= & w_1'& q_1 & w_2 & w_3 & \cdots & \sharp \\
        \hline
        C_2= & w_1'& w_2 & q_2 & w_3 & \cdots & \sharp \\
        \hline
        C_2= & \cdots & \cdots & \cdots & \cdots & \cdots & \sharp \\
        \hline
        \vdots & &&&&& \vdots \\
        \hline
        C_{n^k}= & \cdots & \cdots & \cdots & \cdots & \cdots & \cdots \\
        \hline
    \end{array}
    $$

    On va donc coder une formule $\varphi_w$ qui code l'existence d'un tel tableau.

    On définit les variables $x_{i,j,a}$ pour $i,j\in \Lbrack 0,n^k \Rbrack$ et $a$ symbole de $A=\Gamma\cup Q$ qui codent le fait que la variable $a$ se trouve dans la case $i,j$. Il y a $|A| n^{2k+2}$ telles variables.

    On décompose notre formule $\varphi_w$ en quatre formules $\varphi_0$, $\varphi_1$, $\varphi_2$ et $\varphi_3$, qui vont chacune coder une propriété du tableau.

    \begin{itemize}
        \item[$\varphi_0$~:]
        Cette formule code le fait que chaque case du tableau contient un et un seul symbole de $A$~:
        $$\varphi_0 = \bigwedge_{0\leqslant i,j \leqslant n^k} \left[ \left( \bigvee_{a\in A} x_{i,j,a} \right) \land \left( \bigwedge_{a\not= a' \in A} (\overline{x}_{i,j,a} \lor \overline{x}_{i,j,a'} \right) \right].$$
        \item[$\varphi_1$~:]
        Cette formule code le fait que la première ligne du tableau est bien $q_0 w$~:
        $$\varphi_1 = \left( \bigwedge_{0\leqslant i \leqslant n} x_{0,i,w_i} \right) \land \left( \bigwedge_{n+1 \leqslant i \leqslant n^k} x_{0,i,\sharp}\right) .$$
        \item[$\varphi_2$~:]
        Cette formule assure que chaque ligne est obtenue en appliquant une transition valide de $\mathcal M$.

        Il suffit de remarquer que la valeur d'une case $(i,j)$ ne dépend que des trois cases au-dessus $(i-1,j-1)$, $(i-1,j)$ et $(i-1,j+1)$.

        Si dans ces trois cases se trouvent des symboles de bande, alors le contenu de la case $(i,j)$ est le même qu'en $(i-1,j)$.

        Si l'état de la configuration se trouve en $(i-1,j)$, alors l'état de $C_i$ se trouve en $(i,j-1)$ ou $(i,j+1)$.

        Donc, il suffit bien de regarder les "fenêtres" de taille $2\times 3$ du tableau. L'ensemble des fenêtres possibles ne dépend que de $A$ et des transitions de $\mathcal M$, et donc ne dépend pas de la taille de l'entrée $n$.

        Le fait que chaque fenêtre du tableau corresponde bien à une transition s'écrit donc comme une conjonction pour $0 \leqslant i,j \leqslant n^k$ de disjonctions des fenêtres possibles, ce qui est polynomial en $n$.

        \item[$\varphi_3$~:]
        Cette formule code le fait que $\mathcal M$ accepte $w$, \ie{} qu'au moins une des cases de la dernière ligne contient un état final~:
        $$\varphi_3 = \bigvee_{q\in F} \left( \bigvee_{0 \leqslant j \leqslant n^k} x_{n^k,j,q}\right).$$
    \end{itemize}
\end{proof}



\end{document}