\begin{frame}{Exercise}
  \begin{exampleblock}{}
    Reduce this bounded tiling problem
    to the satisfiability problem.\\
    \medskip
    
    \begin{minipage}{.5\textwidth}
    Types of tiles:
    \begin{center}\vspace{-2ex}
      \begin{tikzpicture}[default]
        \tile{0}{0}{g}{b}{r}{b}
        \tile{1.5}{0}{r}{b}{g}{b}
        \tile{3}{0}{r}{z}{g}{b}
        \node at (0.5,1.2) {$t_1$};
        \node at (0.5+1.5,1.2) {$t_2$};
        \node at (0.5+3,1.2) {$t_3$};
      \end{tikzpicture}
    \end{center}
    \end{minipage}\hfill%
    \begin{minipage}{.39\textwidth}
    First row:
    \begin{center}\vspace{-2ex}
      \begin{tikzpicture}[default]
        \tile{0}{0}{g}{b}{r}{b}
        \tile{1}{0}{r}{b}{g}{b}
        \node at (0.5,1.2) {$t_1$};
        \node at (0.5+1,1.2) {$t_2$};
      \end{tikzpicture}
    \end{center}
    \end{minipage}%
    \medskip
    \pause
    
    Then $\Phi$ is the conjunction of:
    \begin{enumerate}
      \item
        {\small\begin{math}
          \textstyle x_{11t_1} \wedge x_{12t_2}
        \end{math}}
    \pause
      \item 
        {\small
        \begin{math}
          \neg (x_{11t_1} \wedge x_{11t_2}) \wedge
          \neg (x_{12t_1} \wedge x_{12t_2}) \wedge
          \neg (x_{21t_1} \wedge x_{21t_2}) \wedge
          \neg (x_{22t_1} \wedge x_{22t_2}) \wedge 
        \end{math}\\%
        \begin{math}
          \neg (x_{11t_1} \wedge x_{11t_3}) \wedge
          \neg (x_{12t_1} \wedge x_{12t_3}) \wedge
          \neg (x_{21t_1} \wedge x_{21t_3}) \wedge
          \neg (x_{22t_1} \wedge x_{22t_3}) \wedge 
        \end{math}\\%
        \begin{math}
          \neg (x_{11t_2} \wedge x_{11t_3}) \wedge
          \neg (x_{12t_2} \wedge x_{12t_3}) \wedge
          \neg (x_{21t_2} \wedge x_{21t_3}) \wedge
          \neg (x_{22t_2} \wedge x_{22t_3}) \hphantom{\wedge} 
        \end{math}
        }\\
    \pause
      \item 
        {\small
        \begin{math}
          \big( (x_{11t_1} \wedge x_{12t_1}) \vee 
          (x_{11t_1} \wedge x_{12t_2}) \vee 
          (x_{11t_1} \wedge x_{12t_3}) \, \vee 
        \end{math}\\%
        \;\;\begin{math}
          (x_{11t_2} \wedge x_{12t_1}) \vee 
          (x_{11t_2} \wedge x_{12t_2}) \vee 
          (x_{11t_2} \wedge x_{12t_3}) \big) \wedge
        \end{math} \\
        \begin{math}
          \big( (x_{21t_1} \wedge x_{22t_1}) \vee 
          (x_{21t_1} \wedge x_{22t_2}) \vee 
          (x_{21t_1} \wedge x_{22t_3}) \, \vee 
        \end{math}\\%
        \;\;\begin{math}
          (x_{21t_2} \wedge x_{22t_1}) \vee 
          (x_{21t_2} \wedge x_{22t_2}) \vee 
          (x_{21t_2} \wedge x_{22t_3}) \big) 
        \end{math}
        }
    \pause
      \item
        {\small
        \begin{math}
          \big( (x_{11t_1} \wedge x_{21t_2}) \vee 
          (x_{11t_1} \wedge x_{21t_3}) \vee 
          (x_{11t_2} \wedge x_{21t_1}) \vee 
          (x_{11t_3} \wedge x_{21t_1}) \big) \wedge  
        \end{math}\\%
        \begin{math}
          \big( (x_{12t_1} \wedge x_{22t_2}) \vee 
          (x_{12t_1} \wedge x_{22t_3}) \vee 
          (x_{12t_2} \wedge x_{22t_1}) \vee 
          (x_{12t_3} \wedge x_{22t_1}) \big) 
        \end{math}\\%
        }
    \end{enumerate}
  \end{exampleblock}
   \end{frame}