\begin{frame}
\mat{Global constraints} involve an arbitrary number of variables (but not necessarily all) 
\begin{columns}
\begin{column}{0.5\textwidth}
\begin{example}[All different]
\end{example}
\centering
\pgfimage[width=3.6cm]{fig/sudoku2}   

Alldiff (A1,A2,A3,A4,A5,A6, A7, A8, A9)\\
Alldiff (B1,B2,B3,B4,B5,B6,B7,B8,B9)\\
...\\
Alldiff (A1,B1,C1,D1,E1, F1,G1,H1, I1)\\
Alldiff (A2,B2,C2,D2,E2, F2,G2,H2, I2)\\
...\\
Alldiff (A1,A2,A3,B1,B2,B3,C1,C2,C3)\\
Alldiff (A4,A5,A6,B4,B5,B6,C4,C5,C6)

\end{column}

\begin{column}{0.5\textwidth}
\only<2->{A logician taking ginkgo biloba
\pgfimage[width=5.2cm]{fig/sudoku0.png}}    
\end{column}
\end{columns}
\end{frame}

\frame[plain]{\frametitle{A logician without ginkgo biloba}
\begin{example}[Killer Sudoku]
The numbers may occur
only once in each row, column and colored area if specified. In addition to Sudoku, a
Killer Sudoku grid is divided into cages, shown with dashed lines. The sum of the 
numbers in a cage must equal the small number in its top-left corner. The same number cannot appear in a cage more than once.
\end{example}
\begin{columns}
\begin{column}{0.42\textwidth}
\centering
\vspace{-0.4cm}
\pgfimage[width=3cm]{fig/killer.png} 

\begin{enumerate}
 \item Note the explicit negation required under the open world assumption
\item Domain size refers to the variables, not to the max value appearing in the formalisation 
\end{enumerate}

\end{column}
\begin{column}{0.58\textwidth}
\pgfimage[width=6.9cm]{fig/killer2.png} 
\end{column}
 
\end{columns}

}


