Wiki Agenda Contact Version française

Computing the number of solutions to the N-queens puzzle


Authors: Jean-Christophe Filliâtre

Topics: Ghost code

Tools: Why3

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


(* Verification of the following 2-lines C program solving the N-queens puzzle:

   t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,(
   c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}
*)

theory S "finite sets of with succ and pred operations"

  use export set.Fsetint

  function succ (set int) : set int

  axiom succ_def:
    forall s: set int, i: int. mem i (succ s) <-> i >= 1 /\ mem (i-1) s

  function pred (set int) : set int

  axiom pred_def:
    forall s: set int, i: int. mem i (pred s) <-> i >= 0 /\ mem (i+1) s

end

module NQueensSetsTermination

  use import S
  use import ref.Refint

  let rec t (a b c : set int) variant { cardinal a } =
    if not (is_empty a) then begin
      let e = ref (diff (diff a b) c) in
      let f = ref 0 in
   'L:while not (is_empty !e) do
        invariant { subset !e (diff (diff a b) c) }
        variant { cardinal !e }
        let d = min_elt !e in
        f += t (remove d a) (succ (add d b)) (pred (add d c));
        e := remove d !e
      done;
      !f
    end else
      1

end

theory Solution

  use import int.Int
  use export map.Map

  (* the number of queens *)
  constant n : int

  type solution = map int int

  (* solutions t and u have the same prefix [0..i[ *)
  predicate eq_prefix (t u: map int 'a) (i: int) =
    forall k: int. 0 <= k < i -> t[k] = u[k]

  predicate eq_sol (t u: solution) = eq_prefix t u n

  (* s stores a partial solution, for the rows 0..k-1 *)
  predicate partial_solution (k: int) (s: solution) =
    forall i: int. 0 <= i < k ->
      0 <= s[i] < n /\
      (forall j: int. 0 <= j < i -> s[i]      <> s[j] /\
                                    s[i]-s[j] <> i-j  /\
                                    s[i]-s[j] <> j-i)

  predicate solution (s: solution) = partial_solution n s

  lemma partial_solution_eq_prefix:
    forall u t: solution, k: int.
    partial_solution k t -> eq_prefix t u k -> partial_solution k u

  predicate lt_sol (s1 s2: solution) =
    exists i: int. 0 <= i < n /\ eq_prefix s1 s2 i /\ s1[i] < s2[i]

  type solutions = map int solution

  (* s[a..b[ is sorted for lt_sol *)
  predicate sorted (s: solutions) (a b: int) =
    forall i j: int. a <= i < j < b -> lt_sol s[i] s[j]

  (* a sorted array of solutions contains no duplicate *)
  lemma no_duplicate:
    forall s: solutions, a b: int. sorted s a b ->
    forall i j: int. a <= i < j < b -> not (eq_sol s[i] s[j])

end

(* 1. Abstract version of the code using sets (not ints) *******************)

module NQueensSets

  use import S
  use import ref.Refint
  use import Solution

  val ghost col: ref solution  (* solution under construction *)
  val ghost k  : ref int       (* current row in the current solution *)

  val ghost sol: ref solutions (* all solutions *)
  val ghost s  : ref int       (* next slot for a solution
                                  = current number of solutions *)

  let rec t3 (a b c : set int) variant { cardinal a }
    requires { 0 <= !k /\ !k + cardinal a = n /\ !s >= 0 /\
      (forall i: int. mem i a <->
        (0<=i<n /\ forall j: int. 0 <= j < !k ->  !col[j] <> i)) /\
      (forall i: int. i>=0 -> (not (mem i b) <->
        (forall j: int. 0 <= j < !k -> !col[j] <> i + j - !k))) /\
      (forall i: int. i>=0 -> (not (mem i c) <->
        (forall j: int. 0 <= j < !k -> !col[j] <> i + !k - j))) /\
      partial_solution !k !col }
    ensures { result = !s - old !s >= 0 /\ !k = old !k /\
      sorted !sol (old !s) !s /\
      (forall t: solution.
         ((solution t /\ eq_prefix !col t !k) <->
          (exists i: int. old !s <= i < !s /\ eq_sol t !sol[i]))) /\
      (* assigns *)
      eq_prefix (old !col) !col !k /\
      eq_prefix (old !sol) !sol (old !s) }
  = if not (is_empty a) then begin
      let e = ref (diff (diff a b) c) in
      let f = ref 0 in
   'L:while not (is_empty !e) do
        invariant {
          !f = !s - at !s 'L >= 0 /\ !k = at !k 'L /\
          subset !e (diff (diff a b) c) /\
          partial_solution !k !col /\
          sorted !sol (at !s 'L) !s /\
          (forall i j: int. mem i (diff (at !e 'L) !e) -> mem j !e -> i < j) /\
          (forall t: solution.
           (solution t /\ eq_prefix !col t !k /\ mem t[!k] (diff (at !e 'L) !e))
           <->
           (exists i: int. (at !s 'L) <= i < !s /\ eq_sol t !sol[i])) /\
          (* assigns *)
          eq_prefix (at !col 'L) !col !k /\
          eq_prefix (at !sol 'L) !sol (at !s 'L) }
        variant { cardinal !e }
        let d = min_elt !e in
        ghost col := !col[!k <- d];
        ghost incr k;
        f += t3 (remove d a) (succ (add d b)) (pred (add d c));
        ghost decr k;
        e := remove d !e
      done;
      !f
    end else begin
      ghost sol := !sol[!s <- !col];
      ghost incr s;
      1
    end

  let queens3 (q: int)
    requires { 0 <= q = n /\ !s = 0 /\ !k = 0 }
    ensures { result = !s /\ sorted !sol 0 !s /\
      forall t: solution.
        solution t <-> (exists i: int. 0 <= i < result /\ eq_sol t !sol[i]) }
  = t3 (interval 0 q) empty empty

end

download ZIP archive