91/122
\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}