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:

• sudoku: array [9] of array [9] of int
  

  The input is a single variable sudoku, which is a matrix with $9$ rows and $9$ columns. Each position of the matrix has either a number between $1$ and $9$, or a $0$ to denote that the position is empty.

• solved: array [9] of array [9] of int
  

  The output is a single variable solved, which is a matrix with $9$ rows and $9$ columns, and each position contains a number between $1$ and $9$ that satisfies the restrictions of the problem.

Note: this problem can be solved in asymptotic constant time without reducing to SAT.