(** {1 An Efficient Sudoku Solver } Author: Claude MarchÃ© (Inria) Guillaume Melquiond (Inria) *) (** {2 A theory of 9x9 grids} *) module Grid use int.Int use map.Map (** A grid is a map from integers to integers *) type grid = map int int (** valid indexes are 0..80 *) predicate is_index (i:int) = 0 <= i < 81 (** valid values are 0..9. 0 denotes an empty cell *) predicate valid_values (g:grid) = forall i. is_index i -> 0 <= g[i] <= 9 (** extensional equality of grids and sub-grids *) predicate grid_eq_sub (g1 g2:grid) (a b:int) = forall j. a <= j < b -> g1[j] = g2[j] 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 (** {3 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; } (** Chunks must point to valid indexes of the grid *) 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 (of the same kind column, row or square) with distinct starting cells must be disjoint *) 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] (** A sudoku grid is well formed when chunks are valid and 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 (** {3 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 occurence 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 (** `valid g` is true when all chunks are valid *) 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 (** `full g` is true when all cells are filled *) predicate full (g : grid) = forall i : int. is_index i -> 1 <= Map.get g i <= 9 (** `included g1 g2` *) 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 (** validity is monotonic w.r.t. inclusion *) 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 lemma subset_valid : forall s g h. well_formed_sudoku s /\ included g h /\ valid s h -> valid s g (** A solution of a grid `data` is a full grid `sol` that is valid and includes `data` *) predicate is_solution_for (s:sudoku_chunks) (sol:grid) (data:grid) = included data sol /\ full sol /\ valid s sol end (** {2 Concrete Values of Chunks for the Classical Sudoku Grid} *) module TheClassicalSudokuGrid 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 (** {2 A Sudoku Solver} *) module Solver use Grid use array.Array use int.Int (** predicate for the loop invariant of next function *) 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 exception Invalid use array.Array (** `check_valid_chunk g i start offsets` checks the validity of the chunk that includes `i` *) 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 (** predicate for the loop invariant of next function *) 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 (** `check_valid s g` checks if the (possibly partially filled) grid `g` is valid. (This function is not needed by the solver) *) 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 (** `full_up_to g i` is true when all cells `0..i-1` in grid `g` are non empty *) predicate full_up_to (g : grid) (i : int) = forall j : int. 0 <= j < i -> 1 <= Map.get g j <= 9 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) } = () (** {3 The main solver loop} *) exception SolutionFound 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 *) (** {2 Some Tests} *) module Test use Grid use TheClassicalSudokuGrid use Solver use map.Map use array.Array (** Solving the empty grid: easy, yet not trivial *) 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 *) (** A grid known to be solvable *) (* 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 *) 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 *) (** A trivially unsolvable grid *) let test2 () raises { NoSolution -> true } = let a = Array.make 81 1 in solve (classical_sudoku()) a end (*** Local Variables: compile-command: "why3 ide --extra-config ../share/strategies.conf sudoku.mlw" End: *)