Question

Model \(16 \times 16\) Sudoku puzzles (with \(4 \times 4\) blocks) as satisfiability problems.

Short answer

The model is \( \wedge _{i = 1}^{16} \wedge _{n = 1}^{16} \vee _{j = 1}^{16}p\left( {i,\;j,\;n} \right)\), \( \wedge _{j = 1}^{16} \wedge _{n = 1}^{16} \vee _{i = 1}^{16}p\left( {i,\;j,\;n} \right)\), \( \wedge _{r = 0}^4 \wedge _{s = 0}^4 \vee _{n = 1}^{16} \vee _{i = 1}^4 \vee _{j = 1}^4p\left( {4r + i,4s + \;j,\;n} \right)\), and \(p\left( {i,\;j,\;n} \right) \to \neg p\left( {i,\;j,\;n'} \right)\).

Step-by-step solution

Describe the given information

Given that 16×16Sudoku puzzle (which thus contains every integer from 1 to 16 in each row, column and\(4 \times 4\)block).

Model \(16 \times 16\) Sudoku puzzles as satisfiability problems

Let \(p\left( {i,\;j,\;n} \right)\) represent the cell in row \(i\) and column \(j\) and that has the value \(n\)is thus an integer between \(1\) and \(16\), inclusive).

Every row needs to contain every number between \(1\) and \(16\). There are \(16\) rows and \(16\) columns.

\( \wedge _{i = 1}^{16} \wedge _{n = 1}^{16} \vee _{j = 1}^{16}p\left( {i,\;j,\;n} \right)\)

Every column needs to contain every number between \(1\) and \(16\). There are \(16\) rows and \(16\) columns.

\( \wedge _{j = 1}^{16} \wedge _{n = 1}^{16} \vee _{i = 1}^{16}p\left( {i,\;j,\;n} \right)\)

Every \(4 \times 4\)block contains every number between 1 and 4.

\( \wedge _{r = 0}^4 \wedge _{s = 0}^4 \vee _{n = 1}^{16} \vee _{i = 1}^4 \vee _{j = 1}^4p\left( {4r + i,4s + \;j,\;n} \right)\)

Finally, no cell contains more than one number.

\(p\left( {i,\;j,\;n} \right) \to \neg p\left( {i,\;j,\;n'} \right)\)

Therefore, the model is \( \wedge _{i = 1}^{16} \wedge _{n = 1}^{16} \vee _{j = 1}^{16}p\left( {i,\;j,\;n} \right)\), \( \wedge _{j = 1}^{16} \wedge _{n = 1}^{16} \vee _{i = 1}^{16}p\left( {i,\;j,\;n} \right)\), \( \wedge _{r = 0}^4 \wedge _{s = 0}^4 \vee _{n = 1}^{16} \vee _{i = 1}^4 \vee _{j = 1}^4p\left( {4r + i,4s + \;j,\;n} \right)\), and \(p\left( {i,\;j,\;n} \right) \to \neg p\left( {i,\;j,\;n'} \right)\).