## The N-queens problem, in Why3

How to place n queens on a nxn chessboard, Why3 version

Authors: Jean-Christophe Filliâtre

Topics: Exceptions

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```(*
VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
Problem 4: N-queens

Author: Jean-Christophe Filliatre (CNRS)
Tool:   Why3 (see http://why3.lri.fr/)
*)

module NQueens

use import int.Int
use import array.Array

predicate eq_board (b1 b2: array int) (pos: int) =
forall q:int. 0 <= q < pos -> b1[q] = b2[q]

lemma eq_board_set:
forall b: array int, pos q i: int.
pos <= q -> eq_board b b[q <- i] pos

lemma eq_board_sym:
forall b1 b2: array int, pos: int.
eq_board b1 b2 pos -> eq_board b2 b1 pos

lemma eq_board_trans:
forall b1 b2 b3: array int, pos: int.
eq_board b1 b2 pos -> eq_board b2 b3 pos -> eq_board b1 b3 pos

lemma eq_board_extension:
forall b1 b2: array int, pos: int.
eq_board b1 b2 pos -> b1[pos] = b2[pos] -> eq_board b1 b2 (pos+1)

predicate consistent_row (board: array int) (pos: int) (q: int) =
board[q] <> board[pos] /\
board[q] - board[pos] <> pos - q /\
board[pos] - board[q] <> pos - q

lemma consistent_row_eq:
forall b1 b2: array int, pos: int.
eq_board b1 b2 (pos+1) -> forall q: int. 0 <= q < pos ->
consistent_row b1 pos q -> consistent_row b2 pos q

predicate is_consistent (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> consistent_row board pos q

exception Inconsistent int

let check_is_consistent (board: array int) (pos: int)
requires { 0 <= pos < length board }
ensures { result=True <-> is_consistent board pos }
= try
for q = 0 to pos - 1 do
invariant { forall j:int. 0 <= j < q -> consistent_row board pos j }
let bq   = board[q]   in
let bpos = board[pos] in
if bq        = bpos    then raise (Inconsistent q);
if bq - bpos = pos - q then raise (Inconsistent q);
if bpos - bq = pos - q then raise (Inconsistent q)
done;
True
with Inconsistent q ->
assert { not (consistent_row board pos q) };
False
end

predicate is_board (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> 0 <= board[q] < length board

predicate solution (board: array int) (pos: int) =
is_board board pos /\
forall q:int. 0 <= q < pos -> is_consistent board q

lemma solution_eq_board:
forall b1 b2: array int, pos: int. length b1 = length b2 ->
eq_board b1 b2 pos -> solution b1 pos -> solution b2 pos

exception Solution

let rec bt_queens (board: array int) (n: int) (pos: int) variant { n - pos }
requires { length board = n /\ 0 <= pos <= n /\ solution board pos }
ensures { (* no solution *)
eq_board board (old board) pos /\
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> not (solution b n) }
raises { Solution -> solution board n }
= 'Init:
if pos = n then raise Solution;
for i = 0 to n - 1 do
invariant {
eq_board board (at board 'Init) pos /\
forall b:array int. length b = n -> is_board b n ->
eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
board[pos] <- i;
if check_is_consistent board pos then bt_queens board n (pos+1)
done

let queens (board: array int) (n: int)
requires { length board = n }
ensures { forall b:array int. length b = n -> is_board b n -> not (solution b n) }
raises { Solution -> solution board n }
= bt_queens board n 0

exception BenchFailure

let test8 () raises { BenchFailure -> true } =
let a = Array.make 8 0 in
try
queens a 8;
raise BenchFailure
with Solution -> a
end

```

variant: counting solutions (not part of the competition)

TODO: prove soundness i.e. we indeed count the number of solutions

```  use import ref.Refint

let rec count_bt_queens (board: array int) (n: int) (pos: int) : int
variant  { n - pos }
requires { length board = n /\ 0 <= pos <= n /\ solution board pos }
ensures  { eq_board board (old board) pos }
= 'Init:
if pos = n then
1
else begin
let s = ref 0 in
for i = 0 to n - 1 do
invariant { eq_board board (at board 'Init) pos }
board[pos] <- i;
if check_is_consistent board pos then
s += count_bt_queens board n (pos+1)
done;
!s
end

let count_queens (board: array int) (n: int) : int
requires { length board = n }
ensures  { true }
= count_bt_queens board n 0

let test_count_8 () =
let a = Array.make 8 0 in
count_queens a 8

end

```

counting solutions with 63-bit machine integers

```module NQueens63

use import ref.Refint
use import mach.array.Array63
use import mach.int.Int63

predicate is_board (board: array63 int63) (pos: int) =
forall q: int. 0 <= q < pos ->
0 <= to_int board[q] < to_int (length board)

exception MInconsistent

let check_is_consistent (board: array63 int63) (pos: int63)
requires { 0 <= to_int pos < to_int (length board) }
requires { is_board board (to_int pos + 1) }
= try
let q = ref (of_int 0) in
while !q < pos do
invariant { 0 <= to_int !q <= to_int pos }
invariant { is_board board (to_int pos + 1) }
variant   { to_int pos - to_int !q }
let bq   = board[!q]   in
let bpos = board[pos] in
if bq        = bpos     then raise MInconsistent;
if bq - bpos = pos - !q then raise MInconsistent;
if bpos - bq = pos - !q then raise MInconsistent;
q := !q + of_int 1
done;
True
with MInconsistent ->
False
end

use mach.peano.Peano as P

let rec count_bt_queens
(solutions: ref P.t) (board: array63 int63) (n: int63) (pos: int63)
requires { to_int (length board) = to_int n }
requires { 0 <= to_int pos <= to_int n }
requires { is_board board (to_int pos) }
variant  { to_int n - to_int pos }
ensures  { is_board board (to_int pos) }
=
if eq pos n then
solutions := P.succ !solutions
else
let i = ref (of_int 0) in
while !i < n do
invariant { 0 <= to_int !i <= to_int n }
invariant { is_board board (to_int pos) }
variant   { to_int n - to_int !i }
board[pos] <- !i;
if check_is_consistent board pos then
count_bt_queens solutions board n (pos + of_int 1);
i := !i + of_int 1
done

let count_queens (n: int63) : P.t
requires { to_int n >= 0 }
ensures  { true }
=
let solutions = ref (P.zero ()) in
let board = Array63.make n (of_int 0) in
count_bt_queens solutions board n (of_int 0);
!solutions

let test_count_8 () =
let n = of_int 8 in
count_queens n

end

```