Modelling sudoku in propositional logic

Sudoku is a puzzle, see [1] for a definition. It can be nicely modelled in propositional logic.

Modelling sudoku in propositional logic means to first identify a set of variables for representing filled grids. One option is to use variables $X_{i,j}^k$ where $\beta(X_{i,j}^k) = 1$ is supposed to mean that in line $i$ and column $j$ we find the symbol $k$.

Here, we let $i,j,k < 9$ for convenience. So we think of the grid as being filled with the symbols $0, \dots, 8$ instead of $1, \dots, 9$ and we start indexing rows and columns with $0$.

To represent all filled grids, we can use the formula $\chi_0$ defined by $$\chi_0 = \bigwedge_{i<9}\bigwedge_{j<9}\dot{\bigvee_{k<9}} X_{i,j}^k\enspace.$$ Then a 1-assignment of $\chi_0$ on the set of variables represents a filled grid, and vice versa.

If we want to represent all correctly filled grids we have to make sure:

1. Each symbol occurs in each row.
2. Each symbol occurs in each column.
3. Each symbol occurs in each subgrid.

This can be expressed by the formuls $\chi_1$ defined by $$\chi_1 = \bigwedge_{k<9}\bigwedge_{i<9}\bigvee_{j<9} X_{i,j}^k \wedge \bigwedge_{k<9}\bigwedge_{j<9}\bigvee_{i<9} X_{i,j}^k \wedge \bigwedge_{k<9}\bigwedge_{i<3}\bigwedge_{j<3}\bigvee_{i'<3}\bigvee_{j'<3} X_{3i+i',3j+j'}^k\enspace,$$ where each of the three conjuncts corresponds to one of the conditions. Here, we can state that a 1-assignment of $\chi_0 \wedge \chi_1$ on the set of variables represents a correctly filled grid, and vice versa.

Typically, a soduko instance is partially prefilled. So in a certain sense we are given a partial function $s \colon \{0, \dots, 8\}^2 \not\to \{0, \dots, 8\}$ and we want to know how we can fill the remaining cells in the grid correctly.

To this end, we turn $s$ into a formula $\varphi_s$: $$\varphi_s = \bigwedge_{\langle i,j \rangle \in \text{dom}(s)} X_{i,j}^{s(i,j)} \enspace$$.

We can now state:

Proposition Let $s \colon \{0, \dots, 8\}^2 \not\to \{0, \dots, 8\}$ be a function which partially prefills sudoku. Then:

1. The 1-assignments of $$\chi_0 \wedge \chi_1 \wedge \varphi_s$$ represent the correctly filled grids that are prefilled according to $s$.
2. The formula $$\chi_0 \wedge \chi_1 \wedge \varphi_s$$ can easily be converted into conjunctive normal form.

Exercises

Exercise Ordinary sudoku is, in some sense, 3-sudoku. (Why is this so?)

1. Give a definition of $n$-soduku for $n > 0$.
2. Model $n$-soduku in propositional logic.