Wiki Agenda Contact English version

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