Our next example is the classic Eight Queens Problem
[Hen1980]. Given a chessboard and eight
queens, one must place the queens on the board so that no two queens hold each other in check;
that is, no two queens may lie in the same row, column, or diagonal.
We shall consider a slightly more general problem of placing n queens on the
board of the size n*n.
Let the rows and columns of the board be numbered from 1 to
n. A chessboard square is said to have the coordinates
(i,j), or, in other words, to be the square (i,j), if it
lies in column i and row j.
Note that all squares lying in the same diagonal running upwards from left to right have the
same sum of the column and row numbers, whereas all squares lying in the same diagonal running
downwards from left to right have the same difference of the column and row numbers.
Thus two squares (i,j) and (i',j') lie in the same
diagonal, if either i+j = i'+j' or i-j = i'-j'. This
condition is easy to check. Namely, if the evaluation of the path
\{
<Add sI sJ> :: sN1, <Add sI1 sJ1> :: sN2, sN1 : sN2;
<Sub sI sJ> :: sN1, <Sub sI1 sJ1> :: sN2, sN1 : sN2;
}
succeeds, the squares (i,j) and (i',j') lie in the same
diagonal.
Now we need a way to represent a board containing queens in the first m
columns.
It is obvious that we may confine our attention to the positions in which each column
contains no more than one queen, because two queens lying in the same column would hold each
other in check, thereby preventing the position from being a solution. On the other hand, the
number of the queens to be placed is equal to the number of columns, implying that each column
must contain exactly one queen. Hence, a position can be represented by a sequence of integers
I1 J2 ... In
where the number
Ik represents the queen lying in column k and
row Ik.
The solution will be constructed incrementally, by filling the columns one by one. Each time,
a queen is placed in a column, it must be checked that no queen puts the new queen in check.
Suppose the board contains k queens lying in the columns 1,
2, ..., k. This partially constructed position can be
represented by the sequence of integers
I1 I2 ... Ik
where the number Im
represents the queen lying in column m and row
Im.
Now we can define the predicate UnderAttack, which returns an empty
expression if the square (i,j) is attacked by the queens placed on the board,
or a failure, if the square is not attacked.
$func? UnderAttack sI sJ ePos = ;
UnderAttack sI sJ ePos =
ePos : $r eRest e, eRest : e sJ1,
<Length eRest> :: sI1,
\{
sI1 : sI;
sJ1 : sJ;
<Add sI sJ> :: sN1, <Add sI1 sJ1> :: sN2, sN1 : sN2;
<Sub sI sJ> :: sN1, <Sub sI1 sJ1> :: sN2, sN1 : sN2;
};
It should be noted that the test i1=i could have been removed,
since our program calls the function UnderAttack in such a way that the
parameter i is guaranteed to be greater than the column numbers of the queens
placed on the board.
Now we can define the function NextQueen making an attempt to add a new
queen to a partially constructed position. NextQueen tries to place the new
queen in different rows. If the queen can be placed, but this queen is not the last, an
attempt is made to place the next queen, etc. If the current queen cannot be placed, the
program "backtracks": i.e. tries to change the position of the previous queen.
$func? NextQueen sI sN ePos = ePos;
NextQueen sI sN ePos =
1 $iter \{ <Lt (sJ) (sN)> = <Add sJ 1>; }
:: sJ,
# <UnderAttack sI sJ ePos>,
ePos sJ :: ePos,
\? {
sI : sN
\! ePos;
\! <NextQueen <Add sI 1> sN ePos>;
};
There are some subtle points in the definition of the function NextQueen
deserving special attention.
First, the search construct tries to evaluate its rest, sequentially binding the variable
j to the values 1, 2, ...,
n, and incrementing j by 1 after each
failure to evaluate the rest of the construct.
Second, the evaluation of the rest of the search construct may fail for two reasons: either
the square (i,j) is attacked by the queens already placed on the board, in
which case the evaluation of the call to the function UnderAttack succeeds,
and, therefore, the negation of this call fails, or, despite the fact that the current queen
can be placed on the square (i,j), the following queens cannot be placed on
the board, and, therefore, the recursive call to the function NextQueen
fails.
Finally, we can define the function Solution, which takes the size of the
board as argument and returns either a solution to the problem, or, if there is no solution, a
failure:
$func? Solution sN = ePos;
Solution sN =
<NextQueen 1 sN >;