# 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 -> Caml.Int.t = <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.023s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 3 rlimit count 1817 mk clause 3 datatype occurs check 21 mk bool var 50 arith assert upper 5 datatype splits 3 decisions 7 arith add rows 7 propagations 2 conflicts 7 arith fixed eqs 4 datatype accessor ax 5 arith conflicts 1 datatype constructor ax 8 num allocs 933548 final checks 6 added eqs 33 del clause 1 arith eq adapter 3 memory 5.9 max memory 5.9
Expand
• start[0.023s]
not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> List.tl _x = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || List.tl _x = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_1208| … expansions
• unroll
 expr (|count_ty_0 list_1208| (|get.::.1_1194| _x_1199)) expansions
• unroll
 expr (|count_ty_0 list_1208| _x_1199) expansions
• ##### unsat
(let ((a!1 (= (|count_ty_0 list_1208| _x_1199)
(+ 1 (|count_ty_0 list_1208| (|get.…

### 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 -> Z.t = <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.017s
details
Expand
smt_stats
 num checks 8 arith assert lower 13 arith pivots 8 rlimit count 6156 mk clause 41 datatype occurs check 36 mk bool var 128 arith assert upper 14 datatype splits 11 decisions 29 arith add rows 17 propagations 80 conflicts 13 arith fixed eqs 7 datatype accessor ax 14 arith conflicts 2 datatype constructor ax 23 num allocs 6.68098e+06 final checks 10 added eqs 104 del clause 8 arith eq adapter 10 memory 9.84 max memory 9.84
Expand
• start[0.017s]
(_x <> [] && List.hd _x = [])
&& not (_x = [])
&& Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> not
(((List.tl _x) <> [] && List.hd (List.tl _x) = [])
&& not (List.tl _x = []))
&& not
(not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
&& not (List.tl _x = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not ((((_x <> [] && List.hd _x = []) && not (_x = [])) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || not (((List.tl _x) <> [] && List.hd (List.tl _x) = []) && not (List.tl _x = [])) && not (not ((List.tl _x) <> [] && List.hd (List.tl _x) = []) && not (List.tl _x = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_1238| … expansions
• unroll
 expr (|count_ty_0 list list_1238| (|get.::.1_1221| _x_1227)) expansions
• unroll
 expr (|count_ty_0 list list_1238| _x_1227) expansions
• ##### unsat
(let ((a!1 (= (ite (>= (|count_ty_0 list_1240| |[]_2|) 0)
(|count_ty_0 list_1…

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.021s
details
Expand
smt_stats
 num checks 8 arith assert lower 11 arith pivots 9 rlimit count 3037 mk clause 33 datatype occurs check 31 mk bool var 94 arith assert upper 12 datatype splits 10 decisions 32 arith add rows 16 propagations 55 conflicts 12 arith fixed eqs 5 datatype accessor ax 7 arith conflicts 2 datatype constructor ax 14 num allocs 4.15166e+06 final checks 8 added eqs 62 del clause 8 arith eq adapter 7 memory 6.91 max memory 6.91
Expand
• start[0.021s]
not (_x <> [] && List.hd _x = [])
&& not (_x = [])
&& Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> not
(((List.tl _x) <> [] && List.hd (List.tl _x) = [])
&& not (List.tl _x = []))
&& not
(not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
&& not (List.tl _x = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not (((not (_x <> [] && List.hd _x = []) && not (_x = [])) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || not (((List.tl _x) <> [] && List.hd (List.tl _x) = []) && not (List.tl _x = [])) && not (not ((List.tl _x) <> [] && List.hd (List.tl _x) = []) && not (List.tl _x = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_1238| … expansions
• unroll
 expr (|count_ty_0 list list_1238| (|get.::.1_1221| _x_1227)) expansions
• unroll
 expr (|count_ty_0 list list_1238| _x_1227) expansions
• ##### unsat
(let ((a!1 (ite (>= (|count_ty_0 list_1240| (|get.::.0_1220| _x_1227)) 0)
(|count_…

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.032s
details
Expand
smt_stats
 num checks 8 arith assert lower 13 arith pivots 8 rlimit count 6156 mk clause 41 datatype occurs check 36 mk bool var 128 arith assert upper 14 datatype splits 11 decisions 29 arith add rows 17 propagations 80 conflicts 13 arith fixed eqs 7 datatype accessor ax 14 arith conflicts 2 datatype constructor ax 23 num allocs 2.11155e+07 final checks 10 added eqs 104 del clause 8 arith eq adapter 10 memory 10.41 max memory 10.41
Expand
• start[0.032s]
(_x <> [] && List.hd _x = [])
&& not (_x = [])
&& Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> not
(((List.tl _x) <> [] && List.hd (List.tl _x) = [])
&& not (List.tl _x = []))
&& not
(not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
&& not (List.tl _x = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not ((((_x <> [] && List.hd _x = []) && not (_x = [])) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || not (((List.tl _x) <> [] && List.hd (List.tl _x) = []) && not (List.tl _x = [])) && not (not ((List.tl _x) <> [] && List.hd (List.tl _x) = []) && not (List.tl _x = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_1269| … expansions
• unroll
 expr (|count_ty_0 list list_1269| (|get.::.1_1252| _x_1258)) expansions
• unroll
 expr (|count_ty_0 list list_1269| _x_1258) expansions
• ##### unsat
(let ((a!1 (= (ite (>= (|count_ty_0 list_1271| |[]_2|) 0)
(|count_ty_0 list_1…

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.029s
details
Expand
smt_stats
 num checks 8 arith assert lower 11 arith pivots 9 rlimit count 3037 mk clause 33 datatype occurs check 31 mk bool var 94 arith assert upper 12 datatype splits 10 decisions 32 arith add rows 16 propagations 55 conflicts 12 arith fixed eqs 5 datatype accessor ax 7 arith conflicts 2 datatype constructor ax 14 num allocs 1.63241e+07 final checks 8 added eqs 62 del clause 8 arith eq adapter 7 memory 7.47 max memory 10.14
Expand
• start[0.029s]
not (_x <> [] && List.hd _x = [])
&& not (_x = [])
&& Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> not
(((List.tl _x) <> [] && List.hd (List.tl _x) = [])
&& not (List.tl _x = []))
&& not
(not ((List.tl _x) <> [] && List.hd (List.tl _x) = [])
&& not (List.tl _x = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not (((not (_x <> [] && List.hd _x = []) && not (_x = [])) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || not (((List.tl _x) <> [] && List.hd (List.tl _x) = []) && not (List.tl _x = [])) && not (not ((List.tl _x) <> [] && List.hd (List.tl _x) = []) && not (List.tl _x = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_1269| … expansions
• unroll
 expr (|count_ty_0 list list_1269| (|get.::.1_1252| _x_1258)) expansions
• unroll
 expr (|count_ty_0 list list_1269| _x_1258) expansions
• ##### unsat
(let ((a!1 (ite (>= (|count_ty_0 list_1271| (|get.::.0_1251| _x_1258)) 0)
(|count_…

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 ordinalOrdinal.Int (if measure_transpose l >= 0 then measure_transpose l else 0)
sub ordinalOrdinal.Int (if measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) >= 0 then measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) 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 assert lower 5 arith pivots 2 rlimit count 2106 mk clause 5 datatype occurs check 46 mk bool var 68 arith assert upper 3 datatype splits 11 decisions 15 arith add rows 2 propagations 4 conflicts 8 arith fixed eqs 1 datatype accessor ax 8 arith conflicts 1 datatype constructor ax 16 num allocs 3.65133e+07 final checks 11 added eqs 48 del clause 5 arith eq adapter 2 memory 8.2 max memory 10.41
Expand
• start[0.015s]
not (l <> [] && List.hd l = [])
&& not (l = [])
&& (if (if l = [] then 0 else List.length (List.hd l)) >= 0
then if l = [] then 0 else List.length (List.hd l) else 0)
>= 0
&& (if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
else List.length …)
>= 0
then
if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
else List.length …
else 0)
>= 0
==> not
(not (true && List.tl (List.hd l) = [])
&& not ((List.tl (List.hd l)) :: (transpose3 …) = []))
|| Ordinal.( << )
(Ordinal.Int
(if (if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
else List.length …)
>= 0
then
if (List.tl (List.hd l)) :: (transpose3 …) = [] then 0
else List.length …
else 0))
(Ordinal.Int
(if (if l = [] then 0 else List.length (List.hd l)) >= 0
then if l = [] then 0 else List.length (List.hd l) else 0))
• ##### simplify
 into (not (((not (l <> [] && List.hd l = []) && not (l = [])) && (if (if l = [] then 0 else List.length (List.hd l)) >= 0 then if l = [] then 0 else List.length (List.hd l) else 0) >= 0) && (if List.length (List.tl (List.hd l)) >= 0 then List.length (List.tl (List.hd l)) else 0) >= 0) || List.tl (List.hd l) = []) || Ordinal.( << ) (Ordinal.Int (if List.length (List.tl (List.hd l)) >= 0 then List.length (List.tl (List.hd l)) else 0)) (Ordinal.Int (if (if l = [] then 0 else List.length (List.hd l)) >= 0 then if l = [] then 0 else List.length (List.hd l) else 0)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (let ((a!1 (>= (|List.length_1338| (|get.::.1_1312| (|get.::.0_1314| l_1331))) 0)) … expansions
• unroll
 expr (|List.length_1338| (|get.::.1_1312| (|get.::.0_1314| l_1331))) expansions
• unroll
 expr (|List.length_1338| (|get.::.0_1314| l_1331)) expansions
• ##### unsat
(let ((a!1 (+ 1 (|List.length_1338| (|get.::.1_1312| (|get.::.0_1314| l_1331)))))
(a!7 (not (a…

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.013s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 3 rlimit count 2043 mk clause 3 datatype occurs check 30 mk bool var 66 arith assert upper 5 datatype splits 6 decisions 14 arith add rows 7 propagations 1 conflicts 10 arith fixed eqs 4 datatype accessor ax 8 arith conflicts 1 datatype constructor ax 16 num allocs 4.97808e+07 final checks 6 added eqs 52 del clause 1 arith eq adapter 3 memory 8.7 max memory 10.41
Expand
• start[0.013s]
not (l = [])
&& not (x = Z)
&& Ordinal.count x >= 0 && Ordinal.count (Destruct(S, 0, x)) >= 0
==> not (not (List.tl l = []) && not (Destruct(S, 0, x) = Z))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
(Ordinal.Int (Ordinal.count x))
• ##### simplify
 into (not (((not (l = []) && not (x = Z)) && Ordinal.count x >= 0) && Ordinal.count (Destruct(S, 0, x)) >= 0) || not (not (List.tl l = []) && not (Destruct(S, 0, x) = Z))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(S, 0, x)))) (Ordinal.Int (Ordinal.count x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (count_nat_1370 (|get.S.0_1349| x_1359))) (|Or… expansions
• unroll
 expr (count_nat_1370 (|get.S.0_1349| x_1359)) expansions
• unroll
 expr (count_nat_1370 x_1359) expansions
• ##### unsat
(let ((a!1 (= (count_nat_1370 x_1359)
(+ 1 (count_nat_1370 (|get.S.0_1349| x_1359)))))…

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.016s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 3 rlimit count 2043 mk clause 3 datatype occurs check 30 mk bool var 66 arith assert upper 5 datatype splits 6 decisions 14 arith add rows 7 propagations 1 conflicts 10 arith fixed eqs 4 datatype accessor ax 8 arith conflicts 1 datatype constructor ax 16 num allocs 6.46183e+07 final checks 6 added eqs 52 del clause 1 arith eq adapter 3 memory 9.12 max memory 10.41
Expand
• start[0.016s]
not (y = [])
&& not (x = Z)
&& Ordinal.count x >= 0 && Ordinal.count (Destruct(S, 0, x)) >= 0
==> not (not (List.tl y = []) && not (Destruct(S, 0, x) = Z))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(S, 0, x))))
(Ordinal.Int (Ordinal.count x))
• ##### simplify
 into (not (((not (y = []) && not (x = Z)) && Ordinal.count x >= 0) && Ordinal.count (Destruct(S, 0, x)) >= 0) || not (not (List.tl y = []) && not (Destruct(S, 0, x) = Z))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (Destruct(S, 0, x)))) (Ordinal.Int (Ordinal.count x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (count_nat_1396 (|get.S.0_1376| x_1385))) (|Or… expansions
• unroll
 expr (count_nat_1396 (|get.S.0_1376| x_1385)) expansions
• unroll
 expr (count_nat_1396 x_1385) expansions
• ##### unsat
(let ((a!1 (= (count_nat_1396 x_1385)
(+ 1 (count_nat_1396 (|get.S.0_1376| x_1385)))))…

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.013s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 3 rlimit count 1936 mk clause 3 datatype occurs check 18 mk bool var 52 arith assert upper 5 datatype splits 3 decisions 7 arith add rows 7 propagations 2 conflicts 7 arith fixed eqs 4 datatype accessor ax 5 arith conflicts 1 datatype constructor ax 8 num allocs 8.15919e+07 final checks 5 added eqs 33 del clause 1 arith eq adapter 3 memory 9.52 max memory 10.41
Expand
• start[0.013s]
not (x = List.hd y)
&& not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
==> not (not (x = List.hd (List.tl y)) && not (List.tl y = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
(Ordinal.Int (Ordinal.count y))
• ##### simplify
 into (not (((not (x = List.hd y) && not (y = [])) && Ordinal.count y >= 0) && Ordinal.count (List.tl y) >= 0) || not (not (x = List.hd (List.tl y)) && not (List.tl y = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y))) (Ordinal.Int (Ordinal.count y)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_1421| … expansions
• unroll
 expr (|count_ty_0 list_1421| (|get.::.1_1404| y_1411)) expansions
• unroll
 expr (|count_ty_0 list_1421| y_1411) expansions
• ##### unsat
(let ((a!1 (= (|count_ty_0 list_1421| y_1411)
(+ 1 (|count_ty_0 list_1421| (|get.:…

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.016s
details
Expand
smt_stats
 num checks 9 arith assert lower 6 arith pivots 4 rlimit count 2357 mk clause 8 datatype occurs check 21 mk bool var 58 arith assert upper 4 datatype splits 3 decisions 15 arith add rows 5 propagations 5 conflicts 7 arith fixed eqs 3 datatype accessor ax 5 arith conflicts 1 datatype constructor ax 6 num allocs 9.31752e+07 final checks 6 added eqs 31 del clause 1 arith eq adapter 3 memory 12.9 max memory 12.9
Expand
• start[0.016s]
not (elem (List.hd x) (List.tl x))
&& not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
==> not
(not (elem (List.hd (List.tl x)) (List.tl (List.tl x)))
&& not (List.tl x = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
(Ordinal.Int (Ordinal.count x))
• ##### simplify
 into (not (((not (elem (List.hd x) (List.tl x)) && not (x = [])) && Ordinal.count x >= 0) && Ordinal.count (List.tl x) >= 0) || not (not (elem (List.hd (List.tl x)) (List.tl (List.tl x))) && not (List.tl x = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x))) (Ordinal.Int (Ordinal.count x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_1447| … expansions
• unroll
 expr (elem_1433 (|get.::.0_1427| (|get.::.1_1428| x_1438)) (|get.::.1_1428| (|get.::.1_1428| x… expansions
• unroll
 expr (|count_ty_0 list_1447| (|get.::.1_1428| x_1438)) expansions
• unroll
 expr (|count_ty_0 list_1447| x_1438) expansions
• ##### unsat
(let ((a!1 (= (|count_ty_0 list_1447| x_1438)
(+ 1 (|count_ty_0 list_1447| (|get.:…

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.013s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 3 rlimit count 1978 mk clause 3 datatype occurs check 29 mk bool var 64 arith assert upper 5 datatype splits 9 decisions 16 arith add rows 7 propagations 2 conflicts 7 arith fixed eqs 4 datatype accessor ax 10 arith conflicts 1 datatype constructor ax 16 num allocs 1.22117e+08 final checks 8 added eqs 49 del clause 1 arith eq adapter 3 memory 10.35 max memory 12.9
Expand
• start[0.013s]
not (l = []) && Ordinal.count l >= 0 && Ordinal.count (List.tl l) >= 0
==> List.tl l = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl l)))
(Ordinal.Int (Ordinal.count l))
• ##### simplify
 into (not ((not (l = []) && Ordinal.count l >= 0) && Ordinal.count (List.tl l) >= 0) || List.tl l = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl l))) (Ordinal.Int (Ordinal.count l)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 option list_1476| … expansions
• unroll
 expr (|count_ty_0 option list_1476| (|get.::.1_1457| l_1467)) expansions
• unroll
 expr (|count_ty_0 option list_1476| l_1467) expansions
• ##### unsat
(let ((a!1 (= (|count_ty_0 option list_1476| l_1467)
(+ 2 (|count_ty_0 option list…

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.014s
details
Expand
smt_stats
 num checks 8 arith assert lower 15 arith pivots 8 rlimit count 2597 mk clause 12 datatype occurs check 29 mk bool var 87 arith assert upper 12 datatype splits 9 decisions 24 arith add rows 12 propagations 10 conflicts 10 arith fixed eqs 7 datatype accessor ax 10 arith conflicts 2 arith assert diseq 1 datatype constructor ax 16 num allocs 1.45429e+08 final checks 8 added eqs 58 del clause 5 arith eq adapter 10 memory 11.02 max memory 12.9
Expand
• start[0.014s]
not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> List.tl _x = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || List.tl _x = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_1535| … expansions
• unroll
 expr (|count_ty_0 list list_1535| (|get.::.1_1515| _x_1526)) expansions
• unroll
 expr (|count_ty_0 list list_1535| _x_1526) expansions
• ##### unsat
(let ((a!1 (ite (>= (|count_ty_0 list_1537| (|get.::.0_1514| _x_1526)) 0)
(|count_…

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.037s
details
Expand
smt_stats
 num checks 8 arith assert lower 15 arith pivots 8 rlimit count 2597 mk clause 12 datatype occurs check 29 mk bool var 87 arith assert upper 12 datatype splits 9 decisions 24 arith add rows 12 propagations 10 conflicts 10 arith fixed eqs 7 datatype accessor ax 10 arith conflicts 2 arith assert diseq 1 datatype constructor ax 16 num allocs 1.70573e+08 final checks 8 added eqs 58 del clause 5 arith eq adapter 10 memory 11.57 max memory 14.35
Expand
• start[0.037s]
not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> List.tl _x = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || List.tl _x = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_1573| … expansions
• unroll
 expr (|count_ty_0 list list_1573| (|get.::.1_1547| _x_1564)) expansions
• unroll
 expr (|count_ty_0 list list_1573| _x_1564) expansions
• ##### unsat
(let ((a!1 (ite (>= (|count_ty_0 list_1575| (|get.::.0_1546| _x_1564)) 0)
(|count_…

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 assert lower 15 arith pivots 8 rlimit count 2597 mk clause 12 datatype occurs check 29 mk bool var 87 arith assert upper 12 datatype splits 9 decisions 24 arith add rows 12 propagations 10 conflicts 10 arith fixed eqs 7 datatype accessor ax 10 arith conflicts 2 arith assert diseq 1 datatype constructor ax 16 num allocs 1.86788e+08 final checks 8 added eqs 58 del clause 5 arith eq adapter 10 memory 15.01 max memory 15.01
Expand
• start[0.021s]
not (_x = []) && Ordinal.count _x >= 0 && Ordinal.count (List.tl _x) >= 0
==> List.tl _x = []
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x)))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not ((not (_x = []) && Ordinal.count _x >= 0) && Ordinal.count (List.tl _x) >= 0) || List.tl _x = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl _x))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list list_1606| … expansions
• unroll
 expr (|count_ty_0 list list_1606| (|get.::.1_1585| _x_1597)) expansions
• unroll
 expr (|count_ty_0 list list_1606| _x_1597) expansions
• ##### unsat
(let ((a!1 (ite (>= (|count_ty_0 list_1608| (|get.::.0_1584| _x_1597)) 0)
(|count_…

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_instances12
definitions0
inductions0
search_time
0.054s
details
Expand
smt_stats
 arith offset eqs 98 num checks 26 arith assert lower 487 arith pivots 125 rlimit count 45098 mk clause 546 datatype occurs check 210 mk bool var 1201 arith assert upper 467 datatype splits 109 decisions 1043 arith add rows 600 arith bound prop 67 propagations 1328 interface eqs 19 conflicts 101 arith fixed eqs 207 datatype accessor ax 121 minimized lits 26 arith conflicts 32 arith assert diseq 164 datatype constructor ax 312 num allocs 2.18246e+08 final checks 56 added eqs 1663 del clause 277 arith eq adapter 317 memory 16.23 max memory 16.23
Expand
• start[0.054s]
not (List.tl (List.tl _x) = [])
&& not (List.tl _x = [])
&& not (_x = [])
&& Ordinal.count _x >= 0
&& Ordinal.count (List.tl (List.tl (List.tl _x))) >= 0
==> not
(not (List.tl (List.tl (List.tl (List.tl (List.tl _x)))) = [])
&& not (List.tl (List.tl (List.tl (List.tl _x))) = [])
&& not (List.tl (List.tl (List.tl _x)) = []))
|| Ordinal.( << )
(Ordinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x)))))
(Ordinal.Int (Ordinal.count _x))
• ##### simplify
 into (not ((((not (List.tl (List.tl _x) = []) && not (List.tl _x = [])) && not (_x = [])) && Ordinal.count _x >= 0) && Ordinal.count (List.tl (List.tl (List.tl _x))) >= 0) || not ((not (List.tl (List.tl (List.tl (List.tl (List.tl _x)))) = []) && not (List.tl (List.tl (List.tl (List.tl _x))) = [])) && not (List.tl (List.tl (List.tl _x)) = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl (List.tl (List.tl _x))))) (Ordinal.Int (Ordinal.count _x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (let ((a!1 (|count_ty_0 list list_1641| (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_… expansions
• unroll
 expr (|count_ty_0 list list_1641| (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_1618| _x_1632)))) expansions
• unroll
 expr (|count_ty_0 list list_1641| _x_1632) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_1618| _x_1632)))))) (|cou… expansions
• unroll
 expr (let ((a!1 (|count_ty_0 list list_1641| (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_… expansions
• unroll
 expr (let ((a!1 (|get.::.0_1617| (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_1618| _x_1632)))))) (|cou… expansions
• unroll
 expr (|count_ty_0 list list_1641| (|get.::.1_1618| _x_1632)) expansions
• unroll
 expr (|count_ty_0 list_1643| (|get.::.0_1617| _x_1632)) expansions
• unroll
 expr (let ((a!1 (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_1618| _x_1632)))))) (|cou… expansions
• unroll
 expr (let ((a!1 (|count_ty_0 list list_1641| (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_… expansions
• unroll
 expr (let ((a!1 (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_1618| (|get.::.1_1618| _x_1632)))))) (|cou… expansions
• unroll
 expr (|count_ty_0 list list_1641| (|get.::.1_1618| (|get.::.1_1618| _x_1632))) expansions
• ##### unsat
(let ((a!1 (>= (|count_ty_0 list_1643|
(|get.::.0_1617| (|get.::.1_1618| _x_1632)…

## 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 -> Imandra_surface.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 -> Imandra_surface.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.015s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 3 rlimit count 2037 mk clause 3 datatype occurs check 30 mk bool var 68 arith assert upper 5 datatype splits 6 decisions 14 arith add rows 7 propagations 1 conflicts 10 arith fixed eqs 4 datatype accessor ax 8 arith conflicts 1 datatype constructor ax 16 num allocs 2.6089e+08 final checks 6 added eqs 54 del clause 1 arith eq adapter 3 memory 17.94 max memory 17.94
Expand
• start[0.015s]
not (l1 = [] || l2 = [])
&& Ordinal.count l1 >= 0 && Ordinal.count (List.tl l1) >= 0
==> (List.tl l1 = [] || List.tl l2 = [])
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl l1)))
(Ordinal.Int (Ordinal.count l1))
• ##### simplify
 into ((not ((not (l1 = [] || l2 = []) && Ordinal.count l1 >= 0) && Ordinal.count (List.tl l1) >= 0) || List.tl l1 = []) || List.tl l2 = []) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl l1))) (Ordinal.Int (Ordinal.count l1)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_ty_0 list_1954| … expansions
• unroll
 expr (|count_ty_0 list_1954| (|get.::.1_1925| l1_1943)) expansions
• unroll
 expr (|count_ty_0 list_1954| l1_1943) expansions
• ##### unsat
(let ((a!1 (= (|count_ty_0 list_1954| l1_1943)
(+ 1 (|count_ty_0 list_1954| (|get.…

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[(List.hd y).0 = None || (List.hd y).1 = None && not (y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 7 arith assert lower 6 arith pivots 5 rlimit count 5693 mk clause 28 datatype occurs check 66 mk bool var 164 arith assert upper 4 datatype splits 42 decisions 34 arith add rows 6 propagations 51 conflicts 12 arith fixed eqs 3 datatype accessor ax 27 arith conflicts 1 datatype constructor ax 35 num allocs 3.17444e+08 final checks 14 added eqs 150 del clause 2 arith eq adapter 3 memory 21.36 max memory 21.38
Expand
• start[0.014s]
((List.hd y).0 = None || (List.hd y).1 = None)
&& not (y = []) && Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
==> not
(((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
&& not (List.tl y = []))
&& not
(Option.get (List.hd (List.tl y)).0 =
Option.get (List.hd (List.tl y)).1
&& not
((List.hd (List.tl y)).0 = None
|| (List.hd (List.tl y)).1 = None)
&& not (List.tl y = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
(Ordinal.Int (Ordinal.count y))
• ##### simplify
 into (not (((((List.hd y).0 = None || (List.hd y).1 = None) && not (y = [])) && Ordinal.count y >= 0) && Ordinal.count (List.tl y) >= 0) || not (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None) && not (List.tl y = [])) && not ((Option.get (List.hd (List.tl y)).0 = Option.get (List.hd (List.tl y)).1 && not ((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)) && not (List.tl y = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y))) (Ordinal.Int (Ordinal.count y)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_(ty_0 option * ty_0 option) list_1985| … expansions
• unroll
 expr (|count_(ty_0 option * ty_0 option) list_1985| (|get.::.1_1967| y_1974)) expansions
• unroll
 expr (|count_(ty_0 option * ty_0 option) list_1985| y_1974) expansions
• ##### unsat
(let ((a!1 (= (|count_(ty_0 option * ty_0 option) list_1985| y_1974)
(+ 4
…

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[Option.get (List.hd y).0 = Option.get (List.hd y).1 && not ((List.hd y).0 = None || (List.hd y).1 = None) && not (y = [])]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.019s
details
Expand
smt_stats
 num checks 7 arith assert lower 5 arith pivots 4 rlimit count 2887 mk clause 26 datatype occurs check 59 mk bool var 147 arith assert upper 5 datatype splits 26 decisions 31 arith add rows 7 propagations 57 conflicts 13 arith fixed eqs 4 datatype accessor ax 26 arith conflicts 1 datatype constructor ax 34 num allocs 2.98033e+08 final checks 11 added eqs 148 del clause 2 arith eq adapter 3 memory 18.55 max memory 21.38
Expand
• start[0.019s]
Option.get (List.hd y).0 = Option.get (List.hd y).1
&& not ((List.hd y).0 = None || (List.hd y).1 = None)
&& not (y = [])
&& Ordinal.count y >= 0 && Ordinal.count (List.tl y) >= 0
==> not
(((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)
&& not (List.tl y = []))
&& not
(Option.get (List.hd (List.tl y)).0 =
Option.get (List.hd (List.tl y)).1
&& not
((List.hd (List.tl y)).0 = None
|| (List.hd (List.tl y)).1 = None)
&& not (List.tl y = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y)))
(Ordinal.Int (Ordinal.count y))
• ##### simplify
 into (not ((((Option.get (List.hd y).0 = Option.get (List.hd y).1 && not ((List.hd y).0 = None || (List.hd y).1 = None)) && not (y = [])) && Ordinal.count y >= 0) && Ordinal.count (List.tl y) >= 0) || not (((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None) && not (List.tl y = [])) && not ((Option.get (List.hd (List.tl y)).0 = Option.get (List.hd (List.tl y)).1 && not ((List.hd (List.tl y)).0 = None || (List.hd (List.tl y)).1 = None)) && not (List.tl y = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl y))) (Ordinal.Int (Ordinal.count y)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_(ty_0 option * ty_0 option) list_1985| … expansions
• unroll
 expr (|count_(ty_0 option * ty_0 option) list_1985| (|get.::.1_1967| y_1974)) expansions
• unroll
 expr (|count_(ty_0 option * ty_0 option) list_1985| y_1974) expansions
• ##### unsat
(let ((a!1 (= (|count_(ty_0 option * ty_0 option) list_1985| y_1974)
(+ 4
…

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[match_cols (zip (List.hd x).0 (List.hd x).1) && not (x = [])]
proof
detailed proof
ground_instances5
definitions0
inductions0
search_time
0.019s
details
Expand
smt_stats
 arith offset eqs 5 num checks 12 arith assert lower 30 arith pivots 20 rlimit count 6702 mk clause 54 datatype occurs check 72 mk bool var 239 arith assert upper 28 datatype splits 27 decisions 92 arith add rows 31 propagations 49 conflicts 17 arith fixed eqs 11 datatype accessor ax 32 minimized lits 2 arith conflicts 6 arith assert diseq 1 datatype constructor ax 55 num allocs 3.57636e+08 final checks 11 added eqs 212 del clause 21 arith eq adapter 20 memory 22.07 max memory 22.07
Expand
• start[0.019s]
match_cols (zip (List.hd x).0 (List.hd x).1)
&& not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
==> not
(match_cols (zip (List.hd (List.tl x)).0 (List.hd (List.tl x)).1)
&& not (List.tl x = []))
|| Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x)))
(Ordinal.Int (Ordinal.count x))
• ##### simplify
 into (not (((match_cols (zip (List.hd x).0 (List.hd x).1) && not (x = [])) && Ordinal.count x >= 0) && Ordinal.count (List.tl x) >= 0) || not (match_cols (zip (List.hd (List.tl x)).0 (List.hd (List.tl x)).1) && not (List.tl x = []))) || Ordinal.( << ) (Ordinal.Int (Ordinal.count (List.tl x))) (Ordinal.Int (Ordinal.count x)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (|count_(ty_0 option list * ty_0 option list) list_2042| … expansions
• unroll
 expr (zip_2020 (|tuple_get.0_2003| (|get.::.0_2006| (|get.::.1_2007| x_2033))) (|tuple_get.1_20… expansions
• unroll
 expr (let ((a!1 (zip_2020 (|tuple_get.0_2003| (|get.::.0_2006| (|get.::.1_2007| x_… expansions
• unroll
 expr (|count_(ty_0 option list * ty_0 option list) list_2042| (|get.::.1_2007| x_2033)) expansions
• unroll
 expr (|count_(ty_0 option list * ty_0 option list) list_2042| x_2033) expansions
• ##### unsat
(let ((a!1 (>= (|count_ty_0 option list_2046|
(|tuple_get.0_2003| (|get.::.0_2006…

## 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, 2.200s):
let s =
{rows =
[[Some C8; Some C1; Some C2; Some C7; Some C5; Some C3; Some C6;
Some C4; Some C9];
[Some C9; Some C4; Some C3; Some C6; Some C8; Some C2; Some C1;
Some C7; Some C5];
[Some C6; Some C7; Some C5; Some C4; Some C9; Some C1; Some C2;
Some C8; Some C3];
[Some C1; Some C5; Some C4; Some C2; Some C3; Some C7; Some C8;
Some C9; Some C6];
[Some C3; Some C6; Some C9; Some C8; Some C4; Some C5; Some C7;
Some C2; Some C1];
[Some C2; Some C8; Some C7; Some C1; Some C6; Some C9; Some C5;
Some C3; Some C4];
[Some C5; Some C2; Some C1; Some C9; Some C7; Some C4; Some C3;
Some C6; Some C8];
[Some C4; Some C3; Some C8; Some C5; Some C2; Some C6; Some C9;
Some C1; Some C7];
[Some C7; Some C9; Some C6; Some C3; Some C1; Some C8; Some C4;
Some C5; Some C2]]}

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