\begin{frame}{Satisfiability Problem is NP-complete}
  \vspace{-1ex}
  \begin{block}{Proof continued\ldots}
    We define $\Phi$ to be the conjunction of the 4 formulas:
    \begin{enumerate}
      \item Fist row is $t_1\cdots t_n$:\vspace{-3ex}
        \begin{talign}
          \textstyle \bigwedge_{c=1}^n x_{1ct_k}
        \end{talign}
      \item At every position at most one tile type:
        \begin{talign}
          \textstyle \bigwedge_{r=1}^n~\bigwedge_{c=1}^n~\bigwedge_{t\neq t'}\neg(x_{rct}\wedge x_{rct'})
        \end{talign}
      \item Neighbouring tiles must match (horizontal neighbours):
        \begin{talign}
          \textstyle \bigwedge_{r=1}^n~\bigwedge_{c=1}^{n-1}~\bigvee_{tt'\,{\rm matches}}(x_{rct}\wedge x_{r(c+1)t'})
        \end{talign}
      \item Neighbouring tiles must match (vertical neighbours):
        \begin{talign}
          \textstyle \bigwedge_{r=1}^{n-1}~\bigwedge_{c=1}^n~\bigvee_{\substack{t'\\\!\!t}{\rm matches}}(x_{rct}\wedge x_{(r+1)ct'})
        \end{talign}
    \end{enumerate}
    \pause
    Size of the formula is polynomial in $n$. 
    
    \pause\smallskip
    There exists an $n\times n$ tiling with first row $t_1 \cdots t_n$ \\
    \hfill $\iff$ the propositional formula $\Phi$ is satisfiable.
    \pause\smallskip
    
    Thus we have a polynomial-time reduction.\qed
  \end{block}
\end{frame}