# Sudoku

The solver itself is a circuit that accepts the problem matrix as

**public input**and the solution matrix as**private input**. Both matrices are 9x9 matrices of`Field`

numbers.The solver itself is a circuit that accepts the problem matrix as

**public input**and the solution matrix as**private input**. Both matrices are 9x9 matrices of`Field`

numbers.sudoku :: Comp ()

sudoku = do

problem <- inputList2 Public 9 9 :: Comp [[UInt 4]]

solution <- inputList2 Private 9 9

The solution matrix must contain all the numbers in the problem matrix. We use the digit

`0`

to indicate empty cells in the problem matrix. So, if a digit is not `0`

, it should be equal to the corresponding digit in the solution matrix. forM_ [0 .. 8] $ \i ->

forM_ [0 .. 8] $ \j ->

assert $

cond

(problem !! i !! j `eq` 0)

true

((problem !! i !! j) `eq` (solution !! i !! j))

We want to make sure that all the numbers in the problem matrix are in the range

`0`

to `9`

. forM_ [0 .. 8] $ \i ->

forM_ [0 .. 8] $ \j ->

assert $ from0to9 (problem !! i !! j)

The helper function

`from0to9`

checks if a number is in the range `0`

to `9`

.from0to9 :: Field -> Boolean

from0to9 x = x `eq` 0 .|. x `eq` 1 .|. x `eq` 2 .|. x `eq` 3 .|. x `eq` 4 .|. x `eq` 5 .|. x `eq` 6 .|. x `eq` 7 .|. x `eq` 8 .|. x `eq` 9

In order for a Sudoku solution to be valid, the following conditions must be met:

- 1.Each row must contain the digits 1-9 without repetition.
- 2.2. Each column must contain the digits 1-9 without repetition.
- 3.3. Each of the 9 3x3 sub-boxes of the grid must contain the digits 1-9 without repetition.

Let's declare a helper function

`valid`

that checks if a list of 9 `Field`

numbers satisfies the Sudoku constraints. Instead of checking that the list contains the digits `1`

to `9`

without repetition, we check that the sum of the list is `45`

and the product of the list is `362880`

.valid :: [Field] -> Comp ()

valid xs = do

assert $ sum xs `eq` 45

assert $ product xs `eq` 362880

Using this helper function, we can check if the solution matrix is valid.

-- check if each row of the solution is valid:

forM_ [0 .. 8] $ \i ->

valid $ solution !! i

-- check if each column of the solution is valid:

forM_ [0 .. 8] $ \j ->

valid $ map (!! j) solution

-- check if each 3x3 sub-matrix of the solution is valid:

forM_ [0, 3, 6] $ \i ->

forM_ [0, 3, 6] $ \j ->

valid $

[ solution !! (i + x) !! (j + y)

| x <- [0 .. 2],

y <- [0 .. 2]

]

Last modified 1mo ago