\item \lect Use propositional logic to solve Sudoku. Rules: A Sudoku grid consists of a 9x9 square, which is partitioned into nine 3x3 squares. The goal of the game is to write one number from 1 to 9 in each cell in such a way, that each row, each column, and each 3x3-square contains each number exactly once. Usually several numbers are already given.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% source: https://texample.net/tikz/examples/sudoku/
%%%% Author: Roberto Bonvallet, published 2012-02-01, last accessed 2021-02-14, modified
\newcounter{row}
\newcounter{col}
\newcommand\setrow[9]{
  \setcounter{col}{1}
  \foreach \n in {#1, #2, #3, #4, #5, #6, #7, #8, #9} {
    \edef\x{\value{col} - 0.5}
    \edef\y{9.5 - \value{row}}
    \node[anchor=center] at (\x, \y) {\n};
    \stepcounter{col}
  }
  \stepcounter{row}
}

\begin{center}
\begin{tikzpicture}[scale=.35]
  \begin{scope}
    \draw (0, 0) grid (9, 9);
    \draw[very thick, scale=3] (0, 0) grid (3, 3);

    \setcounter{row}{1}
    \setrow { }{6}{ }  {7}{ }{ }  {1}{5}{ }
    \setrow { }{ }{3}  {9}{ }{ }  {8}{ }{ }
    \setrow { }{ }{2}  {3}{ }{ }  { }{4}{9}

    \setrow { }{ }{7}  { }{ }{4}  { }{ }{ }
    \setrow { }{4}{ }  { }{9}{ }  { }{8}{ }
    \setrow { }{ }{ }  {1}{ }{ }  {4}{ }{ }

    \setrow {6}{7}{ }  { }{ }{9}  {3}{ }{ }
    \setrow { }{ }{9}  { }{ }{2}  {5}{ }{ }
    \setrow { }{2}{8}  { }{ }{7}  { }{6}{ }

    \node[anchor=center] at (4.5, -1) {Sudoku};
  \end{scope}
\end{tikzpicture}
\end{center}

In order to model SUDOKU using propositional logic, we first need to define the propositional variables that we
want to use in our formula. We define variables $x_{ijk}$ for every row $i$,
for every column $j$, and for every value $k$. This encoding yields to 729 variables ranging from $x_{111}$ to $x_{999}$.
Using this variables, define the constraints for the rows, the columns, the 3x3-squares and the predefined numbers. \\
\vspace{0.5cm}