Download
language ESSENCE' 1.0
given n : int(1..)
letting AMOUNT_QUEENS be domain int(0..n-1)
given init : matrix indexed by [ int(1..given_queens), int(1..2) ] of AMOUNT_QUEENS
find m : matrix indexed by [AMOUNT_QUEENS, AMOUNT_QUEENS] of bool
such that
$ At most and at least one for each row and column.
forAll i : AMOUNT_QUEENS . (
sum(m[i,..])<=1 /\
sum(m[..,i])<=1 /\
or(m[i,..]) /\
or(m[..,i])
),
$ For sum diagonals, at most one
forAll i : int(0..2*n-2).
$sum([m[j,k] | j : AMOUNT_QUEENS, k : AMOUNT_QUEENS, j+k=i])<=1,
sum([m[j,k] | j : AMOUNT_QUEENS, k : int(i-j), k>=0, k<n])<=1,
$ For difference diagonals, at most one
forAll i : int(-n.. n).
$sum([m[j,k] | j : AMOUNT_QUEENS, k : AMOUNT_QUEENS, j-k=i])<=1,
sum([m[j,k] | j : AMOUNT_QUEENS, k : int(j-i), k>=0, k<n])<=1,
$ initialise
forAll i : int(1..given_queens) .
m[init[i,1],init[i,2]],
true