# Sudoku¶

In this notebook we're going to use Imandra to reason about the classic kind of puzzle that you can find everywhere.

(note: this example was adapted from code from Koen Claessen and Dan Rosén)

We're going to define what a sudoku puzzle is, and how to check if a given sudoku is a solution. From that we can get Imandra to find solutions for us, without actually writing a sudoku solver.

## Helpers¶

We're going to define a sudoku as a 9×9 grid.

### Numbers¶

However, for now, the bounded model checker that comes along with Imandra doesn't handle numbers. We do not need much here besides length, so a unary notation (classic Peano arithmetic) will do.

In :
type nat = Z | S of nat;;

(* readability matters, so we write a pretty-printer for nats *)
let rec int_of_nat = function Z -> 0i | S n -> Caml.Int.(1i + int_of_nat n) [@@program]
let pp_nat out n = Format.fprintf out "%d" (int_of_nat n) [@@program];;
#install_printer pp_nat;;

Out:
type nat = Z | S of nat
val int_of_nat : nat -> int/2 = <fun>
val pp_nat : Format.formatter -> nat -> unit = <fun>

In :
let rec length = function
| [] -> Z
| _ :: tl -> S (length tl)

let n3 = S (S (S Z));;
let n6 = S (S (S n3));;
let n9 = S (S (S n6));;

Out:
val length : 'a list -> nat = <fun>
val n3 : nat = 3
val n6 : nat = 6
val n9 : nat = 9

termination proof

### Termination proof

call length (List.tl _x) from length _x
originallength _x
sublength (List.tl _x)
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 10 arith-max-columns 13 arith-conflicts 1 rlimit count 1912 arith-cheap-eqs 2 mk clause 3 datatype occurs check 22 mk bool var 46 arith-lower 5 datatype splits 3 decisions 10 propagations 1 arith-max-rows 5 conflicts 7 datatype accessor ax 5 datatype constructor ax 8 num allocs 8.39887e+08 final checks 6 added eqs 33 del clause 1 arith eq adapter 3 arith-upper 5 memory 22.14 max memory 24.71
Expand
• start[0.014s]
let (_x_0 : int) = Ordinal.count _x in
let (_x_1 : ty_0 list) = List.tl _x in
let (_x_2 : int) = Ordinal.count _x_1 in
not (_x = []) && _x_0 >= 0 && _x_2 >= 0
==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list) = List.tl _x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count _x in (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (_x = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list_2447| _x_2438) expansions
• unroll
 expr (|count_ty_0 list_2447| (|get.::.1_2433| _x_2438)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_2447| … expansions
• Unsat

### Rows, columns, blocks¶

Sudokus have some constraints that work on rows, and some that work on columns. Using a transpose function we can always work on rows.

In :
(** helper for {!transpose} *)
let rec transpose3 = function
| [] -> []
| [] :: tl -> transpose3 tl
| (_::t) :: tl -> t :: transpose3 tl

| [] -> []
| [] :: tl -> get_heads tl
| (h :: _) :: tl -> h :: get_heads tl
;;

(** We need a custom termination function here *)
let measure_transpose = function
| [] -> 0
| x :: _ -> List.length x
;;

(** Transpose rows and columns in a list of lists *)
let rec transpose l =
match l with
| [] -> []
| [] :: _ -> []
| (x1 :: xs) :: xss ->
(x1 :: get_heads xss) :: transpose (xs :: transpose3 xss)
[@@measure Ordinal.of_int (measure_transpose l)]
;;

Out:
val transpose3 : 'a list list -> 'a list list = <fun>
val get_heads : 'a list list -> 'a list = <fun>
val measure_transpose : 'a list list -> int = <fun>
val transpose : 'a list list -> 'a list list = <fun>

termination proof

### Termination proof

call transpose3 (List.tl _x) from transpose3 _x
originaltranspose3 _x
subtranspose3 (List.tl _x)
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[_x <> [] && List.hd _x = [] && not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.019s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 27 arith-max-columns 19 arith-conflicts 2 rlimit count 6417 mk clause 44 datatype occurs check 46 mk bool var 122 arith-lower 19 datatype splits 11 decisions 36 propagations 77 arith-max-rows 7 conflicts 13 datatype accessor ax 13 datatype constructor ax 20 num allocs 9.16121e+08 final checks 10 added eqs 101 del clause 16 arith eq adapter 13 arith-upper 18 memory 25.58 max memory 25.58
Expand
• start[0.019s]
let (_x_0 : int) = Ordinal.count _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = Ordinal.count _x_1 in
let (_x_3 : bool) = _x_1 <> [] && List.hd _x_1 = [] in
let (_x_4 : bool) = not (_x_1 = []) in
(_x <> [] && List.hd _x = []) && not (_x = []) && _x_0 >= 0 && _x_2 >= 0
==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list list) = List.tl _x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count _x in let (_x_3 : bool) = _x_0 <> [] && List.hd _x_0 = [] in let (_x_4 : bool) = not (_x_0 = []) in (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x_3 && _x_4) && not (not _x_3 && _x_4)) || not ((((_x <> [] && List.hd _x = []) && not (_x = [])) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list list_2495| _x_2484) expansions
• unroll
 expr (|count_ty_0 list list_2495| (|get.::.1_2478| _x_2484)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_2495| … expansions
• Unsat

call transpose3 (List.tl _x) from transpose3 _x
originaltranspose3 _x
subtranspose3 (List.tl _x)
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[not (_x <> [] && List.hd _x = []) && not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.018s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 28 arith-max-columns 19 arith-conflicts 2 rlimit count 3228 mk clause 40 datatype occurs check 43 mk bool var 103 arith-lower 20 datatype splits 10 decisions 44 propagations 71 arith-max-rows 7 conflicts 14 datatype accessor ax 7 datatype constructor ax 14 num allocs 8.92607e+08 final checks 8 added eqs 79 del clause 15 arith eq adapter 14 arith-upper 20 memory 23.03 max memory 24.71
Expand
• start[0.018s]
let (_x_0 : int) = Ordinal.count _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = Ordinal.count _x_1 in
let (_x_3 : bool) = _x_1 <> [] && List.hd _x_1 = [] in
let (_x_4 : bool) = not (_x_1 = []) in
not (_x <> [] && List.hd _x = [])
&& not (_x = []) && _x_0 >= 0 && _x_2 >= 0
==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list list) = List.tl _x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count _x in let (_x_3 : bool) = _x_0 <> [] && List.hd _x_0 = [] in let (_x_4 : bool) = not (_x_0 = []) in (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x_3 && _x_4) && not (not _x_3 && _x_4)) || not (((not (_x <> [] && List.hd _x = []) && not (_x = [])) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list list_2495| _x_2484) expansions
• unroll
 expr (|count_ty_0 list list_2495| (|get.::.1_2478| _x_2484)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_2495| … expansions
• Unsat

termination proof

### Termination proof

call get_heads (List.tl _x) from get_heads _x
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[_x <> [] && List.hd _x = [] && not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.037s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 27 arith-max-columns 19 arith-conflicts 2 rlimit count 6425 mk clause 44 datatype occurs check 46 mk bool var 122 arith-lower 19 datatype splits 11 decisions 36 propagations 77 arith-max-rows 7 conflicts 13 datatype accessor ax 13 datatype constructor ax 20 num allocs 1.03943e+09 final checks 10 added eqs 101 del clause 16 arith eq adapter 13 arith-upper 18 memory 23.41 max memory 25.9
Expand
• start[0.037s]
let (_x_0 : int) = Ordinal.count _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = Ordinal.count _x_1 in
let (_x_3 : bool) = _x_1 <> [] && List.hd _x_1 = [] in
let (_x_4 : bool) = not (_x_1 = []) in
(_x <> [] && List.hd _x = []) && not (_x = []) && _x_0 >= 0 && _x_2 >= 0
==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list list) = List.tl _x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count _x in let (_x_3 : bool) = _x_0 <> [] && List.hd _x_0 = [] in let (_x_4 : bool) = not (_x_0 = []) in (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x_3 && _x_4) && not (not _x_3 && _x_4)) || not ((((_x <> [] && List.hd _x = []) && not (_x = [])) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list list_2586| _x_2575) expansions
• unroll
 expr (|count_ty_0 list list_2586| (|get.::.1_2569| _x_2575)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_2586| … expansions
• Unsat

call get_heads (List.tl _x) from get_heads _x
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[not (_x <> [] && List.hd _x = []) && not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.033s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 28 arith-max-columns 19 arith-conflicts 2 rlimit count 3228 mk clause 40 datatype occurs check 43 mk bool var 103 arith-lower 20 datatype splits 10 decisions 44 propagations 71 arith-max-rows 7 conflicts 14 datatype accessor ax 7 datatype constructor ax 14 num allocs 9.90752e+08 final checks 8 added eqs 79 del clause 15 arith eq adapter 14 arith-upper 20 memory 23.32 max memory 25.68
Expand
• start[0.033s]
let (_x_0 : int) = Ordinal.count _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = Ordinal.count _x_1 in
let (_x_3 : bool) = _x_1 <> [] && List.hd _x_1 = [] in
let (_x_4 : bool) = not (_x_1 = []) in
not (_x <> [] && List.hd _x = [])
&& not (_x = []) && _x_0 >= 0 && _x_2 >= 0
==> not (_x_3 && _x_4) && not (not _x_3 && _x_4)
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list list) = List.tl _x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count _x in let (_x_3 : bool) = _x_0 <> [] && List.hd _x_0 = [] in let (_x_4 : bool) = not (_x_0 = []) in (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x_3 && _x_4) && not (not _x_3 && _x_4)) || not (((not (_x <> [] && List.hd _x = []) && not (_x = [])) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list list_2586| _x_2575) expansions
• unroll
 expr (|count_ty_0 list list_2586| (|get.::.1_2569| _x_2575)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_2586| … expansions
• Unsat

termination proof

### Termination proof

call transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) from transpose l
originaltranspose l
subtranspose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))
original ordinallet (_x_0 : int) = measure_transpose l in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
sub ordinallet (_x_0 : int) = measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
path[not (l <> [] && List.hd l = []) && not (l = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 12 arith-max-columns 11 arith-conflicts 1 rlimit count 2507 mk clause 6 datatype occurs check 52 mk bool var 65 arith-lower 3 datatype splits 11 decisions 17 propagations 4 arith-max-rows 4 conflicts 8 datatype accessor ax 8 datatype constructor ax 16 num allocs 1.0686e+09 final checks 11 added eqs 50 del clause 6 arith eq adapter 2 arith-upper 5 memory 26.41 max memory 26.41
Expand
• start[0.015s]
let (_x_0 : ty_0 list) = List.hd l in
let (_x_1 : bool) = l = [] in
let (_x_2 : int) = if _x_1 then 0 else List.length _x_0 in
let (_x_3 : int) = if _x_2 >= 0 then _x_2 else 0 in
let (_x_4 : ty_0 list) = List.tl _x_0 in
let (_x_5 : bool) = _x_4 :: (transpose3 …) = [] in
let (_x_6 : int) = if _x_5 then 0 else List.length … in
let (_x_7 : int) = if _x_6 >= 0 then _x_6 else 0 in
not (l <> [] && _x_0 = []) && not _x_1 && _x_3 >= 0 && _x_7 >= 0
==> not (not (true && _x_4 = []) && not _x_5)
|| Ordinal.( << ) (Ordinal.Int _x_7) (Ordinal.Int _x_3)
• ##### simplify
 into let (_x_0 : ty_0 list) = List.hd l in let (_x_1 : ty_0 list) = List.tl _x_0 in let (_x_2 : int) = List.length _x_1 in let (_x_3 : int) = List.length _x_0 in let (_x_4 : bool) = l = [] in let (_x_5 : bool) = _x_4 || _x_3 >= 0 in (_x_1 = [] || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0)) (Ordinal.Int (if _x_5 then if _x_4 then 0 else _x_3 else 0))) || not ((not (l <> [] && _x_0 = []) && not _x_4) && (_x_5 || not _x_5)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|List.length_2715| (|get.::.0_2691| l_2708)) expansions
• unroll
 expr (|List.length_2715| (|get.::.1_2689| (|get.::.0_2691| l_2708))) expansions
• unroll
 expr (let ((a!1 (>= (|List.length_2715| (|get.::.1_2689| (|get.::.0_2691| l_2708))) 0)) … expansions
• Unsat

Now we also need to extract 3×3 blocks for the additional constraint that none of them contains a duplicate.

This require a few helpers on lists and options, nothing too complicated.

In :
let rec take (x:nat) l : _ list =
match x with
| Z -> []
| S x' ->
match l with
| [] -> []
| y :: tl -> y :: take x' tl

let rec drop x y =
match x with
| Z -> y
| S x' ->
match y with
| [] -> []
| _ :: y' -> drop x' y'

let rec elem x y =  match y with [] -> false | z :: ys -> x=z || elem x ys ;;

(** Is the list [l] composed of unique elements (without duplicates)? *)
let rec unique x : bool =
match x with
| [] -> true
| y :: xs -> not (elem y xs) && unique xs
;;

(** Keep the elements that are [Some _], drop the others *)
let rec keep_some_list l =
match l with
| [] -> []
| y :: tail ->
let tail = keep_some_list tail in
match y with None -> tail | Some x -> x :: tail
;;

(** A block is valid if it doesn't contain duplicates *)
let block_satisfies_constraints x = unique (keep_some_list x) ;;

let rec blocks_3_34 = function
| [] -> []
| y :: z -> drop n6 y :: blocks_3_34 z
;;

let rec blocks_3_33 = function
| [] -> []
| y :: z -> take n3 (drop n3 y) :: blocks_3_33 z
;;

let rec blocks_3_32 = function
| [] -> []
| y :: z -> take n3 y :: blocks_3_32 z
;;

(*

let rec group3 = function
| xs1 :: xs2 :: xs3 :: xss ->
(xs1 @ xs2 @ xs3) :: (group3 xss)
| _ -> []
;;
*)

let rec group3 = function
| [] -> []
| xs1 :: y ->
match y with
| [] -> []
| xs2 :: z ->
match z with
| [] -> []
| xs3 :: xss -> (xs1 @ xs2 @ xs3) :: (group3 xss)
;;

let blocks_3_3 l =
group3 (blocks_3_32 l) @
group3 (blocks_3_33 l) @
group3 (blocks_3_34 l)
;;

Out:
val take : nat -> 'a list -> 'a list = <fun>
val drop : nat -> 'a list -> 'a list = <fun>
val elem : 'a -> 'a list -> bool = <fun>
val unique : 'a list -> bool = <fun>
val keep_some_list : 'a option list -> 'a list = <fun>
val block_satisfies_constraints : 'a option list -> bool = <fun>
val blocks_3_34 : 'a list list -> 'a list list = <fun>
val blocks_3_33 : 'a list list -> 'a list list = <fun>
val blocks_3_32 : 'a list list -> 'a list list = <fun>
val group3 : 'a list list -> 'a list list = <fun>
val blocks_3_3 : 'a list list -> 'a list list = <fun>

termination proof

### Termination proof

call take (Destruct(S, 0, x)) (List.tl l) from take x l
originaltake x l
subtake (Destruct(S, 0, x)) (List.tl l)
original ordinalOrdinal.Int (Ordinal.count x)
sub ordinalOrdinal.Int (Ordinal.count (Destruct(S, 0, x)))
path[not (l = []) && not (x = Z)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 10 arith-max-columns 13 arith-conflicts 1 rlimit count 2114 mk clause 3 datatype occurs check 34 mk bool var 62 arith-lower 4 datatype splits 6 decisions 16 propagations 2 arith-max-rows 5 conflicts 10 datatype accessor ax 8 datatype constructor ax 16 num allocs 1.12309e+09 final checks 6 added eqs 50 del clause 1 arith eq adapter 3 arith-upper 6 memory 26.72 max memory 26.72
Expand
• start[0.014s]
let (_x_0 : int) = Ordinal.count x in
let (_x_1 : nat) = Destruct(S, 0, x) in
let (_x_2 : int) = Ordinal.count _x_1 in
not (l = []) && not (x = Z) && _x_0 >= 0 && _x_2 >= 0
==> not (not (List.tl l = []) && not (_x_1 = Z))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : nat) = Destruct(S, 0, x) in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count x in (not (not (List.tl l = []) && not (_x_0 = Z)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not (l = []) && not (x = Z)) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (count_nat_2795 x_2784) expansions
• unroll
 expr (count_nat_2795 (|get.S.0_2774| x_2784)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (count_nat_2795 (|get.S.0_2774| x_2784))) (|Or… expansions
• Unsat

termination proof

### Termination proof

call drop (Destruct(S, 0, x)) (List.tl y) from drop x y
originaldrop x y
subdrop (Destruct(S, 0, x)) (List.tl y)
original ordinalOrdinal.Int (Ordinal.count x)
sub ordinalOrdinal.Int (Ordinal.count (Destruct(S, 0, x)))
path[not (y = []) && not (x = Z)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 10 arith-max-columns 13 arith-conflicts 1 rlimit count 2114 mk clause 3 datatype occurs check 34 mk bool var 62 arith-lower 4 datatype splits 6 decisions 16 propagations 2 arith-max-rows 5 conflicts 10 datatype accessor ax 8 datatype constructor ax 16 num allocs 1.1778e+09 final checks 6 added eqs 50 del clause 1 arith eq adapter 3 arith-upper 6 memory 26.99 max memory 26.99
Expand
• start[0.013s]
let (_x_0 : int) = Ordinal.count x in
let (_x_1 : nat) = Destruct(S, 0, x) in
let (_x_2 : int) = Ordinal.count _x_1 in
not (y = []) && not (x = Z) && _x_0 >= 0 && _x_2 >= 0
==> not (not (List.tl y = []) && not (_x_1 = Z))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : nat) = Destruct(S, 0, x) in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count x in (not (not (List.tl y = []) && not (_x_0 = Z)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not (y = []) && not (x = Z)) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (count_nat_2839 x_2828) expansions
• unroll
 expr (count_nat_2839 (|get.S.0_2819| x_2828)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (count_nat_2839 (|get.S.0_2819| x_2828))) (|Or… expansions
• Unsat

termination proof

### Termination proof

call elem x (List.tl y) from elem x y
originalelem x y
subelem x (List.tl y)
original ordinalOrdinal.Int (Ordinal.count y)
sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
path[not (x = List.hd y) && not (y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 9 arith-max-columns 13 arith-conflicts 1 rlimit count 2026 arith-cheap-eqs 2 mk clause 3 datatype occurs check 19 mk bool var 48 arith-lower 5 datatype splits 3 decisions 10 propagations 1 arith-max-rows 5 conflicts 7 datatype accessor ax 5 datatype constructor ax 8 num allocs 1.23262e+09 final checks 5 added eqs 33 del clause 1 arith eq adapter 3 arith-upper 5 memory 27.14 max memory 27.14
Expand
• start[0.014s]
let (_x_0 : int) = Ordinal.count y in
let (_x_1 : ty_0 list) = List.tl y in
let (_x_2 : int) = Ordinal.count _x_1 in
not (x = List.hd y) && not (y = []) && _x_0 >= 0 && _x_2 >= 0
==> not (not (x = List.hd _x_1) && not (_x_1 = []))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list) = List.tl y in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count y in (not (not (x = List.hd _x_0) && not (_x_0 = [])) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not (x = List.hd y) && not (y = [])) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list_2882| y_2872) expansions
• unroll
 expr (|count_ty_0 list_2882| (|get.::.1_2865| y_2872)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_2882| … expansions
• Unsat

termination proof

### Termination proof

call unique (List.tl x) from unique x
originalunique x
subunique (List.tl x)
original ordinalOrdinal.Int (Ordinal.count x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
path[not (elem (List.hd x) (List.tl x)) && not (x = [])]
proof
detailed proof
ground_instances4
definitions0
inductions0
search_time
0.020s
details
Expand
smt_stats
 num checks 9 arith-make-feasible 10 arith-max-columns 13 arith-conflicts 1 rlimit count 2389 arith-cheap-eqs 2 mk clause 3 datatype occurs check 22 mk bool var 52 arith-lower 5 datatype splits 3 decisions 10 propagations 1 arith-max-rows 5 conflicts 7 datatype accessor ax 5 datatype constructor ax 8 num allocs 1.31596e+09 final checks 6 added eqs 32 del clause 1 arith eq adapter 3 arith-upper 5 memory 24.94 max memory 27.24
Expand
• start[0.020s]
let (_x_0 : ty_0 list) = List.tl x in
let (_x_1 : int) = Ordinal.count x in
let (_x_2 : int) = Ordinal.count _x_0 in
not (elem (List.hd x) _x_0) && not (x = []) && _x_1 >= 0 && _x_2 >= 0
==> not (not (elem (List.hd _x_0) (List.tl _x_0)) && not (_x_0 = []))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_1)
• ##### simplify
 into let (_x_0 : ty_0 list) = List.tl x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count x in (not (not (elem (List.hd _x_0) (List.tl _x_0)) && not (_x_0 = [])) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not (elem (List.hd x) _x_0) && not (x = [])) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (elem_2912 (|get.::.0_2906| x_2917) (|get.::.1_2907| x_2917)) expansions
• unroll
 expr (|count_ty_0 list_2926| x_2917) expansions
• unroll
 expr (|count_ty_0 list_2926| (|get.::.1_2907| x_2917)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_2926| … expansions
• Unsat

termination proof

### Termination proof

call keep_some_list (List.tl l) from keep_some_list l
originalkeep_some_list l
subkeep_some_list (List.tl l)
original ordinalOrdinal.Int (Ordinal.count l)
sub ordinalOrdinal.Int (Ordinal.count (List.tl l))
path[not (l = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 10 arith-max-columns 13 arith-conflicts 1 rlimit count 2038 mk clause 3 datatype occurs check 36 mk bool var 58 arith-lower 5 datatype splits 9 decisions 17 propagations 1 arith-max-rows 5 conflicts 7 datatype accessor ax 8 datatype constructor ax 14 num allocs 1.40102e+09 final checks 8 added eqs 43 del clause 1 arith eq adapter 3 arith-upper 5 memory 22.5 max memory 27.24
Expand
• start[0.014s]
let (_x_0 : int) = Ordinal.count l in
let (_x_1 : ty_0 option list) = List.tl l in
let (_x_2 : int) = Ordinal.count _x_1 in
not (l = []) && _x_0 >= 0 && _x_2 >= 0
==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 option list) = List.tl l in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count l in (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (l = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 option list_2973| l_2964) expansions
• unroll
 expr (|count_ty_0 option list_2973| (|get.::.1_2954| l_2964)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 option list_2973| … expansions
• Unsat

termination proof

### Termination proof

call blocks_3_34 (List.tl _x) from blocks_3_34 _x
originalblocks_3_34 _x
subblocks_3_34 (List.tl _x)
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.022s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 26 arith-max-columns 19 arith-conflicts 3 rlimit count 2870 mk clause 22 datatype occurs check 52 mk bool var 112 arith-lower 18 arith-diseq 2 datatype splits 14 decisions 34 propagations 14 arith-max-rows 7 conflicts 14 datatype accessor ax 12 datatype constructor ax 23 num allocs 1.46154e+09 final checks 11 added eqs 83 del clause 7 arith eq adapter 15 arith-upper 16 memory 23.02 max memory 27.24
Expand
• start[0.022s]
let (_x_0 : int) = Ordinal.count _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = Ordinal.count _x_1 in
not (_x = []) && _x_0 >= 0 && _x_2 >= 0
==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list list) = List.tl _x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count _x in (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (_x = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list list_3050| _x_3041) expansions
• unroll
 expr (|count_ty_0 list list_3050| (|get.::.1_3030| _x_3041)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_3050| … expansions
• Unsat

termination proof

### Termination proof

call blocks_3_33 (List.tl _x) from blocks_3_33 _x
originalblocks_3_33 _x
subblocks_3_33 (List.tl _x)
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.019s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 26 arith-max-columns 19 arith-conflicts 3 rlimit count 2870 mk clause 22 datatype occurs check 52 mk bool var 112 arith-lower 18 arith-diseq 2 datatype splits 14 decisions 34 propagations 14 arith-max-rows 7 conflicts 14 datatype accessor ax 12 datatype constructor ax 23 num allocs 1.49425e+09 final checks 11 added eqs 83 del clause 7 arith eq adapter 15 arith-upper 16 memory 25.89 max memory 27.24
Expand
• start[0.019s]
let (_x_0 : int) = Ordinal.count _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = Ordinal.count _x_1 in
not (_x = []) && _x_0 >= 0 && _x_2 >= 0
==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list list) = List.tl _x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count _x in (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (_x = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list list_3106| _x_3097) expansions
• unroll
 expr (|count_ty_0 list list_3106| (|get.::.1_3080| _x_3097)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_3106| … expansions
• Unsat

termination proof

### Termination proof

call blocks_3_32 (List.tl _x) from blocks_3_32 _x
originalblocks_3_32 _x
subblocks_3_32 (List.tl _x)
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl _x))
path[not (_x = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.021s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 26 arith-max-columns 19 arith-conflicts 3 rlimit count 2870 mk clause 22 datatype occurs check 52 mk bool var 112 arith-lower 18 arith-diseq 2 datatype splits 14 decisions 34 propagations 14 arith-max-rows 7 conflicts 14 datatype accessor ax 12 datatype constructor ax 23 num allocs 1.61213e+09 final checks 11 added eqs 83 del clause 7 arith eq adapter 15 arith-upper 16 memory 20.85 max memory 27.24
Expand
• start[0.021s]
let (_x_0 : int) = Ordinal.count _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = Ordinal.count _x_1 in
not (_x = []) && _x_0 >= 0 && _x_2 >= 0
==> _x_1 = [] || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list list) = List.tl _x in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count _x in (_x_0 = [] || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (_x = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list list_3157| _x_3148) expansions
• unroll
 expr (|count_ty_0 list list_3157| (|get.::.1_3136| _x_3148)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_3157| … expansions
• Unsat

termination proof

### Termination proof

call group3 (List.tl (List.tl (List.tl _x))) from group3 _x
originalgroup3 _x
subgroup3 (List.tl (List.tl (List.tl _x)))
original ordinalOrdinal.Int (Ordinal.count _x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x))))
path[not (List.tl (List.tl _x) = []) && not (List.tl _x = []) && not (_x = [])]
proof
detailed proof
ground_instances8
definitions0
inductions0
search_time
0.028s
details
Expand
smt_stats
 num checks 18 arith-make-feasible 198 arith-max-columns 53 arith-conflicts 13 rlimit count 11790 arith-cheap-eqs 31 mk clause 188 datatype occurs check 98 mk bool var 531 arith-lower 150 arith-diseq 20 datatype splits 33 decisions 312 arith-propagations 18 propagations 203 arith-bound-propagations-cheap 18 arith-max-rows 25 conflicts 46 datatype accessor ax 31 minimized lits 5 arith-bound-propagations-lp 7 datatype constructor ax 117 num allocs 1.7092e+09 final checks 18 added eqs 564 del clause 105 arith eq adapter 121 arith-upper 172 memory 18.96 max memory 27.24
Expand
• start[0.028s]
let (_x_0 : ty_0 list list) = List.tl _x in
let (_x_1 : ty_0 list list) = List.tl _x_0 in
let (_x_2 : int) = Ordinal.count _x in
let (_x_3 : ty_0 list list) = List.tl _x_1 in
let (_x_4 : int) = Ordinal.count _x_3 in
let (_x_5 : ty_0 list list) = List.tl _x_3 in
not (_x_1 = [])
&& not (_x_0 = []) && not (_x = []) && _x_2 >= 0 && _x_4 >= 0
==> not (not (List.tl _x_5 = []) && not (_x_5 = []) && not (_x_3 = []))
|| Ordinal.( << ) (Ordinal.Int _x_4) (Ordinal.Int _x_2)
• ##### simplify
 into let (_x_0 : ty_0 list list) = List.tl _x in let (_x_1 : ty_0 list list) = List.tl _x_0 in let (_x_2 : ty_0 list list) = List.tl _x_1 in let (_x_3 : int) = Ordinal.count _x_2 in let (_x_4 : int) = Ordinal.count _x in let (_x_5 : ty_0 list list) = List.tl _x_2 in (Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4) || not ((not (List.tl _x_5 = []) && not (_x_5 = [])) && not (_x_2 = []))) || not ((((not (_x_1 = []) && not (_x_0 = [])) && not (_x = [])) && _x_4 >= 0) && _x_3 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list list_3210| _x_3201) expansions
• unroll
 expr (|count_ty_0 list list_3210| (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_3187| _x_3201)))) expansions
• unroll
 expr (let ((a!1 (|count_ty_0 list list_3210| (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_… expansions
• unroll
 expr (|count_ty_0 list list_3210| (|get.::.1_3187| _x_3201)) expansions
• unroll
 expr (|count_ty_0 list_3212| (|get.::.0_3186| _x_3201)) expansions
• unroll
 expr (let ((a!1 (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_3187| _x_3201)))))) (|cou… expansions
• unroll
 expr (let ((a!1 (|get.::.0_3186| (|get.::.1_3187| (|get.::.1_3187| (|get.::.1_3187| _x_3201)))))) (|cou… expansions
• unroll
 expr (|count_ty_0 list list_3210| (|get.::.1_3187| (|get.::.1_3187| _x_3201))) expansions
• Unsat

## The Sudoku type¶

We're ready to define the sudoku as a list of lists of (possibly empty) cells.

First, cells are just an enumeration of 9 distinct cases:

In :
type cell = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 ;;

(* let us also write a nice printer for cells. We will put
it to good use later. *)
let doc_of_cell c =
Document.s (match c with C1->"1"|C2->"2"|C3->"3"|C4->"4"|C5->"5"|C6->"6"|C7->"7"|C8->"8"|C9->"9") [@@program];;

#install_doc doc_of_cell;;

Out:
type cell = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9
val doc_of_cell : cell -> Document.t = <fun>


And the sudoku itself:

In :
type sudoku = { rows: cell option list list } ;;

(* now install a nice printer for sudoku grids *)
let doc_of_sudoku (s:sudoku) : Document.t =
let module D = Document in
let d_of_c = function None -> D.s "·" | Some c -> doc_of_cell c in
D.tbl_of d_of_c s.rows [@@program]
;;

#install_doc doc_of_sudoku;;

Out:
type sudoku = { rows : cell option list list; }
val doc_of_sudoku : sudoku -> Document.t = <fun>


We're going to solve the following instance (still from Dan Rosén and Koen Claessen's code). The custom printer we installed earlier shows the grid in a readable way.

In :
let the_problem : sudoku =
{rows=
[ [ (Some C8) ; None ; None ; None ; None ; None ; None ; None ; None ];
[ None ; None ; (Some C3) ; (Some C6) ; None ; None ; None ; None ; None ];
[ None ; (Some C7) ; None ; None ; (Some C9) ; None ; (Some C2) ; None ; None ];
[ None ; (Some C5) ; None ; None ; None ; (Some C7) ; None ; None ; None ];
[ None ; None ; None ; None ; (Some C4) ; (Some C5) ; (Some C7) ; None ; None ];
[ None ; None ; None ; (Some C1) ; None ; None ; None ; (Some C3) ; None ];
[ None ; None ; (Some C1) ; None ; None ; None ; None ; (Some C6) ; (Some C8); ];
[ None ; None ; (Some C8) ; (Some C5) ; None ; None ; None ; (Some C1) ; None ];
[ None ; (Some C9) ; None ; None ; None ; None ; (Some C4) ; None ; None ];
]}
;;

Out:
val the_problem : sudoku = <document>

 8 · · · · · · · · · · 3 6 · · · · · · 7 · · 9 · 2 · · · 5 · · · 7 · · · · · · · 4 5 7 · · · · · 1 · · · 3 · · · 1 · · · · 6 8 · · 8 5 · · · 1 · · 9 · · · · 4 · ·
In :
(** All the relevant blocks: rows, columns, and 3×3 sub-squares *)
let blocks (x:sudoku) =
x.rows @ transpose x.rows @ blocks_3_3 x.rows

(** Are all constraints satisfied? *)
let satisfies_constraints (x:sudoku) = List.for_all block_satisfies_constraints (blocks x);;

(** is a sudoku entirely defined (all cells are filled)? *)
let is_solved (x:sudoku) =
List.for_all (List.for_all Option.is_some) x.rows;;

(** Is [x] of the correct shape, i.e. a 9×9 grid? *)
let is_valid_sudoku (x:sudoku) =
length x.rows = n9 &&
List.for_all (fun col -> length col = n9) x.rows
;;

Out:
val blocks : sudoku -> cell option list list = <fun>
val satisfies_constraints : sudoku -> bool = <fun>
val is_solved : sudoku -> bool = <fun>
val is_valid_sudoku : sudoku -> bool = <fun>


We have a template (the initial problem) and we want to solve it. It means the sudoku we're looking for must be:

• solved (all cells are Some _ rather than None)
• a solution of the template (i.e. cells defined in the template must match)
In :
(** Combine lists together *)
let rec zip l1 l2 = match l1, l2 with
| [], _ | _, [] -> []
| x1::tl1, x2 :: tl2 -> (x1,x2) :: zip tl1 tl2

let rec match_cols y =
match y with
| [] -> true
| z :: x2 ->
match z with
| None,_ | _, None -> match_cols x2
| (Some n1,Some n2) -> n1=n2 && match_cols x2
;;

let rec match_rows x =
match x with
| [] -> true
| (row1,row2) :: z -> match_cols (zip row1 row2) && match_rows z
;;

(** is [x] a solution of [y]? We check that each cell in each rows,
if defined in [y], has the same value in [x] *)
let is_solution_of (x:sudoku) (y:sudoku) : bool =
is_solved x &&
satisfies_constraints x &&
match_rows (zip x.rows y.rows)

Out:
val zip : 'a list -> 'b list -> ('a * 'b) list = <fun>
val match_cols : ('a option * 'a option) list -> bool = <fun>
val match_rows : ('a option list * 'a option list) list -> bool = <fun>
val is_solution_of : sudoku -> sudoku -> bool = <fun>

termination proof

### Termination proof

call zip (List.tl l1) (List.tl l2) from zip l1 l2
originalzip l1 l2
subzip (List.tl l1) (List.tl l2)
original ordinalOrdinal.Int (Ordinal.count l1)
sub ordinalOrdinal.Int (Ordinal.count (List.tl l1))
path[not (l1 = [] || l2 = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 10 arith-max-columns 13 arith-conflicts 1 rlimit count 2108 mk clause 3 datatype occurs check 34 mk bool var 64 arith-lower 4 datatype splits 6 decisions 16 propagations 2 arith-max-rows 5 conflicts 10 datatype accessor ax 8 datatype constructor ax 16 num allocs 1.82514e+09 final checks 6 added eqs 52 del clause 1 arith eq adapter 3 arith-upper 6 memory 17.87 max memory 27.24
Expand
• start[0.014s]
let (_x_0 : int) = Ordinal.count l1 in
let (_x_1 : ty_0 list) = List.tl l1 in
let (_x_2 : int) = Ordinal.count _x_1 in
not (l1 = [] || l2 = []) && _x_0 >= 0 && _x_2 >= 0
==> (_x_1 = [] || List.tl l2 = [])
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list) = List.tl l1 in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count l1 in ((_x_0 = [] || List.tl l2 = []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not (l1 = [] || l2 = []) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_ty_0 list_3559| l1_3548) expansions
• unroll
 expr (|count_ty_0 list_3559| (|get.::.1_3530| l1_3548)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_3559| … expansions
• Unsat

termination proof

### Termination proof

call match_cols (List.tl y) from match_cols y
originalmatch_cols y
submatch_cols (List.tl y)
original ordinalOrdinal.Int (Ordinal.count y)
sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
path[let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in _x_0.0 = None || _x_0.1 = None && not (y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 10 arith-max-columns 13 arith-conflicts 1 rlimit count 5750 mk clause 28 datatype occurs check 59 mk bool var 143 arith-lower 4 datatype splits 23 decisions 32 propagations 57 arith-max-rows 5 conflicts 12 datatype accessor ax 26 datatype constructor ax 33 num allocs 1.92451e+09 final checks 10 added eqs 147 del clause 2 arith eq adapter 3 arith-upper 6 memory 20.69 max memory 27.24
Expand
• start[0.014s]
let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
let (_x_1 : int) = Ordinal.count y in
let (_x_2 : (ty_0 option * ty_0 option) list) = List.tl y in
let (_x_3 : int) = Ordinal.count _x_2 in
let (_x_4 : (ty_0 option * ty_0 option)) = List.hd _x_2 in
let (_x_5 : ty_0 option) = _x_4.0 in
let (_x_6 : ty_0 option) = _x_4.1 in
let (_x_7 : bool) = _x_5 = None || _x_6 = None in
let (_x_8 : bool) = not (_x_2 = []) in
(_x_0.0 = None || _x_0.1 = None) && not (y = []) && _x_1 >= 0 && _x_3 >= 0
==> not (_x_7 && _x_8)
&& not (Option.get _x_5 = Option.get _x_6 && not _x_7 && _x_8)
|| Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
• ##### simplify
 into let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count y in let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_0 in let (_x_4 : ty_0 option) = _x_3.0 in let (_x_5 : ty_0 option) = _x_3.1 in let (_x_6 : bool) = _x_4 = None || _x_5 = None in let (_x_7 : bool) = not (_x_0 = []) in let (_x_8 : (ty_0 option * ty_0 option)) = List.hd y in (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x_6 && _x_7) && not ((Option.get _x_4 = Option.get _x_5 && not _x_6) && _x_7)) || not ((((_x_8.0 = None || _x_8.1 = None) && not (y = [])) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_(ty_0 option * ty_0 option) list_3608| y_3597) expansions
• unroll
 expr (|count_(ty_0 option * ty_0 option) list_3608| (|get.::.1_3590| y_3597)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_(ty_0 option * ty_0 option) list_3608| … expansions
• Unsat

call match_cols (List.tl y) from match_cols y
originalmatch_cols y
submatch_cols (List.tl y)
original ordinalOrdinal.Int (Ordinal.count y)
sub ordinalOrdinal.Int (Ordinal.count (List.tl y))
path[let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in Option.get _x_0.0 = Option.get _x_0.1 && let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in not (_x_0.0 = None || _x_0.1 = None) && not (y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 11 arith-max-columns 12 arith-conflicts 1 rlimit count 2930 mk clause 26 datatype occurs check 78 mk bool var 139 arith-lower 5 datatype splits 26 decisions 31 propagations 57 arith-max-rows 4 conflicts 13 datatype accessor ax 25 datatype constructor ax 33 num allocs 1.89178e+09 final checks 11 added eqs 142 del clause 2 arith eq adapter 3 arith-upper 5 memory 18.13 max memory 27.24
Expand
• start[0.015s]
let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
let (_x_1 : ty_0 option) = _x_0.0 in
let (_x_2 : ty_0 option) = _x_0.1 in
let (_x_3 : int) = Ordinal.count y in
let (_x_4 : (ty_0 option * ty_0 option) list) = List.tl y in
let (_x_5 : int) = Ordinal.count _x_4 in
let (_x_6 : (ty_0 option * ty_0 option)) = List.hd _x_4 in
let (_x_7 : ty_0 option) = _x_6.0 in
let (_x_8 : ty_0 option) = _x_6.1 in
let (_x_9 : bool) = _x_7 = None || _x_8 = None in
let (_x_10 : bool) = not (_x_4 = []) in
Option.get _x_1 = Option.get _x_2
&& not (_x_1 = None || _x_2 = None)
&& not (y = []) && _x_3 >= 0 && _x_5 >= 0
==> not (_x_9 && _x_10)
&& not (Option.get _x_7 = Option.get _x_8 && not _x_9 && _x_10)
|| Ordinal.( << ) (Ordinal.Int _x_5) (Ordinal.Int _x_3)
• ##### simplify
 into let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in let (_x_1 : int) = Ordinal.count _x_0 in let (_x_2 : int) = Ordinal.count y in let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_0 in let (_x_4 : ty_0 option) = _x_3.0 in let (_x_5 : ty_0 option) = _x_3.1 in let (_x_6 : bool) = _x_4 = None || _x_5 = None in let (_x_7 : bool) = not (_x_0 = []) in let (_x_8 : (ty_0 option * ty_0 option)) = List.hd y in let (_x_9 : ty_0 option) = _x_8.0 in let (_x_10 : ty_0 option) = _x_8.1 in (Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x_6 && _x_7) && not ((Option.get _x_4 = Option.get _x_5 && not _x_6) && _x_7)) || not ((((Option.get _x_9 = Option.get _x_10 && not (_x_9 = None || _x_10 = None)) && not (y = [])) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count_(ty_0 option * ty_0 option) list_3608| y_3597) expansions
• unroll
 expr (|count_(ty_0 option * ty_0 option) list_3608| (|get.::.1_3590| y_3597)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_(ty_0 option * ty_0 option) list_3608| … expansions
• Unsat

termination proof

### Termination proof

call match_rows (List.tl x) from match_rows x
originalmatch_rows x
submatch_rows (List.tl x)
original ordinalOrdinal.Int (Ordinal.count x)
sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
path[let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in match_cols (zip _x_0.0 _x_0.1) && not (x = [])]
proof
detailed proof
ground_instances5
definitions0
inductions0
search_time
0.022s
details
Expand
smt_stats
 num checks 12 arith-assume-eqs 2 arith-make-feasible 59 arith-max-columns 37 arith-conflicts 5 rlimit count 8054 arith-cheap-eqs 3 mk clause 89 datatype occurs check 173 mk bool var 354 arith-lower 39 arith-diseq 4 datatype splits 61 decisions 174 arith-propagations 2 propagations 90 interface eqs 2 arith-bound-propagations-cheap 2 arith-max-rows 19 conflicts 26 datatype accessor ax 33 minimized lits 1 datatype constructor ax 92 num allocs 2.02915e+09 final checks 17 added eqs 358 del clause 30 arith eq adapter 33 arith-upper 41 memory 18.74 max memory 27.24
Expand
• start[0.022s]
let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in
let (_x_1 : int) = Ordinal.count x in
let (_x_2 : (ty_0 option list * ty_0 option list) list) = List.tl x in
let (_x_3 : int) = Ordinal.count _x_2 in
let (_x_4 : (ty_0 option list * ty_0 option list)) = List.hd _x_2 in
match_cols (zip _x_0.0 _x_0.1) && not (x = []) && _x_1 >= 0 && _x_3 >= 0
==> not (match_cols (zip _x_4.0 _x_4.1) && not (_x_2 = []))
|| Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_1)
• ##### simplify
 into let (_x_0 : (ty_0 option list * ty_0 option list) list) = List.tl x in let (_x_1 : (ty_0 option list * ty_0 option list)) = List.hd _x_0 in let (_x_2 : int) = Ordinal.count _x_0 in let (_x_3 : int) = Ordinal.count x in let (_x_4 : (ty_0 option list * ty_0 option list)) = List.hd x in (not (match_cols (zip _x_1.0 _x_1.1) && not (_x_0 = [])) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3)) || not (((match_cols (zip _x_4.0 _x_4.1) && not (x = [])) && _x_3 >= 0) && _x_2 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (zip_3766 (|tuple_get.0_3749| (|get.::.0_3752| x_3779)) (|tuple_get.1_3750| (|get.::.0_375… expansions
• unroll
 expr (match_cols_3773 (zip_3766 (|tuple_get.0_3749| (|get.::.0_3752| x_3779)) … expansions
• unroll
 expr (|count_(ty_0 option list * ty_0 option list) list_3788| x_3779) expansions
• unroll
 expr (|count_(ty_0 option list * ty_0 option list) list_3788| (|get.::.1_3753| x_3779)) expansions
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_(ty_0 option list * ty_0 option list) list_3788| … expansions
• Unsat

## The Satisfaction of Subrepticiously Solving Sudokus using Satisfiability¶

We can now, finally, ask Imandra to find a sudoku that satisfies all the constraints defined before!

NOTE: we have to use [@@blast] because this problem is prone to combinatorial explosion and is too hard for Imandra's default unrolling algorithm.

In :
instance (fun (s:sudoku) -> is_valid_sudoku s && is_solution_of s the_problem) [@@blast] ;;

Out:
- : sudoku -> bool = <fun>
module CX : sig val s : sudoku end

Instance (after 273 steps, 3.103s):
let s =
let (_x_0 : cell option) = Some C8 in
let (_x_1 : cell option) = Some C1 in
let (_x_2 : cell option) = Some C2 in
let (_x_3 : cell option) = Some C7 in
let (_x_4 : cell option) = Some C5 in
let (_x_5 : cell option) = Some C3 in
let (_x_6 : cell option) = Some C6 in
let (_x_7 : cell option) = Some C4 in
let (_x_8 : cell option) = Some C9 in
{rows =
[[_x_0; _x_1; _x_2; _x_3; _x_4; _x_5; _x_6; _x_7; _x_8];
[_x_8; _x_7; _x_5; _x_6; _x_0; _x_2; _x_1; _x_3; _x_4];
[_x_6; _x_3; _x_4; _x_7; _x_8; _x_1; _x_2; _x_0; _x_5];
[_x_1; _x_4; _x_7; _x_2; _x_5; _x_3; _x_0; _x_8; _x_6];
[_x_5; _x_6; _x_8; _x_0; _x_7; _x_4; _x_3; _x_2; _x_1];
[_x_2; _x_0; _x_3; _x_1; _x_6; _x_8; _x_4; _x_5; _x_7];
[_x_4; _x_2; _x_1; _x_8; _x_3; _x_7; _x_5; _x_6; _x_0];
[_x_7; _x_5; _x_0; _x_4; _x_2; _x_6; _x_8; _x_1; _x_3];
[_x_3; _x_8; _x_6; _x_5; _x_1; _x_0; _x_7; _x_4; _x_2]]}

Instance

Let us look at the initial sudoku and its solution side to side:

In :
Imandra.display (Document.tbl [[doc_of_sudoku the_problem; Document.s "-->"; doc_of_sudoku CX.s]]) ;;

Out:
- : unit = ()

 8 · · · · · · · · · · 3 6 · · · · · · 7 · · 9 · 2 · · · 5 · · · 7 · · · · · · · 4 5 7 · · · · · 1 · · · 3 · · · 1 · · · · 6 8 · · 8 5 · · · 1 · · 9 · · · · 4 · ·
-->
 8 1 2 7 5 3 6 4 9 9 4 3 6 8 2 1 7 5 6 7 5 4 9 1 2 8 3 1 5 4 2 3 7 8 9 6 3 6 9 8 4 5 7 2 1 2 8 7 1 6 9 5 3 4 5 2 1 9 7 4 3 6 8 4 3 8 5 2 6 9 1 7 7 9 6 3 1 8 4 5 2

We can manipulate CX.s easily, directly in OCaml:

In :
let transpose_sudoku (s:sudoku) : sudoku = {rows = transpose s.rows};;

transpose_sudoku CX.s;;

Out:
val transpose_sudoku : sudoku -> sudoku = <fun>
- : sudoku = <document>

 8 9 6 1 3 2 5 4 7 1 4 7 5 6 8 2 3 9 2 3 5 4 9 7 1 8 6 7 6 4 2 8 1 9 5 3 5 8 9 3 4 6 7 2 1 3 2 1 7 5 9 4 6 8 6 1 2 8 7 5 3 9 4 4 7 8 9 2 3 6 1 5 9 5 3 6 1 4 8 7 2