# Sudoku¶

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

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

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

## Helpers¶

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

### Numbers¶

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

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

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

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

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

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

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

termination proof

### Termination proof

call length (List.tl _x) from length _x
originallength _x
sublength (List.tl _x)
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.017s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 10 rlimit count 1551 arith-cheap-eqs 1 mk clause 11 datatype occurs check 12 mk bool var 36 arith-lower 4 datatype splits 1 decisions 4 propagations 6 arith-max-rows 2 conflicts 3 datatype accessor ax 7 datatype constructor ax 5 num allocs 688530 final checks 4 added eqs 26 del clause 9 arith eq adapter 3 arith-upper 5 memory 5.22 max memory 5.22
Expand
• start[0.017s]
let (_x_0 : int) = count.list (const 0) _x in
let (_x_1 : ty_0 list) = List.tl _x in
let (_x_2 : int) = count.list (const 0) _x_1 in
not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 list) = List.tl _x in let (_x_1 : int) = count.list (const 0) _x_0 in let (_x_2 : int) = count.list (const 0) _x in (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list (const 0)_1697| _x_1686) expansions
• unroll
 expr (|count.list (const 0)_1697| (|get.::.1_1680| _x_1686)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list (const 0)_1697| (|get.::.… expansions
• Unsat

### Rows, columns, blocks¶

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

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

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

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

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

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

termination proof

### Termination proof

call transpose3 (List.tl _x) from transpose3 _x
originaltranspose3 _x
subtranspose3 (List.tl _x)
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[Is_a([], List.hd _x) && not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.015s
details
Expand
smt_stats
 num checks 8 arith-assume-eqs 1 arith-make-feasible 18 arith-max-columns 19 arith-conflicts 2 rlimit count 5442 mk clause 34 datatype occurs check 24 mk bool var 97 arith-lower 11 datatype splits 6 decisions 21 propagations 29 interface eqs 1 arith-max-rows 7 conflicts 7 datatype accessor ax 14 datatype constructor ax 15 num allocs 4.53445e+06 final checks 7 added eqs 77 del clause 22 arith eq adapter 9 arith-upper 16 memory 8.69 max memory 8.69
Expand
• start[0.015s]
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) = Is_a([], List.hd _x_1) in
let (_x_4 : bool) = not Is_a([], _x_1) in
Is_a([], List.hd _x) && not Is_a([], _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) = Is_a([], List.hd _x_0) in let (_x_2 : bool) = not Is_a([], _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 (((Is_a([], List.hd _x) && not Is_a([], _x)) && _x_4 >= 0) && _x_3 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_921831342_1755| _x_1742) expansions
• unroll
 expr (|count.list clos_921831342_1755| (|get.::.1_1735| _x_1742)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list clos_921831342_1755| … expansions
• Unsat

call transpose3 (List.tl _x) from transpose3 _x
originaltranspose3 _x
subtranspose3 (List.tl _x)
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[not Is_a([], List.hd _x) && not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 8 arith-assume-eqs 1 arith-make-feasible 24 arith-max-columns 19 arith-conflicts 2 rlimit count 2825 mk clause 38 datatype occurs check 27 mk bool var 114 arith-lower 15 datatype splits 9 decisions 29 propagations 35 interface eqs 1 arith-max-rows 7 conflicts 9 datatype accessor ax 17 datatype constructor ax 18 num allocs 2.86219e+06 final checks 7 added eqs 93 del clause 26 arith eq adapter 13 arith-upper 21 memory 6.09 max memory 6.09
Expand
• start[0.014s]
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) = Is_a([], List.hd _x_1) in
let (_x_4 : bool) = not Is_a([], _x_1) in
not Is_a([], List.hd _x) && not Is_a([], _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) = Is_a([], List.hd _x_0) in let (_x_2 : bool) = not Is_a([], _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 Is_a([], List.hd _x) && not Is_a([], _x)) && _x_4 >= 0) && _x_3 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_921831342_1755| _x_1742) expansions
• unroll
 expr (|count.list clos_921831342_1755| (|get.::.1_1735| _x_1742)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list clos_921831342_1755| … expansions
• Unsat

termination proof

### Termination proof

call get_heads (List.tl _x) from get_heads _x
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[Is_a([], List.hd _x) && not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.014s
details
Expand
smt_stats
 num checks 8 arith-assume-eqs 1 arith-make-feasible 18 arith-max-columns 19 arith-conflicts 2 rlimit count 5442 mk clause 34 datatype occurs check 24 mk bool var 97 arith-lower 11 datatype splits 6 decisions 21 propagations 29 interface eqs 1 arith-max-rows 7 conflicts 7 datatype accessor ax 14 datatype constructor ax 15 num allocs 1.37734e+07 final checks 7 added eqs 77 del clause 22 arith eq adapter 9 arith-upper 16 memory 8.99 max memory 8.99
Expand
• start[0.014s]
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) = Is_a([], List.hd _x_1) in
let (_x_4 : bool) = not Is_a([], _x_1) in
Is_a([], List.hd _x) && not Is_a([], _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) = Is_a([], List.hd _x_0) in let (_x_2 : bool) = not Is_a([], _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 (((Is_a([], List.hd _x) && not Is_a([], _x)) && _x_4 >= 0) && _x_3 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_148560117_1865| _x_1852) expansions
• unroll
 expr (|count.list clos_148560117_1865| (|get.::.1_1845| _x_1852)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list clos_148560117_1865| … expansions
• Unsat

call get_heads (List.tl _x) from get_heads _x
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[not Is_a([], List.hd _x) && not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 8 arith-assume-eqs 1 arith-make-feasible 24 arith-max-columns 19 arith-conflicts 2 rlimit count 2825 mk clause 38 datatype occurs check 27 mk bool var 114 arith-lower 15 datatype splits 9 decisions 29 propagations 35 interface eqs 1 arith-max-rows 7 conflicts 9 datatype accessor ax 17 datatype constructor ax 18 num allocs 1.09415e+07 final checks 7 added eqs 93 del clause 26 arith eq adapter 13 arith-upper 21 memory 6.43 max memory 8.69
Expand
• start[0.013s]
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) = Is_a([], List.hd _x_1) in
let (_x_4 : bool) = not Is_a([], _x_1) in
not Is_a([], List.hd _x) && not Is_a([], _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) = Is_a([], List.hd _x_0) in let (_x_2 : bool) = not Is_a([], _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 Is_a([], List.hd _x) && not Is_a([], _x)) && _x_4 >= 0) && _x_3 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_148560117_1865| _x_1852) expansions
• unroll
 expr (|count.list clos_148560117_1865| (|get.::.1_1845| _x_1852)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list clos_148560117_1865| … expansions
• Unsat

termination proof

### Termination proof

call transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) from transpose l
originaltranspose l
subtranspose ((List.tl (List.hd l)) :: (transpose3 (List.tl l)))
original ordinallet (_x_0 : int) = measure_transpose l in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
sub ordinallet (_x_0 : int) = measure_transpose ((List.tl (List.hd l)) :: (transpose3 (List.tl l))) in Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)
path[not Is_a([], List.hd l) && not Is_a([], l)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.013s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 9 rlimit count 1881 mk clause 8 datatype occurs check 13 mk bool var 41 arith-lower 2 datatype splits 2 decisions 6 propagations 4 arith-max-rows 2 conflicts 3 datatype accessor ax 11 datatype constructor ax 9 num allocs 2.38384e+07 final checks 4 added eqs 35 del clause 8 arith eq adapter 2 arith-upper 5 memory 6.77 max memory 8.99
Expand
• start[0.013s]
let (_x_0 : ty_0 list) = List.hd l in
let (_x_1 : bool) = Is_a([], l) in
let (_x_2 : int) = if _x_1 then 0 else List.length _x_0 in
let (_x_3 : int) = if _x_2 >= 0 then _x_2 else 0 in
let (_x_4 : int) = List.length … in
let (_x_5 : int) = if _x_4 >= 0 then _x_4 else 0 in
not Is_a([], _x_0) && not _x_1 && _x_3 >= 0 && _x_5 >= 0
==> Is_a([], 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) = Is_a([], l) in let (_x_5 : bool) = _x_4 || _x_3 >= 0 in (Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 0 then _x_2 else 0)) (Ordinal.Int (if _x_5 then if _x_4 then 0 else _x_3 else 0))) || not ((not Is_a([], _x_0) && not _x_4) && (_x_5 || not _x_5)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|List.length_2018| (|get.::.0_1990| l_2010)) expansions
• unroll
 expr (|List.length_2018| (|get.::.1_1988| (|get.::.0_1990| l_2010))) expansions
• unroll
 expr (let ((a!1 (>= (|List.length_2018| (|get.::.1_1988| (|get.::.0_1990| l_2010))) 0)) … expansions
• Unsat

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

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

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

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

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

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

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

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

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

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

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

(*

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

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

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

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

termination proof

### Termination proof

call take (Destruct(S, 0, x)) (List.tl l) from take x l
originaltake x l
subtake (Destruct(S, 0, x)) (List.tl l)
original ordinalOrdinal.Int (_cnt x)
sub ordinalOrdinal.Int (_cnt (Destruct(S, 0, x)))
path[not Is_a([], l) && not Is_a(Z, x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.012s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 10 rlimit count 1720 arith-cheap-eqs 1 mk clause 11 datatype occurs check 17 mk bool var 48 arith-lower 4 datatype splits 2 decisions 8 propagations 5 arith-max-rows 2 conflicts 3 datatype accessor ax 12 datatype constructor ax 10 num allocs 3.17781e+07 final checks 4 added eqs 40 del clause 9 arith eq adapter 3 arith-upper 5 memory 7.05 max memory 8.99
Expand
• start[0.012s]
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
not Is_a([], l) && not Is_a(Z, x) && _x_0 >= 0 && _x_2 >= 0
==> not (not Is_a([], List.tl l) && not Is_a(Z, _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 (not Is_a([], List.tl l) && not Is_a(Z, _x_0)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not Is_a([], l) && not Is_a(Z, x)) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.nat_17| x_2082) expansions
• unroll
 expr (|count.nat_17| (|get.S.0_2072| x_2082)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.nat_17| (|get.S.0_2072| x_2082))) (|O… expansions
• Unsat

termination proof

### Termination proof

call drop (Destruct(S, 0, x)) (List.tl y) from drop x y
originaldrop x y
subdrop (Destruct(S, 0, x)) (List.tl y)
original ordinalOrdinal.Int (_cnt x)
sub ordinalOrdinal.Int (_cnt (Destruct(S, 0, x)))
path[not Is_a([], y) && not Is_a(Z, x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.012s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 10 rlimit count 1720 arith-cheap-eqs 1 mk clause 11 datatype occurs check 17 mk bool var 48 arith-lower 4 datatype splits 2 decisions 8 propagations 5 arith-max-rows 2 conflicts 3 datatype accessor ax 12 datatype constructor ax 10 num allocs 4.07336e+07 final checks 4 added eqs 40 del clause 9 arith eq adapter 3 arith-upper 5 memory 7.3 max memory 8.99
Expand
• start[0.012s]
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
not Is_a([], y) && not Is_a(Z, x) && _x_0 >= 0 && _x_2 >= 0
==> not (not Is_a([], List.tl y) && not Is_a(Z, _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 (not Is_a([], List.tl y) && not Is_a(Z, _x_0)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not Is_a([], y) && not Is_a(Z, x)) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.nat_17| x_2132) expansions
• unroll
 expr (|count.nat_17| (|get.S.0_2122| x_2132)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.nat_17| (|get.S.0_2122| x_2132))) (|O… expansions
• Unsat

termination proof

### Termination proof

call elem x (List.tl y) from elem x y
originalelem x y
subelem x (List.tl y)
original ordinalOrdinal.Int (_cnt y)
sub ordinalOrdinal.Int (_cnt (List.tl y))
path[not (x = List.hd y) && not Is_a([], y)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.012s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 10 rlimit count 1675 arith-cheap-eqs 1 mk clause 11 datatype occurs check 12 mk bool var 38 arith-lower 4 datatype splits 1 decisions 4 propagations 6 arith-max-rows 2 conflicts 3 datatype accessor ax 7 datatype constructor ax 5 num allocs 5.11525e+07 final checks 4 added eqs 26 del clause 9 arith eq adapter 3 arith-upper 5 memory 7.54 max memory 8.99
Expand
• start[0.012s]
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) && not Is_a([], y) && _x_0 >= 0 && _x_2 >= 0
==> not (not (x = List.hd _x_1) && not Is_a([], _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) && not Is_a([], _x_0)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not (x = List.hd y) && not Is_a([], y)) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list (const 0)_2193| y_2181) expansions
• unroll
 expr (|count.list (const 0)_2193| (|get.::.1_2174| y_2181)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list (const 0)_2193| (|get.::.… expansions
• Unsat

termination proof

### Termination proof

call unique (List.tl x) from unique x
originalunique x
subunique (List.tl x)
original ordinalOrdinal.Int (_cnt x)
sub ordinalOrdinal.Int (_cnt (List.tl x))
path[not (elem (List.hd x) (List.tl x)) && not Is_a([], x)]
proof
detailed proof
ground_instances4
definitions0
inductions0
search_time
0.012s
details
Expand
smt_stats
 num checks 9 arith-make-feasible 8 arith-max-columns 10 rlimit count 2055 arith-cheap-eqs 1 mk clause 11 datatype occurs check 15 mk bool var 44 arith-lower 4 datatype splits 1 decisions 5 propagations 6 arith-max-rows 2 conflicts 4 datatype accessor ax 8 datatype constructor ax 6 num allocs 6.22876e+07 final checks 5 added eqs 28 del clause 9 arith eq adapter 3 arith-upper 5 memory 7.79 max memory 8.99
Expand
• start[0.012s]
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) && not Is_a([], x) && _x_1 >= 0 && _x_2 >= 0
==> not (not (elem (List.hd _x_0) (List.tl _x_0)) && not Is_a([], _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)) && not Is_a([], _x_0)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not (elem (List.hd x) _x_0) && not Is_a([], x)) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (elem_2230 (|get.::.0_2224| x_2235) (|get.::.1_2225| x_2235)) expansions
• unroll
 expr (|count.list (const 0)_2246| x_2235) expansions
• unroll
 expr (|count.list (const 0)_2246| (|get.::.1_2225| x_2235)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list (const 0)_2246| (|get.::.… expansions
• Unsat

termination proof

### Termination proof

call keep_some_list (List.tl l) from keep_some_list l
originalkeep_some_list l
subkeep_some_list (List.tl l)
original ordinalOrdinal.Int (_cnt l)
sub ordinalOrdinal.Int (_cnt (List.tl l))
path[not Is_a([], l)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.011s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 11 rlimit count 1660 arith-cheap-eqs 1 mk clause 10 datatype occurs check 14 mk bool var 43 arith-lower 4 datatype splits 3 decisions 11 propagations 5 arith-max-rows 2 conflicts 3 datatype accessor ax 10 datatype constructor ax 11 num allocs 7.45563e+07 final checks 4 added eqs 36 del clause 8 arith eq adapter 3 arith-upper 5 memory 8.04 max memory 8.99
Expand
• start[0.011s]
let (_x_0 : int) = count.list (count.option (const 0)) l in
let (_x_1 : ty_0 option list) = List.tl l in
let (_x_2 : int) = count.list (count.option (const 0)) _x_1 in
not Is_a([], l) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ##### simplify
 into let (_x_0 : ty_0 option list) = List.tl l in let (_x_1 : int) = count.list (count.option (const 0)) _x_0 in let (_x_2 : int) = count.list (count.option (const 0)) l in (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], l) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_976953524_2302| l_2291) expansions
• unroll
 expr (|count.list clos_976953524_2302| (|get.::.1_2281| l_2291)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list clos_976953524_2302| … expansions
• Unsat

termination proof

### Termination proof

call blocks_3_34 (List.tl _x) from blocks_3_34 _x
originalblocks_3_34 _x
subblocks_3_34 (List.tl _x)
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.028s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 19 arith-max-columns 16 arith-conflicts 2 rlimit count 2373 mk clause 21 datatype occurs check 14 mk bool var 69 arith-lower 16 arith-diseq 1 datatype splits 3 decisions 19 propagations 15 arith-max-rows 4 conflicts 7 datatype accessor ax 10 datatype constructor ax 11 num allocs 8.84643e+07 final checks 4 added eqs 54 del clause 14 arith eq adapter 11 arith-upper 13 memory 8.46 max memory 8.99
Expand
• start[0.028s]
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
not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _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 (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_790807200_2390| _x_2379) expansions
• unroll
 expr (|count.list clos_790807200_2390| (|get.::.1_2367| _x_2379)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list clos_790807200_2390| … expansions
• Unsat

termination proof

### Termination proof

call blocks_3_33 (List.tl _x) from blocks_3_33 _x
originalblocks_3_33 _x
subblocks_3_33 (List.tl _x)
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.012s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 19 arith-max-columns 16 arith-conflicts 2 rlimit count 2373 mk clause 21 datatype occurs check 14 mk bool var 69 arith-lower 16 arith-diseq 1 datatype splits 3 decisions 19 propagations 15 arith-max-rows 4 conflicts 7 datatype accessor ax 10 datatype constructor ax 11 num allocs 1.03363e+08 final checks 4 added eqs 54 del clause 14 arith eq adapter 11 arith-upper 13 memory 8.72 max memory 8.99
Expand
• start[0.012s]
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
not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _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 (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_661142004_2458| _x_2447) expansions
• unroll
 expr (|count.list clos_661142004_2458| (|get.::.1_2429| _x_2447)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list clos_661142004_2458| … expansions
• Unsat

termination proof

### Termination proof

call blocks_3_32 (List.tl _x) from blocks_3_32 _x
originalblocks_3_32 _x
subblocks_3_32 (List.tl _x)
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl _x))
path[not Is_a([], _x)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.023s
details
Expand
smt_stats
 num checks 8 arith-make-feasible 19 arith-max-columns 16 arith-conflicts 2 rlimit count 2373 mk clause 21 datatype occurs check 14 mk bool var 69 arith-lower 16 arith-diseq 1 datatype splits 3 decisions 19 propagations 15 arith-max-rows 4 conflicts 7 datatype accessor ax 10 datatype constructor ax 11 num allocs 1.19413e+08 final checks 4 added eqs 54 del clause 14 arith eq adapter 11 arith-upper 13 memory 8.98 max memory 8.99
Expand
• start[0.023s]
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
not Is_a([], _x) && _x_0 >= 0 && _x_2 >= 0
==> Is_a([], _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 (Is_a([], _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not ((not Is_a([], _x) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_388039378_2520| _x_2509) expansions
• unroll
 expr (|count.list clos_388039378_2520| (|get.::.1_2497| _x_2509)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list clos_388039378_2520| … expansions
• Unsat

termination proof

### Termination proof

call group3 (List.tl (List.tl (List.tl _x))) from group3 _x
originalgroup3 _x
subgroup3 (List.tl (List.tl (List.tl _x)))
original ordinalOrdinal.Int (_cnt _x)
sub ordinalOrdinal.Int (_cnt (List.tl (List.tl (List.tl _x))))
path[not Is_a([], List.tl (List.tl _x)) && not Is_a([], List.tl _x) && not Is_a([], _x)]
proof
detailed proof
ground_instances8
definitions0
inductions0
search_time
0.027s
details
Expand
smt_stats
 num checks 18 arith-assume-eqs 8 arith-make-feasible 236 arith-max-columns 54 arith-conflicts 17 rlimit count 13124 arith-cheap-eqs 72 mk clause 321 datatype occurs check 75 mk bool var 669 arith-lower 197 arith-diseq 31 datatype splits 19 decisions 308 arith-propagations 22 propagations 322 interface eqs 8 arith-bound-propagations-cheap 22 arith-max-rows 25 conflicts 51 datatype accessor ax 52 minimized lits 7 arith-bound-propagations-lp 28 datatype constructor ax 133 num allocs 1.30696e+08 final checks 27 added eqs 716 del clause 180 arith eq adapter 170 arith-upper 227 time 0.001 memory 12.33 max memory 12.33
Expand
• start[0.027s]
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
not Is_a([], _x_1)
&& not Is_a([], _x_0) && not Is_a([], _x) && _x_2 >= 0 && _x_4 >= 0
==> not
(not Is_a([], List.tl _x_5) && not Is_a([], _x_5) && not Is_a([], _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 ((not Is_a([], List.tl _x_5) && not Is_a([], _x_5)) && not Is_a([], _x_2))) || not ((((not Is_a([], _x_1) && not Is_a([], _x_0)) && not Is_a([], _x)) && _x_4 >= 0) && _x_3 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list clos_592014680_2584| _x_2573) expansions
• unroll
 expr (|count.list clos_592014680_2584| (|get.::.1_2559| (|get.::.1_2559| (|get.::.1_2559| _x_2573)… expansions
• unroll
 expr (let ((a!1 (|count.list clos_592014680_2584| (|get.::.1_2559| (|get.::.1_2559| (|g… expansions
• unroll
 expr (|count.list clos_592014680_2584| (|get.::.1_2559| _x_2573)) expansions
• unroll
 expr (|count.list (const 0)_2588| (|get.::.0_2558| _x_2573)) expansions
• unroll
 expr (let ((a!1 (|get.::.1_2559| (|get.::.1_2559| (|get.::.1_2559| (|get.::.1_2559| _x_2573)))))) (|co… expansions
• unroll
 expr (let ((a!1 (|get.::.0_2558| (|get.::.1_2559| (|get.::.1_2559| (|get.::.1_2559| _x_2573)))))) (|co… expansions
• unroll
 expr (|count.list clos_592014680_2584| (|get.::.1_2559| (|get.::.1_2559| _x_2573))) expansions
• Unsat

## The Sudoku type¶

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

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

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

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

#install_doc doc_of_cell;;

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


And the sudoku itself:

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

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

#install_doc doc_of_sudoku;;

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


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

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

Out:
val the_problem : sudoku = <document>

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

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

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

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

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


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

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

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

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

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

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

termination proof

### Termination proof

call zip (List.tl l1) (List.tl l2) from zip l1 l2
originalzip l1 l2
subzip (List.tl l1) (List.tl l2)
original ordinalOrdinal.Int (_cnt l1)
sub ordinalOrdinal.Int (_cnt (List.tl l1))
path[not Is_a([], l2) && not Is_a([], l1)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.026s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 10 rlimit count 1730 arith-cheap-eqs 1 mk clause 11 datatype occurs check 17 mk bool var 50 arith-lower 4 datatype splits 2 decisions 8 propagations 5 arith-max-rows 2 conflicts 3 datatype accessor ax 12 datatype constructor ax 10 num allocs 1.55901e+08 final checks 4 added eqs 42 del clause 9 arith eq adapter 3 arith-upper 5 memory 13.67 max memory 13.67
Expand
• start[0.026s]
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
not Is_a([], l2) && not Is_a([], l1) && _x_0 >= 0 && _x_2 >= 0
==> not (not Is_a([], List.tl l2) && not Is_a([], _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 (not Is_a([], List.tl l2) && not Is_a([], _x_0)) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)) || not (((not Is_a([], l2) && not Is_a([], l1)) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list (const 0)_2963| l1_2950) expansions
• unroll
 expr (|count.list (const 0)_2963| (|get.::.1_2926| l1_2950)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list (const 0)_2963| (|get.::.… expansions
• Unsat

termination proof

### Termination proof

call match_cols (List.tl y) from match_cols y
originalmatch_cols y
submatch_cols (List.tl y)
original ordinalOrdinal.Int (_cnt y)
sub ordinalOrdinal.Int (_cnt (List.tl y))
path[Is_a(None, (List.hd y).0) && not Is_a([], y)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 8 arith-max-columns 12 rlimit count 6624 arith-cheap-eqs 2 mk clause 26 datatype occurs check 24 mk bool var 86 arith-lower 4 datatype splits 6 decisions 16 propagations 23 arith-max-rows 3 conflicts 4 datatype accessor ax 18 datatype constructor ax 19 num allocs 1.99166e+08 final checks 6 added eqs 81 del clause 6 arith eq adapter 3 arith-upper 5 memory 19.23 max memory 19.23
Expand
• start[0.016s]
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) = not Is_a([], _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) && not Is_a([], 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) = not Is_a([], _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) && not Is_a([], y)) && _x_9 >= 0) && _x_8 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list anon_fun._cnt.1_3078| y_3010) expansions
• unroll
 expr (|count.list anon_fun._cnt.1_3078| (|get.::.1_3001| y_3010)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list anon_fun._cnt.1_3078| … expansions
• Unsat

call match_cols (List.tl y) from match_cols y
originalmatch_cols y
submatch_cols (List.tl y)
original ordinalOrdinal.Int (_cnt y)
sub ordinalOrdinal.Int (_cnt (List.tl y))
path[Is_a(None, (List.hd y).1) && not Is_a(None, (List.hd y).0) && not Is_a([], y)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 8 arith-max-columns 12 rlimit count 4445 arith-cheap-eqs 2 mk clause 26 datatype occurs check 21 mk bool var 84 arith-lower 4 datatype splits 3 decisions 12 propagations 24 arith-max-rows 3 conflicts 4 datatype accessor ax 19 datatype constructor ax 17 num allocs 1.87846e+08 final checks 6 added eqs 79 del clause 6 arith eq adapter 3 arith-upper 5 memory 16.62 max memory 16.62
Expand
• start[0.016s]
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) = not Is_a([], _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) && not Is_a([], 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) = not Is_a([], _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 let (_x_10 : (ty_0 option * ty_0 option)) = List.hd 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, _x_10.1) && not Is_a(None, _x_10.0)) && not Is_a([], y)) && _x_9 >= 0) && _x_8 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list anon_fun._cnt.1_3055| y_3010) expansions
• unroll
 expr (|count.list anon_fun._cnt.1_3055| (|get.::.1_3001| y_3010)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list anon_fun._cnt.1_3055| … expansions
• Unsat

call match_cols (List.tl y) from match_cols y
originalmatch_cols y
submatch_cols (List.tl y)
original ordinalOrdinal.Int (_cnt y)
sub ordinalOrdinal.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) && not Is_a([], y)]
proof
detailed proof
ground_instances3
definitions0
inductions0
search_time
0.016s
details
Expand
smt_stats
 num checks 7 arith-make-feasible 7 arith-max-columns 12 rlimit count 2256 arith-cheap-eqs 2 mk clause 25 datatype occurs check 21 mk bool var 86 arith-lower 4 datatype splits 3 decisions 12 propagations 24 arith-max-rows 3 conflicts 4 datatype accessor ax 19 datatype constructor ax 17 num allocs 1.77037e+08 final checks 6 added eqs 81 del clause 5 arith eq adapter 3 arith-upper 5 memory 14.04 max memory 14.04
Expand
• start[0.016s]
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) = not Is_a([], _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) && not Is_a([], 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) = not Is_a([], _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)) && not Is_a([], y)) && _x_2 >= 0) && _x_1 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|count.list anon_fun._cnt.1_3029| y_3010) expansions
• unroll
 expr (|count.list anon_fun._cnt.1_3029| (|get.::.1_3001| y_3010)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list anon_fun._cnt.1_3029| … expansions
• Unsat

termination proof

### Termination proof

call match_rows (List.tl x) from match_rows x
originalmatch_rows x
submatch_rows (List.tl x)
original ordinalOrdinal.Int (_cnt x)
sub ordinalOrdinal.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) && not Is_a([], x)]
proof
detailed proof
ground_instances5
definitions0
inductions0
search_time
0.018s
details
Expand
smt_stats
 num checks 12 arith-assume-eqs 3 arith-make-feasible 59 arith-max-columns 33 arith-conflicts 4 rlimit count 7104 arith-cheap-eqs 20 mk clause 91 datatype occurs check 79 mk bool var 261 arith-lower 34 arith-diseq 3 datatype splits 23 decisions 139 arith-propagations 2 propagations 73 interface eqs 3 arith-bound-propagations-cheap 2 arith-max-rows 15 conflicts 15 datatype accessor ax 40 minimized lits 1 datatype constructor ax 68 num allocs 2.3579e+08 final checks 13 added eqs 280 del clause 44 arith eq adapter 33 arith-upper 52 memory 17.16 max memory 19.23
Expand
• start[0.018s]
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) && not Is_a([], x) && _x_1 >= 0 && _x_3 >= 0
==> not (match_cols (zip _x_4.0 _x_4.1) && not Is_a([], _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) && not Is_a([], _x_0)) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_3)) || not (((match_cols (zip _x_4.0 _x_4.1) && not Is_a([], x)) && _x_3 >= 0) && _x_2 >= 0) expansions [] rewrite_steps forward_chaining
• unroll
 expr (zip_3326 (|tuple_get.0_3308| (|get.::.0_3311| x_3343)) (|tuple_get.1_3309| (|get.::.0_331… expansions
• unroll
 expr (match_cols_3335 (zip_3326 (|tuple_get.0_3308| (|get.::.0_3311| x_3343)) … expansions
• unroll
 expr (|count.list anon_fun._cnt.1_3358| x_3343) expansions
• unroll
 expr (|count.list anon_fun._cnt.1_3358| (|get.::.1_3312| x_3343)) expansions
• unroll
 expr (|Ordinal.<<_126| (|Ordinal.Int_111| (|count.list anon_fun._cnt.1_3358| … 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, 1.635s):
let s =
let (_x_0 : cell option) = Some C8 in
let (_x_1 : cell option) = Some C1 in
let (_x_2 : cell option) = Some C2 in
let (_x_3 : cell option) = Some C7 in
let (_x_4 : cell option) = Some C5 in
let (_x_5 : cell option) = Some C3 in
let (_x_6 : cell option) = Some C6 in
let (_x_7 : cell option) = Some C4 in
let (_x_8 : cell option) = Some C9 in
{rows =
[[_x_0; _x_1; _x_2; _x_3; _x_4; _x_5; _x_6; _x_7; _x_8];
[_x_8; _x_7; _x_5; _x_6; _x_0; _x_2; _x_1; _x_3; _x_4];
[_x_6; _x_3; _x_4; _x_7; _x_8; _x_1; _x_2; _x_0; _x_5];
[_x_1; _x_4; _x_7; _x_2; _x_5; _x_3; _x_0; _x_8; _x_6];
[_x_5; _x_6; _x_8; _x_0; _x_7; _x_4; _x_3; _x_2; _x_1];
[_x_2; _x_0; _x_3; _x_1; _x_6; _x_8; _x_4; _x_5; _x_7];
[_x_4; _x_2; _x_1; _x_8; _x_3; _x_7; _x_5; _x_6; _x_0];
[_x_7; _x_5; _x_0; _x_4; _x_2; _x_6; _x_8; _x_1; _x_3];
[_x_3; _x_8; _x_6; _x_5; _x_1; _x_0; _x_7; _x_4; _x_2]]}

Instance

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

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

Out:
- : unit = ()

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

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

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

transpose_sudoku CX.s;;

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

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