part4.eprime

language ESSENCE' 1.0

$ Constraint solving model for M-queens problem clas taking in the board size as the parameter.
given BOARD_SIZE : int

letting RANGE be domain int(1..BOARD_SIZE)

$ General lower bound.
letting minQueens1 = BOARD_SIZE/2

$ Lower bound for number of queens where M can be expressed as 4k+1
letting minQueens2 = (BOARD_SIZE%4 = 1) * (BOARD_SIZE/2 + 1)

$ Take the maximum of the two
letting minQueens = max(minQueens1, minQueens2)

$ Want to find an M*M board of {0,1}, where 1 denotes the cell containing a queen.
find result : matrix indexed by [RANGE, RANGE] of int(0,1)

$ Want to find the smallest possible solution.
minimising sum(flatten(result))

such that

$ Use the lower bound for the number of queens.
sum(flatten(result)) >= minQueens,

$ Cut down on the symmetry on x axis.
result[1,..] >=lex result[BOARD_SIZE,..],

$ Cut down on the symmetry on y axis.
result[1,..] >=lex [result[1,BOARD_SIZE-i] | i : int(0,BOARD_SIZE-1)],

$ Cut down on the 90 degree symmetry.
result[1,..] >=lex [result[i,BOARD_SIZE] | i : int(1,BOARD_SIZE)],

$ Cut down on the 180 degree symmetry
result[1,..] >=lex [result[BOARD_SIZE,BOARD_SIZE-i] | i : int(0,BOARD_SIZE-1)],

$ Cut down on the 270 degree symmetry
result[1,..] >=lex [result[BOARD_SIZE-i,1] | i : int(0,BOARD_SIZE-1)],


$ Queens do not attack each other.
$ No more than one queen in each row.
forAll row : RANGE . sum(result[row,..]) <= 1,

$ And no more than one queen in each column.
forAll col : RANGE . sum(result[..,col]) <= 1,

forAll col : RANGE . sum(result[..,col]) <= 1,

$ Constraints for the number of queens in / diagonals.
forAll diagSum : int(2..BOARD_SIZE*2) .
	(sum row, col : RANGE . (row + col = diagSum) * result[row,col]) <=1,

$ Constraint for the number of queens in bottom \ diagonals.
forAll row : RANGE .
	(sum col : int(1..BOARD_SIZE-row+1) . result[row+col-1,col]) <= 1,

$ Constraints for the number of queens in the top \ diagonals.
forAll col : RANGE .
	(sum row : int(1..BOARD_SIZE-col+1) . result[row,row+col-1]) <= 1,


$ All fields must be under attack.
forAll row : RANGE .
	forAll col : RANGE .
		(sum(result[row,..]) + sum(result[..,col]) + (sum  row2,col2 : RANGE . (result[row2,col2] != 0) /\ (|row2 - row| = |col2 - col|))) >= 1