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