1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 | 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 |