Wiki Agenda Contact Version française

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

References: The 1st Verified Software Competition / The VerifyThis Benchmarks

See also: The N-queens problem, in C with Caduceus tool

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


download ZIP archive

Why3 Proof Results for Project "vstte10_queens"

Theory "vstte10_queens.NQueens": fully verified in 1.91 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)CVC4 (1.4)Z3 (3.2)
eq_board_set0.00---------
eq_board_sym0.01---------
eq_board_trans0.01---------
eq_board_extension0.01---------
consistent_row_eq0.06---------
VC for check_is_consistent---0.02------
solution_eq_board---------0.06
VC for bt_queens---1.42------
VC for queens0.02---------
VC for test80.01---------
VC for count_bt_queens------0.27---
VC for count_queens0.01---------
VC for test_count_80.01---------

Theory "vstte10_queens.NQueens63": fully verified in 1.06 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)Z3 (4.3.2)
VC for check_is_consistent---0.09---
VC for count_bt_queens---------
split_goal_wp
  1. postcondition0.02------
2. integer overflow0.02------
3. loop invariant init0.02------
4. loop invariant init0.02------
5. type invariant0.02------
6. index in array63 bounds0.02------
7. precondition0.02------
8. precondition0.17------
9. integer overflow0.02------
10. integer overflow0.04------
11. variant decrease0.02------
12. precondition0.02------
13. precondition0.02------
14. precondition0.000.05---
15. integer overflow0.02------
16. integer overflow0.13------
17. loop invariant preservation0.02------
18. loop invariant preservation0.02------
19. loop variant decrease0.02------
20. integer overflow0.01------
21. integer overflow0.02------
22. loop invariant preservation0.02------
23. loop invariant preservation0.11------
24. loop variant decrease0.02------
25. type invariant0.020.05---
26. postcondition0.01------
VC for count_queens0.01------
VC for test_count_80.00---0.01