Loading [Contrib]/a11y/accessibility-menu.js
Download
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