\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}