\begin{itemize}
    \item \emph{Row-constraints:} \emph{If} a cell in a row has a certain value, \emph{then} no other cell in that row can have that value. For each $i$, and each $k$ we have:
    $$x_{i1k} \imp \lnot x_{i2k} \land \lnot x_{i3k} \land ... \land \lnot x_{i9k}$$
    $$x_{i2k} \imp \lnot x_{i1k} \land \lnot x_{i2k} \land ... \land \lnot x_{i9k}$$
    $$\vdots$$
    $$x_{i9k} \imp \lnot x_{i1k} \land \lnot x_{i2k} \land ... \land \lnot x_{i8k}$$

    \item \emph{Column-constraints:} \emph{If} a cell in a column has a certain value, \emph{then} no other cell in that column can have that value. For each $j$, and each $k$ we have:
    $$x_{1jk} \imp \lnot x_{2jk} \land \lnot x_{3jk} \land ... \land \lnot x_{9jk}$$
    $$x_{2jk} \imp \lnot x_{1jk} \land \lnot x_{2jk} \land ... \land \lnot x_{9jk}$$
    $$\vdots$$
    $$x_{9jk} \imp \lnot x_{1jk} \land \lnot x_{2jk} \land ... \land \lnot x_{8jk}$$

    \item \emph{Square-constraints:} \emph{If} a cell in a 3x3 square has a certain value, \emph{then} no other cell in that square can have that value. For the first square, we have for each $k$:
    $$x_{11k} \imp \lnot x_{12k} \land \lnot x_{13k} \land \lnot x_{21k} \land \lnot x_{22k} \land \lnot x_{23k} \land \lnot x_{31k} \land \lnot x_{32k} \land \lnot x_{33k}$$
    $$\vdots$$
    $$x_{33k} \imp \lnot x_{11k} \land \lnot x_{12k} \land \lnot x_{13k} \land \lnot x_{21k} \land \lnot x_{22k} \land \lnot x_{23k} \land \lnot x_{31k} \land \lnot x_{32k}$$
    The constraints for the remaining squares are similar.

    \item \emph{Predefined-number-constraints:} If a cell has a predefined value, we need to set the corresponding variable to true, e.g., the cell in the fifth row and the fifth column has the value 9.
    Therefore we have $$x_{559}.$$

    \item \emph{Cell-constraints:} Each cell must contain a number ranging from one to nine.
    For each $i$, and each $j$ we have
    $$x_{ij1} \lor x_{ij2} \lor ... \lor x_{ij9}.$$ On its own, this constraint would allow for a cell to have more than one value. However, this is not possible due to the other constraints.
\end{itemize}

To construct the final propositional formula, all constraints need to be connected via conjunctions.
A satisfying assignment for the final formula represents one possible solution for the Sudoku puzzle.
In case that there does not exists a solution, the SAT sovler would return UNSAT.