Sudoku

Here's how to implement a Sudoku solver in Keelung!
Describing the Problem & the Solution
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))
Checking the problem matrix
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
Checking the solution matrix
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