Download
language ESSENCE' 1.0
given      n : int(1..)
letting    AMOUNT_QUEENS be domain int(0..n-1)
given      blocks : matrix indexed by [ int(1..blocked_squares), int(1..2) ] of int(1..n)


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..blocked_squares) .
    !m[blocks[i,1]-1,blocks[i,2]-1],

true