Wiki Agenda Contact Version française

A Sudoku solver


Authors: Claude Marché / Guillaume Melquiond

Topics: Array Data Structure

Tools: 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 import int.Int
  use import 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

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 import 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

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

Concrete Values of Chunks for the Classical Sudoku Grid

module TheClassicalSudokuGrid

  use import Grid
  use import map.Map
  use import int.Int

  use import 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 import Grid
  use import array.Array
  use import 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 import 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] = True 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 }

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

  lemma valid_up_to_change :
    forall s:sudoku_chunks, g:grid, i x : int.
      well_formed_sudoku s /\
      is_index i /\ valid_up_to s g i /\ 1 <= x <= 9 /\
      valid_column s (Map.set g i x) i /\
      valid_row s (Map.set g i x) i /\
      valid_square s (Map.set g i x) i
      -> valid_up_to s (Map.set g i x) (i+1)

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
      'L:
      for k = 1 to 9 do
        invariant { grid_eq (at g 'L).elts (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 (at g 'L).elts i k' in
          forall h : grid. included g' h /\ full h -> not (valid s h) }
        g[i] <- k;
        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 (at g '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 g (i + 1)
        with Invalid ->
          assert { (* for completeness *)
            not (valid s (Map.set (at g 'L).elts i k)) };
          assert { (* for completeness *)
            let g' = Map.set (at g 'L).elts 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 (at g 'L).elts h /\ full h ->
          let k' = Map.get h i in
          let g' = Map.set (at g '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 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

(*
module RandomSolver

  (* a variant: solve using a random order of cells *)

  use import Grid
  use import array.Array
  use import int.Int
  use random.Random

  use import 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
      'L:
      for k = 1 to 9 do
        invariant { grid_eq (at g '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 (at g '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 (at g '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 (at g 'L).elts i k)) };
          assert { (* for completeness *)
            let g' = Map.set (at g '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 (at g 'L).elts h /\ full h ->
          let k' = Map.get h i in
          let g' = Map.set (at g '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 import Grid
  use import TheClassicalSudokuGrid

  use import Solver
  use array.Array
  use import map.Map
  use map.Const

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
*)
  constant solvable : grid =
    (Const.const 0)
    [0<-2][2<-9][7<-1]
    [13<-6]
    [19<-5][20<-3][21<-8][23<-2][24<-7]
    [27<-3]
    [40<-7][41<-5][44<-3]
    [46<-4][47<-1][48<-2][50<-8][51<-9]
    [56<-4][58<-9][61<-2]
    [63<-8][68<-1][71<-5]
    [79<-7][80<-6]

  lemma valid_values_solvable: valid_values solvable

  let test1 ()
    raises { NoSolution -> true }
  = let a = Array.make 81 0 in
    for i = 0 to 80 do
      invariant { valid_values a.Array.elts }
      Array.([]<-) a i (Map.get solvable i)
    done;
    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


download ZIP archive