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.
\{ <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.
I1 J2 ... Inwhere the number Ik represents the queen lying in column k and row Ik.
I1 I2 ... Ikwhere 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.
$func? Solution sN = ePos; Solution sN = <NextQueen 1 sN >;