{                     N x N Queens
By asking the query "all Queens(n)" all solutions to the n x n queens
are computed and displayed.

The basic data structure is a dynamically allocated symbolic array 'pos' of
the type Board. The relation
               pos(r) = c
means that the queen in the row r is in the column c.

The array pos is allocated in the predicate Queens to be of the
size specified by the argument by specifying the constraint:
               Len(pos,size) 


Some solutions:

Queens(8)  :     92 solutions (     914 backtracks)
...
Queens(11) :   2680 solutions (   89393 backtracks)
Queens(12) :  14200 solutions (  467802 backtracks)
Queens(13) :  73712 solutions ( 2600469 backtracks)
Queens(14) : 365596 solutions (15419300 backtracks)
Queens(15) :2279184 solutions (96699767 backtracks)
...

}

Nl :<S = '\n'
Board = [0..]->[0..]                        {flexible array of col. positions}

pred Queens(size:<[1..]) iff
   pos::Board & Len(pos,size) &             {symbolic flexible array pos}
   Queens1(pos,0)                           {find a solution into pos}
   & Present(0,pos)                         {display the solution in pos}

pred Queens1(pos::Board,row:<I)  iff
  { the partial solution [0..row-1] in pos can be extended to [0..Len(pos] }
  if row < Len(pos) then                    {row r is not set}
    pos(row) < Len(pos) &                   {constraint on the max column}
    NoAttack(row,pos,row - 1) &             {queen r does not attack [0..r-1]}
    Queens1(pos,row + 1)                    {set the remaining queens}
  end

pred NoAttack(r:<I,pos::Board,i:<I) iff
  { the queen in the row r does not attack queens in [0..i] }
  if i >= 0 then                            
    pos(r) <> pos(i) &                      {r and i not in the same column}
    pos(r)+r <> pos(i)+i &                  {r and i not in same \ diagonal }
    pos(r)+i <> pos(i)+r &                  {r and i not in same / diagonal }
    NoAttack(r,pos,i - 1)                   {r does not attack [0..i-1] }
  end

proc Present(row:<I,pos:< Board) iff        {display a solution}
   if row < Len(pos) then 
     Print('\n      ') &
     Onerow(0,pos(row),Len(pos)) &
     Present(row+1,pos)                     {tail recursion: compiled as loop}
   end

proc Onerow(c:<I,qpos:<I,size:<I) iff       {display one row of a solution}
   if c < size then
     if c <> qpos then Print('.') else Print('*') end &
     Print(' ') &
     Onerow(c+1,qpos,size)                 
   end

      

This page was created by F1toHTML