Solve the following exercise by means of a reduction to
SAT:
- Given a $9\times 9$ matrix with some positions
initialized with a number between $1$ and $9$, assign (if possible) to each of
the empty positions of the matrix a number between $1$ and $9$ such that the
following conditions hold: (i) all the numbers occurring in each row of the
matrix are distinct, (ii) all the numbers occurring in each column of the
matrix are distinct, and (iii) all the numbers occurring in each of the nine
non-overlapping $3\times 3$ submatrices of the matrix are distinct.
The input of the exercise and the output with the solution (when the input is
solvable) are as follows:
Note: this problem can be solved in asymptotic constant time without reducing to SAT.