Commit 2491615d authored by MARCHE Claude's avatar MARCHE Claude

miserable attempt to randomize the sudoku solver

parent 4f7e7ef0
......@@ -274,3 +274,9 @@ module null.Null
syntax val get "(fun x -> x)"
end
module random.Random
syntax val random_int "Why3__BigInt.random_int"
end
\ No newline at end of file
......@@ -487,12 +487,119 @@ this is true but with 2 different possible reasons:
raises { NoSolution ->
forall h : grid. included g.elts h /\ full h -> not (valid s h) }
=
if check_valid s g then
try solve_aux s g 0;
raise NoSolution
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
else raise NoSolution
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
......
......@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
endif
MAIN=main
GEN = map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
GEN = map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver sudoku__RandomSolver
OBJ=$(GEN)
GENML = $(addsuffix .ml, $(GEN))
......
......@@ -107,7 +107,7 @@ let solve_board rows _ =
done;
begin
try
let a = Sudoku__Solver.check_then_solve sudoku input_grid in
let a = Sudoku__RandomSolver.check_then_solve sudoku input_grid in
display_sol rows a
with Sudoku__Solver.NoSolution -> no_sol rows
end;
......
......@@ -37,7 +37,7 @@ let print_grid fmt a =
let () =
let sudoku = Sudoku__TheClassicalSudokuGrid.classical_sudoku () in
printf "Problem: %a@." print_grid input_grid;
let a = Sudoku__Solver.solve sudoku input_grid
let a = Sudoku__RandomSolver.solve sudoku input_grid
in
printf "Solution: %a@." print_grid a
......@@ -71,3 +71,11 @@ should give:
5 9 2 4 8 3 1 7 6
*)
(* other tests:
7,0,0,0,0,0,0,0,8,0,9,0,7,0,6,0,3,0,0,0,1,0,0,0,9,0,0,0,7,0,1,0,4,0,5,0,0,0,0,0,6,0,0,0,0,0,5,0,3,0,7,0,1,0,0,0,2,0,0,0,1,0,0,0,1,0,9,0,8,0,7,0,8,0,0,0,0,0,0,0,6
0,0,0,0,0,0,0,0,0,0,0,0,0,0,3,0,8,5,0,0,1,0,2,0,0,0,0,0,0,0,5,0,7,0,0,0,0,0,4,0,0,0,1,0,0,0,9,0,0,0,0,0,0,0,5,0,0,0,0,0,0,7,3,0,0,2,0,1,0,0,0,0,0,0,0,0,4,0,0,0,9
*)
......@@ -73,3 +73,9 @@ let power x y =
let print n = Pervasives.print_string (to_string n)
let chr n = Pervasives.char_of_int (to_int n)
let code c = of_int (Pervasives.int_of_char c)
let random_int n =
try let n = int64_of_big_int n in
if n >= 0L then big_int_of_int64 (Random.int64 n) else raise Exit
with _ -> invalid_arg "Why3__BigInt.random"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment