You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

30 lines
2.3 KiB

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