A Sudoku solver
Auteurs: Claude Marché / Guillaume Melquiond
Catégories: Array Data Structure
Outils: Why3
see also the index (by topic, by tool, by reference, by year)
An Efficient Sudoku Solver
Author: Claude Marché (Inria) Guillaume Melquiond (Inria)
A theory of 9x9 grids
module Grid use int.Int use map.Map type grid = map int int
A grid is a map from integers to integers
predicate is_index (i:int) = 0 <= i < 81
valid indexes are 0..80
predicate valid_values (g:grid) = forall i. is_index i -> 0 <= g[i] <= 9
valid values are 0..9. 0 denotes an empty cell
predicate grid_eq_sub (g1 g2:grid) (a b:int) = forall j. a <= j < b -> g1[j] = g2[j]
extensional equality of grids and sub-grids
predicate grid_eq (g1 g2:grid) = grid_eq_sub g1 g2 0 81 lemma grid_eq_sub: forall g1 g2 a b. 0 <= a <= 81 /\ 0 <= b <= 81 /\ grid_eq g1 g2 -> grid_eq_sub g1 g2 a b
Grid "Chunks"
A chunk is either a column, a row or a square.
A chunk is defined by a starting index s and a set of 9 offsets {o0,..,o8}, that thus denotes a set of 9 cells {s+o0,..,s+o8} in a grid.
Each cell of the grid belongs to 3 chunks, one of each kind. For each cell index, there is a unique starting index respectively for the column, the row and the square it belongs to.
use array.Array type sudoku_chunks = { column_start : array int; column_offsets : array int; row_start : array int; row_offsets : array int; square_start : array int; square_offsets : array int; } predicate chunk_valid_indexes (start:array int) (offsets:array int) = start.length = 81 /\ offsets.length = 9 /\ forall i o:int. is_index i /\ 0 <= o < 9 -> is_index(start[i] + offsets[o])
Chunks must point to valid indexes of the grid
predicate disjoint_chunks (start:array int) (offsets:array int) = start.length = 81 /\ offsets.length = 9 /\ forall i1 i2 o:int. is_index i1 /\ is_index i2 /\ 0 <= o < 9 -> let s1 = start[i1] in let s2 = start[i2] in s1 <> s2 -> i1 <> s2 + offsets[o]
Chunks (of the same kind column, row or square) with distinct starting cells must be disjoint
predicate well_formed_sudoku (s:sudoku_chunks) = chunk_valid_indexes s.column_start s.column_offsets /\ chunk_valid_indexes s.row_start s.row_offsets /\ chunk_valid_indexes s.square_start s.square_offsets /\ disjoint_chunks s.column_start s.column_offsets /\ disjoint_chunks s.row_start s.row_offsets /\ disjoint_chunks s.square_start s.square_offsets
A sudoku grid is well formed when chunks are valid and disjoint
Valid Sudoku Solutions
valid_chunk g i start offsets is true whenever the chunk
denoted by start,offsets from cell i is "valid" in grid g, in
the sense that it contains at most one occurrence of each number
between 1 and 9
predicate valid_chunk (g:grid) (i:int) (start:array int) (offsets:array int) = let s = start[i] in forall o1 o2 : int. 0 <= o1 < 9 /\ 0 <= o2 < 9 /\ o1 <> o2 -> let i1 = s + offsets[o1] in let i2 = s + offsets[o2] in 1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 -> Map.get g i1 <> Map.get g i2 predicate valid_column (s:sudoku_chunks) (g:grid) (i:int) = valid_chunk g i s.column_start s.column_offsets predicate valid_row (s:sudoku_chunks) (g:grid) (i:int) = valid_chunk g i s.row_start s.row_offsets predicate valid_square (s:sudoku_chunks) (g:grid) (i:int) = valid_chunk g i s.square_start s.square_offsets predicate valid (s:sudoku_chunks) (g : grid) = forall i : int. is_index i -> valid_column s g i /\ valid_row s g i /\ valid_square s g i
valid g is true when all chunks are valid
predicate full (g : grid) = forall i : int. is_index i -> 1 <= Map.get g i <= 9
full g is true when all cells are filled
predicate included (g1 g2 : grid) = forall i : int. is_index i /\ 1 <= Map.get g1 i <= 9 -> Map.get g2 i = Map.get g1 i
included g1 g2
lemma subset_valid_chunk : forall g h : grid. included g h -> forall i:int, s o:array int. is_index i /\ chunk_valid_indexes s o /\ valid_chunk h i s o -> valid_chunk g i s o
validity is monotonic w.r.t. inclusion
lemma subset_valid : forall s g h. well_formed_sudoku s /\ included g h /\ valid s h -> valid s g predicate is_solution_for (s:sudoku_chunks) (sol:grid) (data:grid) = included data sol /\ full sol /\ valid s sol
A solution of a grid data is a full grid sol
that is valid and includes data
end module TheClassicalSudokuGrid
Concrete Values of Chunks for the Classical Sudoku Grid
use Grid use map.Map use int.Int use array.Array let classical_sudoku () : sudoku_chunks ensures { well_formed_sudoku result } = (* column start *) let cs = Array.make 81 0 in cs[ 0]<-0; cs[ 1]<-1; cs[ 2]<-2; cs[ 3]<-3; cs[ 4]<-4; cs[ 5]<-5; cs[ 6]<-6; cs[ 7]<-7; cs[ 8]<-8; cs[ 9]<-0; cs[10]<-1; cs[11]<-2; cs[12]<-3; cs[13]<-4; cs[14]<-5; cs[15]<-6; cs[16]<-7; cs[17]<-8; cs[18]<-0; cs[19]<-1; cs[20]<-2; cs[21]<-3; cs[22]<-4; cs[23]<-5; cs[24]<-6; cs[25]<-7; cs[26]<-8; cs[27]<-0; cs[28]<-1; cs[29]<-2; cs[30]<-3; cs[31]<-4; cs[32]<-5; cs[33]<-6; cs[34]<-7; cs[35]<-8; cs[36]<-0; cs[37]<-1; cs[38]<-2; cs[39]<-3; cs[40]<-4; cs[41]<-5; cs[42]<-6; cs[43]<-7; cs[44]<-8; cs[45]<-0; cs[46]<-1; cs[47]<-2; cs[48]<-3; cs[49]<-4; cs[50]<-5; cs[51]<-6; cs[52]<-7; cs[53]<-8; cs[54]<-0; cs[55]<-1; cs[56]<-2; cs[57]<-3; cs[58]<-4; cs[59]<-5; cs[60]<-6; cs[61]<-7; cs[62]<-8; cs[63]<-0; cs[64]<-1; cs[65]<-2; cs[66]<-3; cs[67]<-4; cs[68]<-5; cs[69]<-6; cs[70]<-7; cs[71]<-8; cs[72]<-0; cs[73]<-1; cs[74]<-2; cs[75]<-3; cs[76]<-4; cs[77]<-5; cs[78]<-6; cs[79]<-7; cs[80]<-8; (* column offset *) let co = Array.make 9 0 in co[ 0]<-0; co[ 1]<-9; co[ 2]<-18; co[ 3]<-27; co[ 4]<-36; co[ 5]<-45; co[ 6]<-54; co[ 7]<-63; co[ 8]<-72; (* row start *) let rs = Array.make 81 0 in rs[ 0]<- 0; rs[ 1]<- 0; rs[ 2]<- 0; rs[ 3]<- 0; rs[ 4]<-0; rs[5]<-0; rs[ 6]<- 0; rs[ 7]<- 0; rs[ 8]<- 0; rs[ 9]<- 9; rs[10]<-9; rs[11]<-9; rs[12]<- 9; rs[13]<- 9; rs[14]<- 9; rs[15]<- 9; rs[16]<-9; rs[17]<-9; rs[18]<-18; rs[19]<-18; rs[20]<-18; rs[21]<-18; rs[22]<-18; rs[23]<-18; rs[24]<-18; rs[25]<-18; rs[26]<-18; rs[27]<-27; rs[28]<-27; rs[29]<-27; rs[30]<-27; rs[31]<-27; rs[32]<-27; rs[33]<-27; rs[34]<-27; rs[35]<-27; rs[36]<-36; rs[37]<-36; rs[38]<-36; rs[39]<-36; rs[40]<-36; rs[41]<-36; rs[42]<-36; rs[43]<-36; rs[44]<-36; rs[45]<-45; rs[46]<-45; rs[47]<-45; rs[48]<-45; rs[49]<-45; rs[50]<-45; rs[51]<-45; rs[52]<-45; rs[53]<-45; rs[54]<-54; rs[55]<-54; rs[56]<-54; rs[57]<-54; rs[58]<-54; rs[59]<-54; rs[60]<-54; rs[61]<-54; rs[62]<-54; rs[63]<-63; rs[64]<-63; rs[65]<-63; rs[66]<-63; rs[67]<-63; rs[68]<-63; rs[69]<-63; rs[70]<-63; rs[71]<-63; rs[72]<-72; rs[73]<-72; rs[74]<-72; rs[75]<-72; rs[76]<-72; rs[77]<-72; rs[78]<-72; rs[79]<-72; rs[80]<-72; (* row offset *) let ro = Array.make 9 0 in ro[ 0]<-0; ro[ 1]<-1; ro[ 2]<-2; ro[ 3]<-3; ro[ 4]<-4; ro[ 5]<-5; ro[ 6]<-6; ro[ 7]<-7; ro[ 8]<-8; (* square start *) let ss = Array.make 81 0 in ss[ 0]<- 0; ss[ 1]<- 0; ss[ 2]<- 0; ss[ 3]<- 3; ss[ 4]<- 3; ss[ 5]<- 3; ss[ 6]<- 6; ss[ 7]<- 6; ss[ 8]<- 6; ss[ 9]<- 0; ss[10]<- 0; ss[11]<- 0; ss[12]<- 3; ss[13]<- 3; ss[14]<- 3; ss[15]<- 6; ss[16]<- 6; ss[17]<- 6; ss[18]<- 0; ss[19]<- 0; ss[20]<- 0; ss[21]<- 3; ss[22]<- 3; ss[23]<- 3; ss[24]<- 6; ss[25]<- 6; ss[26]<- 6; ss[27]<-27; ss[28]<-27; ss[29]<-27; ss[30]<-30; ss[31]<-30; ss[32]<-30; ss[33]<-33; ss[34]<-33; ss[35]<-33; ss[36]<-27; ss[37]<-27; ss[38]<-27; ss[39]<-30; ss[40]<-30; ss[41]<-30; ss[42]<-33; ss[43]<-33; ss[44]<-33; ss[45]<-27; ss[46]<-27; ss[47]<-27; ss[48]<-30; ss[49]<-30; ss[50]<-30; ss[51]<-33; ss[52]<-33; ss[53]<-33; ss[54]<-54; ss[55]<-54; ss[56]<-54; ss[57]<-57; ss[58]<-57; ss[59]<-57; ss[60]<-60; ss[61]<-60; ss[62]<-60; ss[63]<-54; ss[64]<-54; ss[65]<-54; ss[66]<-57; ss[67]<-57; ss[68]<-57; ss[69]<-60; ss[70]<-60; ss[71]<-60; ss[72]<-54; ss[73]<-54; ss[74]<-54; ss[75]<-57; ss[76]<-57; ss[77]<-57; ss[78]<-60; ss[79]<-60; ss[80]<-60; (* square offset *) let sqo = Array.make 9 0 in sqo[0]<-0; sqo[1]<-1; sqo[2]<-2; sqo[3]<-9; sqo[4]<-10; sqo[5]<-11; sqo[6]<-18; sqo[7]<-19; sqo[8]<-20; { column_start = cs; column_offsets = co; row_start = rs; row_offsets = ro; square_start = ss; square_offsets = sqo; } end
A Sudoku Solver
module Solver use Grid use array.Array use int.Int predicate valid_chunk_up_to (g:grid) (i:int) (start:array int) (offsets:array int) (off:int) = let s = start[i] in forall o1 o2 : int. 0 <= o1 < off /\ 0 <= o2 < off /\ o1 <> o2 -> let i1 = s + offsets[o1] in let i2 = s + offsets[o2] in 1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 -> Map.get g i1 <> Map.get g i2
predicate for the loop invariant of next function
exception Invalid use array.Array let check_valid_chunk (g:array int) (i:int) (start:array int) (offsets:array int) : unit requires { g.length = 81 } requires { valid_values g.elts } requires { is_index i } requires { chunk_valid_indexes start offsets } ensures { valid_chunk g.elts i start offsets } raises { Invalid -> not (valid_chunk g.elts i start offsets) } = let s = start[i] in let b = Array.make 10 False in for off = 0 to 8 do invariant { valid_chunk_up_to g.elts i start offsets off } invariant { forall o:int. 0 <= o < off -> let v = g[s + offsets[o]] in 1 <= v <= 9 -> b[v] = True } invariant { forall j:int. 1 <= j <= 9 -> b[j] = True -> exists o:int. 0 <= o < off /\ Map.get g.elts (s + offsets[o]) = j } let v = g[s + offsets[off]] in if 1 <= v && v <= 9 then begin if b[v] then raise Invalid; b[v] <- True end done
check_valid_chunk g i start offsets checks the validity
of the chunk that includes i
predicate valid_up_to (s:sudoku_chunks) (g:grid) (i:int) = forall j : int. 0 <= j < i -> valid_column s g j /\ valid_row s g j /\ valid_square s g j
predicate for the loop invariant of next function
let check_valid (s:sudoku_chunks) (g : array int) : bool requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } ensures { result <-> valid s g.elts } = try for i = 0 to 80 do invariant { valid_up_to s g.elts i } check_valid_chunk g i s.column_start s.column_offsets; check_valid_chunk g i s.row_start s.row_offsets; check_valid_chunk g i s.square_start s.square_offsets done; True with Invalid -> False end
check_valid s g checks if the (possibly partially filled) grid
g is valid. (This function is not needed by the solver)
predicate full_up_to (g : grid) (i : int) = forall j : int. 0 <= j < i -> 1 <= Map.get g j <= 9
full_up_to g i is true when all cells 0..i-1 in grid g are
non empty
lemma full_up_to_change : forall g i x. is_index i /\ full_up_to g i -> 1 <= x <= 9 -> full_up_to (Map.set g i x) (i+1) let rec lemma full_up_to_frame (g1 g2:grid) (i:int) requires { 0 <= i <= 81 } requires { grid_eq_sub g1 g2 0 i } requires { full_up_to g1 i } variant { i } ensures { full_up_to g2 i } = if i > 0 then begin assert { full_up_to g1 (i-1) }; full_up_to_frame g1 g2 (i-1) end let lemma full_up_to_frame_all (g1 g2:grid) (i:int) requires { 0 <= i <= 81 } requires { grid_eq g1 g2 } requires { full_up_to g1 i } ensures { full_up_to g2 i } = assert { grid_eq_sub g1 g2 0 i } let lemma valid_chunk_frame (start:array int) (offsets:array int) (g1 g2:grid) (i:int) requires { chunk_valid_indexes start offsets } requires { 0 <= i < 81 } requires { grid_eq g1 g2 } requires { valid_chunk g1 i start offsets } ensures { valid_chunk g2 i start offsets } = () let rec lemma valid_up_to_frame (s:sudoku_chunks) (g1 g2:grid) (i:int) requires { well_formed_sudoku s } requires { 0 <= i <= 81 } requires { grid_eq g1 g2 } requires { valid_up_to s g1 i } variant { i } ensures { valid_up_to s g2 i } = if i > 0 then begin assert { valid_up_to s g1 (i-1) }; valid_up_to_frame s g1 g2 (i-1); valid_chunk_frame s.column_start s.column_offsets g1 g2 (i-1); valid_chunk_frame s.row_start s.row_offsets g1 g2 (i-1); valid_chunk_frame s.square_start s.square_offsets g1 g2 (i-1); end
how to prove the "hard" property : if
valid_up_to s g i
and
h = g[i <- k (with 1 <= k <= 9)]
and
valid_column s h i /\ valid_row s h i /\ valid_square s h i
then
valid_up_to s h (i+1)
then the problem is that one should prove that for each j in 0..i-1 :
valid_column s h j /\ valid_row s h j /\ valid_square s h j
this is true but with 2 different possible reasons:
if column_start j = column_start i then
valid_column s h j is true because valid_column s h i is true
else
valid_column s h j is true because valid_column s g j is true
because valid_column s h j does not depend on h[i]
lemma valid_unchanged_chunks: forall g : grid, i1 i2 k:int, start offsets:array int. disjoint_chunks start offsets -> is_index i1 /\ is_index i2 /\ 1 <= k <= 9 -> let s1 = start[i1] in let s2 = start[i2] in let h = Map.set g i1 k in s1 <> s2 /\ valid_chunk g i2 start offsets -> valid_chunk h i2 start offsets lemma valid_changed_chunks: forall g : grid, i1 i2 k:int, start offsets:array int. is_index i1 /\ is_index i2 /\ 1 <= k <= 9 -> let s1 = start[i1] in let s2 = start[i2] in let h = Map.set g i1 k in s1 = s2 /\ valid_chunk h i1 start offsets -> valid_chunk h i2 start offsets let ghost valid_up_to_change (s:sudoku_chunks) (g:grid) (i x : int) requires { well_formed_sudoku s } requires { is_index i } requires { valid_up_to s g i } requires { 1 <= x <= 9 } requires { valid_column s (Map.set g i x) i } requires { valid_row s (Map.set g i x) i } requires { valid_square s (Map.set g i x) i } ensures { valid_up_to s (Map.set g i x) (i+1) } = () exception SolutionFound
The main solver loop
let rec solve_aux (s:sudoku_chunks) (g : array int) (i : int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } requires { 0 <= i <= 81 } requires { valid_up_to s g.elts i } requires { full_up_to g.elts i } writes { g } variant { 81 - i } ensures { grid_eq (old g).elts g.elts } ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) } raises { SolutionFound -> is_solution_for s g.elts (old g).elts } = if i = 81 then raise SolutionFound; (* assert { is_index i }; *) if g[i] <> 0 then try (* assert { 1 <= g[i] <= 9 }; *) check_valid_chunk g i s.column_start s.column_offsets; check_valid_chunk g i s.row_start s.row_offsets; check_valid_chunk g i s.square_start s.square_offsets; solve_aux s g (i + 1) with Invalid -> () end else begin let ghost old_g = g.elts in for k = 1 to 9 do invariant { grid_eq old_g (Map.set g.elts i 0) } invariant { full_up_to g.elts i } invariant { (* for completeness *) forall k'. 1 <= k' < k -> let g' = Map.set old_g i k' in forall h : grid. included g' h /\ full h -> not (valid s h) } g[i] <- k; valid_up_to_frame s old_g (Map.set g.elts i 0) i; try check_valid_chunk g i s.column_start s.column_offsets; check_valid_chunk g i s.row_start s.row_offsets; check_valid_chunk g i s.square_start s.square_offsets; (* the hard part: see lemma valid_up_to_change *) assert { let grid' = Map.set old_g i k in grid_eq grid' g.elts && valid_chunk grid' i s.column_start s.column_offsets && valid_chunk grid' i s.row_start s.row_offsets && valid_chunk grid' i s.square_start s.square_offsets && valid_up_to s grid' (i+1) }; valid_up_to_change s old_g i k; solve_aux s g (i + 1) with Invalid -> assert { (* for completeness *) not (valid s (Map.set old_g i k)) }; assert { (* for completeness *) let g' = Map.set old_g i k in forall h : grid. included g' h /\ full h -> not (valid s h) } end done; g[i] <- 0; assert { (* for completeness *) forall h:grid. included old_g h /\ full h -> let k' = Map.get h i in let g' = Map.set old_g i k' in included g' h } end exception NoSolution let solve (s:sudoku_chunks) (g : array int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ensures { is_solution_for s g.elts (old g).elts } raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = try solve_aux s g 0; raise NoSolution with SolutionFound -> g end let check_then_solve (s:sudoku_chunks) (g : array int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ensures { is_solution_for s g.elts (old g).elts } raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = if check_valid s g then solve s g else raise NoSolution end (* Proof in progress module RandomSolver (* a variant: solve using a random order of cells *) use Grid use array.Array use int.Int use random.Random use Solver let rec solve_aux (s:sudoku_chunks) (randoffset:int) (g : array int) (i : int) requires { well_formed_sudoku s } requires { 0 <= randoffset <= 80 } requires { g.length = 81 } requires { valid_values g.elts } requires { 0 <= i <= 81 } requires { valid_up_to s g.elts i } requires { full_up_to g.elts i } writes { g } variant { 81 - i } ensures { grid_eq (old g).elts g.elts } ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) } raises { SolutionFound -> is_solution_for s g.elts (old g).elts } = if i = 81 then raise SolutionFound; (* assert { is_index i }; *) let j = i + randoffset in let j = if j >= 81 then j - 81 else j in (* assert { is_index j }; *) if g[j] <> 0 then try (* assert { 1 <= g[j] <= 9 }; *) Solver.check_valid_chunk g j s.column_start s.column_offsets; check_valid_chunk g j s.row_start s.row_offsets; check_valid_chunk g j s.square_start s.square_offsets; solve_aux s randoffset g (i + 1) with Invalid -> () end else begin label L in for k = 1 to 9 do invariant { grid_eq (g at L).elts (Map.set g.elts j 0) } invariant { full_up_to g.elts i } (* TODO i -> j *) invariant { (* for completeness *) forall k'. 1 <= k' < k -> let g' = Map.set (g at L).elts i k' in (* TODO i -> j *) forall h : grid. included g' h /\ full h -> not (valid s h) } g[j] <- k; try check_valid_chunk g j s.column_start s.column_offsets; check_valid_chunk g j s.row_start s.row_offsets; check_valid_chunk g j s.square_start s.square_offsets; (* the hard part: see lemma valid_up_to_change *) (* TODO i -> j *) assert { let grid' = Map.set (g at L).elts i k in grid_eq grid' g.elts && valid_chunk grid' i s.column_start s.column_offsets && valid_chunk grid' i s.row_start s.row_offsets && valid_chunk grid' i s.square_start s.square_offsets && valid_up_to s grid' (i+1) }; assert { valid_up_to s g.elts (i+1) }; solve_aux s randoffset g (i + 1) with Invalid -> assert { (* for completeness *) not (valid s (Map.set (g at L).elts i k)) }; assert { (* for completeness *) let g' = Map.set (g at L).elts i k in forall h : grid. included g' h /\ full h -> not (valid s h) } end done; g[j] <- 0; assert { (* for completeness *) forall h:grid. included (g at L).elts h /\ full h -> let k' = Map.get h i in let g' = Map.set (g at L).elts i k' in included g' h } end exception NoSolution let solve (s:sudoku_chunks) (g : array int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ensures { is_solution_for s g.elts (old g).elts } raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = try let randoffset = 27 in solve_aux s randoffset g 0; raise NoSolution with SolutionFound -> g end let check_then_solve (s:sudoku_chunks) (g : array int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ensures { is_solution_for s g.elts (old g).elts } raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = if check_valid s g then solve s g else raise NoSolution end *)
Some Tests
module Test use Grid use TheClassicalSudokuGrid use Solver use map.Map use array.Array let test0 () raises { NoSolution -> true } = let a = Array.make 81 0 in solve (classical_sudoku()) a (* a possible solution: 1, 2, 3, 4, 5, 6, 7, 8, 9, 4, 5, 6, 7, 8, 9, 1, 2, 3, 7, 8, 9, 1, 2, 3, 4, 5, 6, 2, 1, 4, 3, 6, 5, 8, 9, 7, 3, 6, 5, 8, 9, 7, 2, 1, 4, 8, 9, 7, 2, 1, 4, 3, 6, 5, 5, 3, 1, 6, 4, 2, 9, 7, 8, 6, 4, 2, 9, 7, 8, 5, 3, 1, 9, 7, 8, 5, 3, 1, 6, 4, 2 *)
Solving the empty grid: easy, yet not trivial
(*
2 0 9 0 0 0 0 1 0
0 0 0 0 6 0 0 0 0
0 5 3 8 0 2 7 0 0
3 0 0 0 0 0 0 0 0
0 0 0 0 7 5 0 0 3
0 4 1 2 0 8 9 0 0
0 0 4 0 9 0 0 2 0
8 0 0 0 0 1 0 0 5
0 0 0 0 0 0 0 7 6
*)
A grid known to be solvable
let test1 () raises { NoSolution -> true } = let a = Array.make 81 0 in a[0] <- 2; a[2] <- 9; a[7] <- 1; a[13] <- 6; a[19] <- 5; a[20] <- 3; a[21] <- 8; a[23] <- 2; a[24] <- 7; a[27] <- 3; a[40] <- 7; a[41] <- 5; a[44] <- 3; a[46] <- 4; a[47] <- 1; a[48] <- 2; a[50] <- 8; a[51] <- 9; a[56] <- 4; a[58] <- 9; a[61] <- 2; a[63] <- 8; a[68] <- 1; a[71] <- 5; a[79] <- 7; a[80] <- 6; assert { valid_values a.Array.elts }; solve (classical_sudoku()) a (* the solution: 2, 6, 9, 3, 5, 7, 8, 1, 4, 1, 8, 7, 9, 6, 4, 5, 3, 2, 4, 5, 3, 8, 1, 2, 7, 6, 9, 3, 7, 5, 6, 4, 9, 2, 8, 1, 9, 2, 8, 1, 7, 5, 6, 4, 3, 6, 4, 1, 2, 3, 8, 9, 5, 7, 7, 1, 4, 5, 9, 6, 3, 2, 8, 8, 3, 6, 7, 2, 1, 4, 9, 5, 5, 9, 2, 4, 8, 3, 1, 7, 6 *) let test2 () raises { NoSolution -> true } = let a = Array.make 81 1 in solve (classical_sudoku()) a
A trivially unsolvable grid
end
download ZIP archive