$ Peaceable Army of queens
$
$ Place 2 equally-sized armies of queens (white and black)
$ on a chess board without attacking each other
$ Maximise the size of the armies.

language ESSENCE' 1.b.a



$ board width
given        n : int
letting      N be domain int(1..n)


$ 0: empty field, 1:white queen, 2: black queen
find        board : matrix indexed by [N,N] of int(0..2)
find        amountOfQueens : int(1..(n*n)/2)     


maximising   amountOfQueens


such that

   
   $ we have the same amount of white as black queens
   (sum row : N .
       (sum col : N .
          (board[row,col] = 1))) = amountOfQueens,

   (sum row : N .
       (sum col : N . 
           (board[row,col] = 2))) = amountOfQueens,


   $ if we have a white queen at position row and column
   $ there is no field on the same row/column/diagonal
   $ that holds a black queen
   forall row,col : N . 
      (board[row, col] = 1) =>
            (forall i : N .
               ((i != row) =>
                  (board[i,col] < 2))
               /\
               ((i!=col) =>
                  (board[row,i] < 2))
	       /\ 
               (((row+i <= n) /\ (col+i <= n)) =>
                (board[row+i,col+i] < 2)	  
		)  
	       /\ 
               (((row-i > 0) /\ (col-i > 0)) =>
                (board[row-i,col-i] < 2)	  
		)  
	       /\ 
               (((row+i <= n) /\ (col-i > 0)) =>
                (board[row+i,col-i] < 2)	  
		)  
	       /\ 
               (((row-i > 0) /\ (col+i <= n)) =>
                (board[row-i,col+i] < 2)	  
		)),  

   $ if we have a black queen at position row and column
   $ there is no field on the same row/column/diagonal
   $ that holds a white queen

   forall row,col : N . 
      (board[row, col] = 2) =>
            (forall j : N .
               ((j != row) =>
                  (board[j,col] !=  1) )
               /\
               ((j!=col) =>
                  (board[row,j] != 1))
	       /\ 
               (((row+j <= n) /\ (col+j <= n)) =>
                         (board[row+j,col+j] != 1))	  
		  
	       /\ 
               (((row-j > 0) /\ (col-j > 0)) =>
                   (board[row-j,col-j] != 1))	    
	       /\ 
               (((row+j <= n) /\ (col-j > 0)) =>
                   (board[row+j,col-j] != 1) )	   
		  
	       /\ 
               (((row-j > 0) /\ (col+j <= n)) =>
                     (board[row-j,col+j] != 1)) 	  
            )