# 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 = <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
original:length _x
sub:length (List.tl _x)
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[_x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 5 arith tableau max rows: 4 arith tableau max columns: 11 arith pivots: 4 rlimit count: 1806 mk clause: 12 datatype occurs check: 12 mk bool var: 52 arith assert upper: 5 datatype splits: 1 decisions: 10 arith row summations: 7 propagations: 12 conflicts: 7 arith fixed eqs: 4 datatype accessor ax: 10 arith conflicts: 1 arith num rows: 4 datatype constructor ax: 8 num allocs: 5.51568e+06 final checks: 4 added eqs: 37 del clause: 4 arith eq adapter: 5 memory: 15.36 max memory: 15.36
Expand
• start[0.009s]
let (_x_0 : ty_0 list) = List.tl … in
let (_x_1 : int) = count.list (const 0) _x_0 in
_x <> [] && ((count.list (const 0) _x >= 0) && (_x_1 >= 0))
==> not (_x_0 <> [])
|| Ordinal.( << ) (Ordinal.Int _x_1)
(Ordinal.Int (count.list (const 0) …))
• ###### simplify
 into: let (_x_0 : ty_0 list) = List.tl … in let (_x_1 : int) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) … in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (… <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_388/server| (|get.::.1_371/server|… expansions:
• unroll
 expr: (|count.list_388/server| (|get.::.1_371/server| _x_377/server)) expansions:
• unroll
 expr: (|count.list_388/server| _x_377/server) 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 -> Z.t = <fun>
val transpose : 'a list list -> 'a list list = <fun>

termination proof

### Termination proof

call transpose3 (List.tl _x) from transpose3 _x
original:transpose3 _x
sub:transpose3 (List.tl _x)
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[(List.hd _x) <> [] && _x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.008s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 15 arith tableau max rows: 6 arith tableau max columns: 17 arith pivots: 11 rlimit count: 5987 mk clause: 34 datatype occurs check: 25 mk bool var: 119 arith assert upper: 12 datatype splits: 6 decisions: 33 arith row summations: 17 propagations: 62 conflicts: 11 arith fixed eqs: 8 datatype accessor ax: 21 arith conflicts: 2 arith num rows: 6 datatype constructor ax: 26 num allocs: 1.59216e+07 final checks: 6 added eqs: 109 del clause: 9 arith eq adapter: 11 memory: 16.21 max memory: 16.24
Expand
• start[0.008s]
let (_x_0 : int) = count.list (count.list (const 0)) _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
let (_x_3 : bool) = (List.hd _x_1) <> [] in
let (_x_4 : bool) = _x_1 <> [] in
(List.hd _x) <> [] && (_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 : bool) = (List.hd _x_0) <> [] in let (_x_2 : bool) = _x_0 <> [] in let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in let (_x_4 : int) = count.list (count.list (const 0)) _x in (not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4) || not ((List.hd _x) <> [] && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_444/server| (|get.::.1_424/server|… expansions:
• unroll
 expr: (|count.list_444/server| (|get.::.1_424/server| _x_431/server)) expansions:
• unroll
 expr: (|count.list_444/server| _x_431/server) expansions:
• Unsat
call transpose3 (List.tl _x) from transpose3 _x
original:transpose3 _x
sub:transpose3 (List.tl _x)
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[not ((List.hd _x) <> []) && _x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 15 arith tableau max rows: 6 arith tableau max columns: 17 arith pivots: 11 rlimit count: 2977 mk clause: 34 datatype occurs check: 22 mk bool var: 112 arith assert upper: 12 datatype splits: 3 decisions: 30 arith row summations: 17 propagations: 62 conflicts: 11 arith fixed eqs: 8 datatype accessor ax: 15 arith conflicts: 2 arith num rows: 6 datatype constructor ax: 23 num allocs: 1.05182e+07 final checks: 6 added eqs: 102 del clause: 9 arith eq adapter: 11 memory: 16.24 max memory: 16.24
Expand
• start[0.010s]
let (_x_0 : int) = count.list (count.list (const 0)) _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
let (_x_3 : bool) = (List.hd _x_1) <> [] in
let (_x_4 : bool) = _x_1 <> [] in
not ((List.hd _x) <> []) && (_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 : bool) = (List.hd _x_0) <> [] in let (_x_2 : bool) = _x_0 <> [] in let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in let (_x_4 : int) = count.list (count.list (const 0)) _x in (not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4) || not (not ((List.hd _x) <> []) && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_444/server| (|get.::.1_424/server|… expansions:
• unroll
 expr: (|count.list_444/server| (|get.::.1_424/server| _x_431/server)) expansions:
• unroll
 expr: (|count.list_444/server| _x_431/server) expansions:
• Unsat
termination proof

### Termination proof

call get_heads (List.tl _x) from get_heads _x
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[(List.hd _x) <> [] && _x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 15 arith tableau max rows: 6 arith tableau max columns: 17 arith pivots: 11 rlimit count: 5987 mk clause: 34 datatype occurs check: 25 mk bool var: 119 arith assert upper: 12 datatype splits: 6 decisions: 33 arith row summations: 17 propagations: 62 conflicts: 11 arith fixed eqs: 8 datatype accessor ax: 21 arith conflicts: 2 arith num rows: 6 datatype constructor ax: 26 num allocs: 3.04489e+07 final checks: 6 added eqs: 109 del clause: 9 arith eq adapter: 11 memory: 16.5 max memory: 16.51
Expand
• start[0.009s]
let (_x_0 : int) = count.list (count.list (const 0)) _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
let (_x_3 : bool) = (List.hd _x_1) <> [] in
let (_x_4 : bool) = _x_1 <> [] in
(List.hd _x) <> [] && (_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 : bool) = (List.hd _x_0) <> [] in let (_x_2 : bool) = _x_0 <> [] in let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in let (_x_4 : int) = count.list (count.list (const 0)) _x in (not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4) || not ((List.hd _x) <> [] && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_555/server| (|get.::.1_535/server|… expansions:
• unroll
 expr: (|count.list_555/server| (|get.::.1_535/server| _x_542/server)) expansions:
• unroll
 expr: (|count.list_555/server| _x_542/server) expansions:
• Unsat
call get_heads (List.tl _x) from get_heads _x
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[not ((List.hd _x) <> []) && _x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 15 arith tableau max rows: 6 arith tableau max columns: 17 arith pivots: 11 rlimit count: 2977 mk clause: 34 datatype occurs check: 22 mk bool var: 112 arith assert upper: 12 datatype splits: 3 decisions: 30 arith row summations: 17 propagations: 62 conflicts: 11 arith fixed eqs: 8 datatype accessor ax: 15 arith conflicts: 2 arith num rows: 6 datatype constructor ax: 23 num allocs: 2.28288e+07 final checks: 6 added eqs: 102 del clause: 9 arith eq adapter: 11 memory: 16.51 max memory: 16.51
Expand
• start[0.009s]
let (_x_0 : int) = count.list (count.list (const 0)) _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
let (_x_3 : bool) = (List.hd _x_1) <> [] in
let (_x_4 : bool) = _x_1 <> [] in
not ((List.hd _x) <> []) && (_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 : bool) = (List.hd _x_0) <> [] in let (_x_2 : bool) = _x_0 <> [] in let (_x_3 : int) = count.list (count.list (const 0)) _x_0 in let (_x_4 : int) = count.list (count.list (const 0)) _x in (not (_x_1 && _x_2) && not (not _x_1 && _x_2)) || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4) || not (not ((List.hd _x) <> []) && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_555/server| (|get.::.1_535/server|… expansions:
• unroll
 expr: (|count.list_555/server| (|get.::.1_535/server| _x_542/server)) expansions:
• unroll
 expr: (|count.list_555/server| _x_542/server) expansions:
• Unsat
termination proof

### Termination proof

call transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) from transpose l
original:transpose l
sub:transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))
original ordinal:let (_x_0 : int) = measure_transpose l in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
sub ordinal:let (_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:[(List.hd l) <> [] && l <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 7 arith assert lower: 5 arith tableau max rows: 2 arith tableau max columns: 6 arith pivots: 1 rlimit count: 2086 mk clause: 6 datatype occurs check: 13 mk bool var: 37 arith assert upper: 3 datatype splits: 2 decisions: 6 propagations: 4 conflicts: 4 datatype accessor ax: 11 arith conflicts: 1 arith num rows: 2 datatype constructor ax: 9 num allocs: 3.98768e+07 final checks: 4 added eqs: 28 del clause: 3 arith eq adapter: 2 memory: 16.89 max memory: 16.89
Expand
• start[0.009s]
let (_x_0 : ty_0 list) = List.hd l in
let (_x_1 : bool) = l <> [] in
let (_x_2 : int) = if _x_1 then List.length _x_0 else 0 in
let (_x_3 : int) = if _x_2 >= 0 then _x_2 else 0 in
let (_x_4 : int) = List.length … in
let (_x_5 : int) = if _x_4 >= 0 then _x_4 else 0 in
_x_0 <> [] && (_x_1 && ((_x_3 >= 0) && (_x_5 >= 0)))
==> not ((List.tl _x_0) <> [])
|| Ordinal.( << ) (Ordinal.Int _x_5) (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) = not _x_4 || (_x_3 >= 0) in not (_x_1 <> []) || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0)) (Ordinal.Int (if _x_5 then if _x_4 then _x_3 else 0 else 0)) || not (_x_0 <> [] && _x_4 && (_x_5 || not _x_5)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (>= (|List.length_711/server| (|get.::.1_681/server| (|get.::.0_683/serv… expansions:
• unroll
 expr: (|List.length_711/server| (|get.::.1_681/server| (|get.::.0_683/server| l_703/server))) expansions:
• unroll
 expr: (|List.length_711/server| (|get.::.0_683/server| l_703/server)) 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
original:take x l
sub:take (Destruct(S, 0, x)) (List.tl l)
original ordinal:Ordinal.Int (_cnt x)
sub ordinal:Ordinal.Int (_cnt (Destruct(S, 0, x)))
path:[l <> [] && Is_a(S, x)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.008s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 7 arith tableau max rows: 5 arith tableau max columns: 12 arith pivots: 6 rlimit count: 1982 mk clause: 13 datatype occurs check: 17 mk bool var: 69 arith assert upper: 7 datatype splits: 2 decisions: 13 arith row summations: 9 propagations: 14 conflicts: 7 arith fixed eqs: 4 datatype accessor ax: 14 arith conflicts: 1 arith num rows: 5 arith assert diseq: 1 datatype constructor ax: 12 num allocs: 5.01844e+07 final checks: 4 added eqs: 55 del clause: 5 arith eq adapter: 8 memory: 17.16 max memory: 17.16
Expand
• start[0.008s]
let (_x_0 : int) = count.nat x in
let (_x_1 : nat) = Destruct(S, 0, x) in
let (_x_2 : int) = count.nat _x_1 in
l <> [] && (Is_a(S, x) && ((_x_0 >= 0) && (_x_2 >= 0)))
==> not ((List.tl l) <> [] && Is_a(S, _x_1))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : nat) = Destruct(S, 0, x) in let (_x_1 : int) = count.nat _x_0 in let (_x_2 : int) = count.nat x in not ((List.tl l) <> [] && Is_a(S, _x_0)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (l <> [] && Is_a(S, x) && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.nat_1247/client| (|get.S.0_764/server| … expansions:
• unroll
 expr: (|count.nat_1247/client| (|get.S.0_764/server| x_774/server)) expansions:
• unroll
 expr: (|count.nat_1247/client| x_774/server) expansions:
• Unsat
termination proof

### Termination proof

call drop (Destruct(S, 0, x)) (List.tl y) from drop x y
original:drop x y
sub:drop (Destruct(S, 0, x)) (List.tl y)
original ordinal:Ordinal.Int (_cnt x)
sub ordinal:Ordinal.Int (_cnt (Destruct(S, 0, x)))
path:[y <> [] && Is_a(S, x)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 6 arith tableau max rows: 4 arith tableau max columns: 11 arith pivots: 6 rlimit count: 1989 mk clause: 12 datatype occurs check: 17 mk bool var: 67 arith assert upper: 6 datatype splits: 2 decisions: 15 arith row summations: 8 propagations: 14 conflicts: 8 arith fixed eqs: 3 datatype accessor ax: 13 arith conflicts: 1 arith num rows: 4 arith assert diseq: 1 datatype constructor ax: 13 num allocs: 6.16711e+07 final checks: 4 added eqs: 51 del clause: 4 arith eq adapter: 7 memory: 17.41 max memory: 17.41
Expand
• start[0.009s]
let (_x_0 : int) = count.nat x in
let (_x_1 : nat) = Destruct(S, 0, x) in
let (_x_2 : int) = count.nat _x_1 in
y <> [] && (Is_a(S, x) && ((_x_0 >= 0) && (_x_2 >= 0)))
==> not ((List.tl y) <> [] && Is_a(S, _x_1))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : nat) = Destruct(S, 0, x) in let (_x_1 : int) = count.nat _x_0 in let (_x_2 : int) = count.nat x in not ((List.tl y) <> [] && Is_a(S, _x_0)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (y <> [] && Is_a(S, x) && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.nat_1247/client| (|get.S.0_815/server| … expansions:
• unroll
 expr: (|count.nat_1247/client| (|get.S.0_815/server| x_825/server)) expansions:
• unroll
 expr: (|count.nat_1247/client| x_825/server) expansions:
• Unsat
termination proof

### Termination proof

call elem x (List.tl y) from elem x y
original:elem x y
sub:elem x (List.tl y)
original ordinal:Ordinal.Int (_cnt y)
sub ordinal:Ordinal.Int (_cnt (List.tl y))
path:[not (x = List.hd y) && y <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 8 arith tableau max rows: 4 arith tableau max columns: 11 arith pivots: 5 rlimit count: 1996 mk clause: 14 datatype occurs check: 12 mk bool var: 60 arith assert upper: 6 datatype splits: 1 decisions: 11 arith row summations: 8 propagations: 16 conflicts: 7 arith fixed eqs: 5 datatype accessor ax: 10 arith conflicts: 1 arith num rows: 4 datatype constructor ax: 8 num allocs: 7.45296e+07 final checks: 4 added eqs: 46 del clause: 6 arith eq adapter: 7 memory: 17.65 max memory: 17.65
Expand
• start[0.009s]
let (_x_0 : int) = count.list (const 0) y in
let (_x_1 : ty_0 list) = List.tl y in
let (_x_2 : int) = count.list (const 0) _x_1 in
not (x = List.hd y) && (y <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
==> not (not (x = List.hd _x_1) && _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) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) y in not (not (x = List.hd _x_0) && _x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (not (x = List.hd y) && y <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_887/server| (|get.::.1_868/server|… expansions:
• unroll
 expr: (|count.list_887/server| (|get.::.1_868/server| y_875/server)) expansions:
• unroll
 expr: (|count.list_887/server| y_875/server) expansions:
• Unsat
termination proof

### Termination proof

call unique (List.tl x) from unique x
original:unique x
sub:unique (List.tl x)
original ordinal:Ordinal.Int (_cnt x)
sub ordinal:Ordinal.Int (_cnt (List.tl x))
path:[not (elem (List.hd x) (List.tl x)) && x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 5 arith tableau max rows: 4 arith tableau max columns: 11 arith pivots: 4 rlimit count: 2046 mk clause: 11 datatype occurs check: 12 mk bool var: 50 arith assert upper: 5 datatype splits: 1 decisions: 10 arith row summations: 7 propagations: 10 conflicts: 7 arith fixed eqs: 4 datatype accessor ax: 9 arith conflicts: 1 arith num rows: 4 datatype constructor ax: 7 num allocs: 8.88158e+07 final checks: 4 added eqs: 34 del clause: 3 arith eq adapter: 4 memory: 17.99 max memory: 17.99
Expand
• start[0.009s]
let (_x_0 : ty_0 list) = List.tl x in
let (_x_1 : int) = count.list (const 0) x in
let (_x_2 : int) = count.list (const 0) _x_0 in
not (elem (List.hd x) _x_0) && (x <> [] && ((_x_1 >= 0) && (_x_2 >= 0)))
==> not (not (elem (List.hd _x_0) (List.tl _x_0)) && _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) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) x in not (not (elem (List.hd _x_0) (List.tl _x_0)) && _x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (not (elem (List.hd x) _x_0) && x <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_941/server| (|get.::.1_920/server|… expansions:
• unroll
 expr: (|count.list_941/server| (|get.::.1_920/server| x_930/server)) expansions:
• unroll
 expr: (|count.list_941/server| x_930/server) expansions:
• Unsat
termination proof

### Termination proof

call keep_some_list (List.tl l) from keep_some_list l
original:keep_some_list l
sub:keep_some_list (List.tl l)
original ordinal:Ordinal.Int (_cnt l)
sub ordinal:Ordinal.Int (_cnt (List.tl l))
path:[l <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.008s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 8 arith tableau max rows: 4 arith tableau max columns: 12 arith pivots: 5 rlimit count: 1955 mk clause: 14 datatype occurs check: 14 mk bool var: 66 arith assert upper: 6 datatype splits: 3 decisions: 18 arith row summations: 8 propagations: 15 conflicts: 7 arith fixed eqs: 5 datatype accessor ax: 13 arith conflicts: 1 arith num rows: 4 datatype constructor ax: 14 num allocs: 1.03977e+08 final checks: 4 added eqs: 58 del clause: 6 arith eq adapter: 7 memory: 18.16 max memory: 18.16
Expand
• start[0.008s]
let (_x_0 : int) = count.list (count.option (const 0)) … in
let (_x_1 : ty_0 option list) = List.tl … in
let (_x_2 : int) = count.list (count.option (const 0)) _x_1 in
l <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
==> not (_x_1 <> [])
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : ty_0 option list) = List.tl … in let (_x_1 : int) = count.list (count.option (const 0)) _x_0 in let (_x_2 : int) = count.list (count.option (const 0)) … in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (… <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_997/server| (|get.::.1_976/server|… expansions:
• unroll
 expr: (|count.list_997/server| (|get.::.1_976/server| l_986/server)) expansions:
• unroll
 expr: (|count.list_997/server| l_986/server) expansions:
• Unsat
termination proof

### Termination proof

call blocks_3_34 (List.tl _x) from blocks_3_34 _x
original:blocks_3_34 _x
sub:blocks_3_34 (List.tl _x)
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[_x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 18 arith tableau max rows: 7 arith tableau max columns: 18 arith pivots: 9 rlimit count: 2520 mk clause: 27 datatype occurs check: 14 mk bool var: 87 arith assert upper: 16 datatype splits: 3 decisions: 23 arith row summations: 19 propagations: 26 conflicts: 10 arith fixed eqs: 8 datatype accessor ax: 11 minimized lits: 1 arith conflicts: 2 arith num rows: 7 datatype constructor ax: 15 num allocs: 1.20923e+08 final checks: 4 added eqs: 64 del clause: 15 arith eq adapter: 13 memory: 18.7 max memory: 18.7
Expand
• start[0.009s]
let (_x_0 : int) = count.list (count.list (const 0)) _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
_x <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
==> not (_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) = count.list (count.list (const 0)) _x_0 in let (_x_2 : int) = count.list (count.list (const 0)) _x in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_1087/server| (|g… expansions:
• unroll
 expr: (|count.list_1087/server| (|get.::.1_1064/server| _x_1076/server)) expansions:
• unroll
 expr: (|count.list_1087/server| _x_1076/server) expansions:
• Unsat
termination proof

### Termination proof

call blocks_3_33 (List.tl _x) from blocks_3_33 _x
original:blocks_3_33 _x
sub:blocks_3_33 (List.tl _x)
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[_x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 22 arith tableau max rows: 7 arith tableau max columns: 18 arith pivots: 11 rlimit count: 2643 mk clause: 34 datatype occurs check: 14 mk bool var: 98 arith assert upper: 18 datatype splits: 3 decisions: 22 arith row summations: 20 arith bound prop: 1 propagations: 41 conflicts: 9 arith fixed eqs: 12 datatype accessor ax: 13 minimized lits: 1 arith conflicts: 2 arith num rows: 7 arith assert diseq: 1 datatype constructor ax: 15 num allocs: 1.38475e+08 final checks: 4 added eqs: 84 del clause: 14 arith eq adapter: 17 memory: 18.95 max memory: 18.95
Expand
• start[0.009s]
let (_x_0 : int) = count.list (count.list (const 0)) _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
_x <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
==> not (_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) = count.list (count.list (const 0)) _x_0 in let (_x_2 : int) = count.list (count.list (const 0)) _x in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_1156/server| (|g… expansions:
• unroll
 expr: (|count.list_1156/server| (|get.::.1_1127/server| _x_1145/server)) expansions:
• unroll
 expr: (|count.list_1156/server| _x_1145/server) expansions:
• Unsat
termination proof

### Termination proof

call blocks_3_32 (List.tl _x) from blocks_3_32 _x
original:blocks_3_32 _x
sub:blocks_3_32 (List.tl _x)
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl _x))
path:[_x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.008s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 18 arith tableau max rows: 7 arith tableau max columns: 18 arith pivots: 9 rlimit count: 2520 mk clause: 27 datatype occurs check: 14 mk bool var: 87 arith assert upper: 16 datatype splits: 3 decisions: 23 arith row summations: 19 propagations: 26 conflicts: 10 arith fixed eqs: 8 datatype accessor ax: 11 minimized lits: 1 arith conflicts: 2 arith num rows: 7 datatype constructor ax: 15 num allocs: 1.57227e+08 final checks: 4 added eqs: 64 del clause: 15 arith eq adapter: 13 memory: 19.28 max memory: 19.28
Expand
• start[0.008s]
let (_x_0 : int) = count.list (count.list (const 0)) _x in
let (_x_1 : ty_0 list list) = List.tl _x in
let (_x_2 : int) = count.list (count.list (const 0)) _x_1 in
_x <> [] && ((_x_0 >= 0) && (_x_2 >= 0))
==> not (_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) = count.list (count.list (const 0)) _x_0 in let (_x_2 : int) = count.list (count.list (const 0)) _x in not (_x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (_x <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_1219/server| (|g… expansions:
• unroll
 expr: (|count.list_1219/server| (|get.::.1_1196/server| _x_1208/server)) expansions:
• unroll
 expr: (|count.list_1219/server| _x_1208/server) expansions:
• Unsat
termination proof

### Termination proof

call group3 (List.tl (List.tl (List.tl _x))) from group3 _x
original:group3 _x
sub:group3 (List.tl (List.tl (List.tl _x)))
original ordinal:Ordinal.Int (_cnt _x)
sub ordinal:Ordinal.Int (_cnt (List.tl (List.tl (List.tl _x))))
path:[(List.tl (List.tl _x)) <> [] && (List.tl _x) <> [] && _x <> []]
proof:
detailed proof
ground_instances:12
definitions:0
inductions:0
search_time:
0.025s
details:
Expand
smt_stats:
 arith offset eqs: 56 num checks: 26 arith assert lower: 682 arith tableau max rows: 42 arith tableau max columns: 83 arith pivots: 222 rlimit count: 56304 mk clause: 570 datatype occurs check: 180 mk bool var: 1382 arith assert upper: 571 datatype splits: 39 decisions: 1450 arith row summations: 847 arith bound prop: 51 propagations: 1372 interface eqs: 4 conflicts: 83 arith fixed eqs: 326 arith assume eqs: 4 datatype accessor ax: 130 minimized lits: 8 arith conflicts: 21 arith num rows: 42 arith assert diseq: 118 datatype constructor ax: 321 num allocs: 1.79175e+08 final checks: 32 added eqs: 2047 del clause: 348 arith eq adapter: 405 time: 0.001 memory: 20.13 max memory: 20.13
Expand
• start[0.025s]
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) = count.list (count.list (const 0)) _x in
let (_x_3 : ty_0 list list) = List.tl _x_1 in
let (_x_4 : int) = count.list (count.list (const 0)) _x_3 in
let (_x_5 : ty_0 list list) = List.tl _x_3 in
_x_1 <> [] && (_x_0 <> [] && (_x <> [] && ((_x_2 >= 0) && (_x_4 >= 0))))
==> not ((List.tl _x_5) <> [] && (_x_5 <> [] && _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) = count.list (count.list (const 0)) _x_2 in let (_x_4 : int) = count.list (count.list (const 0)) _x in let (_x_5 : ty_0 list list) = List.tl _x_2 in Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_4) || not ((List.tl _x_5) <> [] && _x_5 <> [] && _x_2 <> []) || not (_x_1 <> [] && _x_0 <> [] && _x <> [] && (_x_4 >= 0) && (_x_3 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (|count.list_1284/server| (|get.::.1_1259/server| (|get.::.1_… expansions:
• unroll
 expr: (|count.list_1284/server| (|get.::.1_1259/server| (|get.::.1_1259/server| (|get.::.1_1259/serv… expansions:
• unroll
 expr: (|count.list_1284/server| _x_1273/server) expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1259/server| (|get.::.1_1259/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (|count.list_1284/server| (|get.::.1_1259/server| (|get.::.1_… expansions:
• unroll
 expr: (let ((a!1 (|get.::.0_1258/server| (|get.::.1_1259/server| (|get.::.1_12… expansions:
• unroll
 expr: (|count.list_1284/server| (|get.::.1_1259/server| _x_1273/server)) expansions:
• unroll
 expr: (|count.list_1288/server| (|get.::.0_1258/server| _x_1273/server)) expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1259/server| (|get.::.1_1259/server| (|get.::.1_12… expansions:
• unroll
 expr: (let ((a!1 (|count.list_1284/server| (|get.::.1_1259/server| (|get.::.1_… expansions:
• unroll
 expr: (let ((a!1 (|get.::.1_1259/server| (|get.::.1_1259/server| (|get.::.1_12… expansions:
• unroll
 expr: (|count.list_1284/server| (|get.::.1_1259/server| (|get.::.1_1259/server| _x_1273/server))) 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
original:zip l1 l2
sub:zip (List.tl l1) (List.tl l2)
original ordinal:Ordinal.Int (_cnt l1)
sub ordinal:Ordinal.Int (_cnt (List.tl l1))
path:[l2 <> [] && l1 <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 7 arith tableau max rows: 5 arith tableau max columns: 12 arith pivots: 6 rlimit count: 1992 mk clause: 13 datatype occurs check: 17 mk bool var: 71 arith assert upper: 7 datatype splits: 2 decisions: 13 arith row summations: 9 propagations: 14 conflicts: 7 arith fixed eqs: 4 datatype accessor ax: 14 arith conflicts: 1 arith num rows: 5 arith assert diseq: 1 datatype constructor ax: 12 num allocs: 2.09011e+08 final checks: 4 added eqs: 57 del clause: 5 arith eq adapter: 8 memory: 21.34 max memory: 21.34
Expand
• start[0.009s]
let (_x_0 : int) = count.list (const 0) l1 in
let (_x_1 : ty_0 list) = List.tl l1 in
let (_x_2 : int) = count.list (const 0) _x_1 in
l2 <> [] && (l1 <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
==> not ((List.tl l2) <> [] && _x_1 <> [])
|| 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) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) l1 in not ((List.tl l2) <> [] && _x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (l2 <> [] && l1 <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_1665/server| (|g… expansions:
• unroll
 expr: (|count.list_1665/server| (|get.::.1_1628/server| l1_1652/server)) expansions:
• unroll
 expr: (|count.list_1665/server| l1_1652/server) expansions:
• Unsat
termination proof

### Termination proof

call match_cols (List.tl y) from match_cols y
original:match_cols y
sub:match_cols (List.tl y)
original ordinal:Ordinal.Int (_cnt y)
sub ordinal:Ordinal.Int (_cnt (List.tl y))
path:[Is_a(None, (List.hd y).0) && y <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.008s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 13 arith tableau max rows: 5 arith tableau max columns: 13 arith pivots: 9 rlimit count: 9332 mk clause: 33 datatype occurs check: 27 mk bool var: 142 arith assert upper: 9 datatype splits: 6 decisions: 38 arith row summations: 15 propagations: 80 conflicts: 12 arith fixed eqs: 7 datatype accessor ax: 29 arith conflicts: 1 arith num rows: 5 datatype constructor ax: 36 num allocs: 2.8259e+08 final checks: 6 added eqs: 150 del clause: 18 arith eq adapter: 9 memory: 21.7 max memory: 21.74
Expand
• start[0.008s]
let (_x_0 : int) = count.list anon_fun._cnt.1 y in
let (_x_1 : (ty_0 option * ty_0 option) list) = List.tl y in
let (_x_2 : int) = count.list anon_fun._cnt.1 _x_1 in
let (_x_3 : (ty_0 option * ty_0 option)) = List.hd _x_1 in
let (_x_4 : ty_0 option) = _x_3.0 in
let (_x_5 : bool) = Is_a(None, _x_4) in
let (_x_6 : bool) = _x_1 <> [] in
let (_x_7 : ty_0 option) = _x_3.1 in
let (_x_8 : bool) = Is_a(None, _x_7) in
let (_x_9 : bool) = not _x_5 && _x_6 in
Is_a(None, (List.hd y).0) && (y <> [] && ((_x_0 >= 0) && (_x_2 >= 0)))
==> (not (_x_5 && _x_6)
&& (not (_x_8 && _x_9)
&& not ((Option.get _x_4 = Option.get _x_7) && (not _x_8 && _x_9))))
|| Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : (ty_0 option * ty_0 option) list) = List.tl y in let (_x_1 : (ty_0 option * ty_0 option)) = List.hd _x_0 in let (_x_2 : ty_0 option) = _x_1.0 in let (_x_3 : bool) = Is_a(None, _x_2) in let (_x_4 : bool) = _x_0 <> [] in let (_x_5 : ty_0 option) = _x_1.1 in let (_x_6 : bool) = Is_a(None, _x_5) in let (_x_7 : bool) = not _x_3 in let (_x_8 : int) = count.list anon_fun._cnt.1 _x_0 in let (_x_9 : int) = count.list anon_fun._cnt.1 y in (not (_x_3 && _x_4) && not (_x_6 && _x_7 && _x_4) && not ((Option.get _x_2 = Option.get _x_5) && not _x_6 && _x_7 && _x_4)) || Ordinal.( << ) (Ordinal.Int _x_8) (Ordinal.Int _x_9) || not (Is_a(None, (List.hd y).0) && y <> [] && (_x_9 >= 0) && (_x_8 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|count.list_1777/server| (|get.::.1_1704/server| y_1713/server)) expansions:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_1777/server| (|g… expansions:
• unroll
 expr: (|count.list_1777/server| y_1713/server) expansions:
• Unsat
call match_cols (List.tl y) from match_cols y
original:match_cols y
sub:match_cols (List.tl y)
original ordinal:Ordinal.Int (_cnt y)
sub ordinal:Ordinal.Int (_cnt (List.tl y))
path:[Is_a(None, (List.hd y).1) && not Is_a(None, (List.hd y).0) && y <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 9 arith tableau max rows: 6 arith tableau max columns: 14 arith pivots: 5 rlimit count: 6197 mk clause: 28 datatype occurs check: 24 mk bool var: 116 arith assert upper: 8 datatype splits: 4 decisions: 38 arith row summations: 14 propagations: 50 conflicts: 11 arith fixed eqs: 4 datatype accessor ax: 23 arith conflicts: 1 arith num rows: 6 arith assert diseq: 1 datatype constructor ax: 27 num allocs: 2.57785e+08 final checks: 6 added eqs: 112 del clause: 13 arith eq adapter: 8 memory: 21.68 max memory: 21.74
Expand
• start[0.009s]
let (_x_0 : (ty_0 option * ty_0 option)) = List.hd y in
let (_x_1 : int) = count.list anon_fun._cnt.1 y in
let (_x_2 : (ty_0 option * ty_0 option) list) = List.tl y in
let (_x_3 : int) = count.list anon_fun._cnt.1 _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 : bool) = Is_a(None, _x_5) in
let (_x_7 : bool) = _x_2 <> [] in
let (_x_8 : ty_0 option) = _x_4.1 in
let (_x_9 : bool) = Is_a(None, _x_8) in
let (_x_10 : bool) = not _x_6 && _x_7 in
Is_a(None, _x_0.1)
&& (not Is_a(None, _x_0.0) && (y <> [] && ((_x_1 >= 0) && (_x_3 >= 0))))
==> (not (_x_6 && _x_7)
&& (not (_x_9 && _x_10)
&& not
((Option.get _x_5 = Option.get _x_8) && (not _x_9 && _x_10))))
|| 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 : (ty_0 option * ty_0 option)) = List.hd _x_0 in let (_x_2 : ty_0 option) = _x_1.0 in let (_x_3 : bool) = Is_a(None, _x_2) in let (_x_4 : bool) = _x_0 <> [] in let (_x_5 : ty_0 option) = _x_1.1 in let (_x_6 : bool) = Is_a(None, _x_5) in let (_x_7 : bool) = not _x_3 in let (_x_8 : (ty_0 option * ty_0 option)) = List.hd y in let (_x_9 : int) = count.list anon_fun._cnt.1 y in let (_x_10 : int) = count.list anon_fun._cnt.1 _x_0 in (not (_x_3 && _x_4) && not (_x_6 && _x_7 && _x_4) && not ((Option.get _x_2 = Option.get _x_5) && not _x_6 && _x_7 && _x_4)) || not (Is_a(None, _x_8.1) && not Is_a(None, _x_8.0) && y <> [] && (_x_9 >= 0) && (_x_10 >= 0)) || Ordinal.( << ) (Ordinal.Int _x_10) (Ordinal.Int _x_9) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_1756/server| (|g… expansions:
• unroll
 expr: (|count.list_1756/server| (|get.::.1_1704/server| y_1713/server)) expansions:
• unroll
 expr: (|count.list_1756/server| y_1713/server) expansions:
• Unsat
call match_cols (List.tl y) from match_cols y
original:match_cols y
sub:match_cols (List.tl y)
original ordinal:Ordinal.Int (_cnt y)
sub ordinal:Ordinal.Int (_cnt (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 && not Is_a(None, (List.hd y).1) && not Is_a(None, (List.hd y).0) && y <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 10 arith tableau max rows: 5 arith tableau max columns: 13 arith pivots: 6 rlimit count: 3045 mk clause: 31 datatype occurs check: 22 mk bool var: 141 arith assert upper: 9 datatype splits: 3 decisions: 33 arith row summations: 15 propagations: 77 conflicts: 13 arith fixed eqs: 5 datatype accessor ax: 33 arith conflicts: 1 arith num rows: 5 arith assert diseq: 1 datatype constructor ax: 33 num allocs: 2.33535e+08 final checks: 6 added eqs: 145 del clause: 6 arith eq adapter: 9 memory: 21.74 max memory: 21.74
Expand
• start[0.009s]
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) = count.list anon_fun._cnt.1 y in
let (_x_4 : (ty_0 option * ty_0 option) list) = List.tl y in
let (_x_5 : int) = count.list anon_fun._cnt.1 _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 : bool) = Is_a(None, _x_7) in
let (_x_9 : bool) = _x_4 <> [] in
let (_x_10 : ty_0 option) = _x_6.1 in
let (_x_11 : bool) = Is_a(None, _x_10) in
let (_x_12 : bool) = not _x_8 && _x_9 in
(Option.get _x_1 = Option.get _x_2)
&& (not Is_a(None, _x_2)
&& (not Is_a(None, _x_1) && (y <> [] && ((_x_3 >= 0) && (_x_5 >= 0)))))
==> (not (_x_8 && _x_9)
&& (not (_x_11 && _x_12)
&& not
((Option.get _x_7 = Option.get _x_10) && (not _x_11 && _x_12))))
|| 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) = count.list anon_fun._cnt.1 _x_0 in let (_x_2 : int) = count.list anon_fun._cnt.1 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 : bool) = Is_a(None, _x_4) in let (_x_6 : bool) = _x_0 <> [] in let (_x_7 : ty_0 option) = _x_3.1 in let (_x_8 : bool) = Is_a(None, _x_7) in let (_x_9 : bool) = not _x_5 in let (_x_10 : (ty_0 option * ty_0 option)) = List.hd y in let (_x_11 : ty_0 option) = _x_10.0 in let (_x_12 : ty_0 option) = _x_10.1 in Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || (not (_x_5 && _x_6) && not (_x_8 && _x_9 && _x_6) && not ((Option.get _x_4 = Option.get _x_7) && not _x_8 && _x_9 && _x_6)) || not ((Option.get _x_11 = Option.get _x_12) && not Is_a(None, _x_12) && not Is_a(None, _x_11) && y <> [] && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_1732/server| (|g… expansions:
• unroll
 expr: (|count.list_1732/server| (|get.::.1_1704/server| y_1713/server)) expansions:
• unroll
 expr: (|count.list_1732/server| y_1713/server) expansions:
• Unsat
termination proof

### Termination proof

call match_rows (List.tl x) from match_rows x
original:match_rows x
sub:match_rows (List.tl x)
original ordinal:Ordinal.Int (_cnt x)
sub ordinal:Ordinal.Int (_cnt (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) && x <> []]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
 arith offset eqs: 7 num checks: 8 arith assert lower: 37 arith tableau max rows: 9 arith tableau max columns: 26 arith pivots: 21 rlimit count: 4803 mk clause: 65 datatype occurs check: 21 mk bool var: 174 arith assert upper: 40 datatype splits: 7 decisions: 68 arith row summations: 44 arith bound prop: 3 propagations: 74 conflicts: 18 arith fixed eqs: 12 datatype accessor ax: 23 minimized lits: 2 arith conflicts: 7 arith num rows: 9 arith assert diseq: 3 datatype constructor ax: 37 num allocs: 3.10591e+08 final checks: 5 added eqs: 151 del clause: 36 arith eq adapter: 31 memory: 22.02 max memory: 22.02
Expand
• start[0.010s]
let (_x_0 : (ty_0 option list * ty_0 option list)) = List.hd x in
let (_x_1 : int) = count.list anon_fun._cnt.1 x in
let (_x_2 : (ty_0 option list * ty_0 option list) list) = List.tl x in
let (_x_3 : int) = count.list anon_fun._cnt.1 _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) && (x <> [] && ((_x_1 >= 0) && (_x_3 >= 0)))
==> not (match_cols (zip _x_4.0 _x_4.1) && _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) = count.list anon_fun._cnt.1 _x_0 in let (_x_3 : int) = count.list anon_fun._cnt.1 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) && _x_0 <> []) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3) || not (match_cols (zip _x_4.0 _x_4.1) && x <> [] && (_x_3 >= 0) && (_x_2 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.list_2056/server| (|g… expansions:
• unroll
 expr: (|count.list_2056/server| (|get.::.1_2010/server| x_2041/server)) expansions:
• unroll
 expr: (|count.list_2056/server| x_2041/server) 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 283 steps, 0.998s):
let s : sudoku =
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