this repo has no description
1% RUNS ON mzn20_fd
2% RUNS ON mzn-fzn_fd
3% RUNS ON mzn20_fd_linear
4% RUNS ON mzn20_mip
5
6% Regression test for MiniZinc bug 110.
7% mzn2fzn 1.1 was generating out of range array indicies in reified contexts,
8% when the result of the reification should have just been "false".
9
10% Peacable Army of queens in MiniZinc.
11%
12% Translation of the ESSENCE' model in the Minion Translator examples:
13% http://www.cs.st-andrews.ac.uk/~andrea/examples/peacableArmyOfQueens/peaceableArmyOfQueens.eprime
14% """
15% Place 2 equally-sized armies of queens (white and black)
16% on a chess board without attacking each other
17% Maximise the size of the armies.
18%
19% 'occurrence' representation
20% """
21
22%
23% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
24% See also my MiniZinc page: http://www.hakank.org/minizinc
25%
26% There are 18 solutions for n=5
27% For n=6: 560 solutions
28
29
30% board width
31% given n : int(1..1000)
32int: n;
33% letting N be domain int(1..n)
34set of int: N = 1..n;
35
36
37% 0: empty field, 1:white queen, 2: black queen
38array[N,N] of var 0..2: board;
39var 1..(n*n) div 2: amountOfQueens;
40
41
42solve :: int_search([board[i,j] | i,j in N], first_fail, indomain, complete) maximize amountOfQueens;
43
44constraint
45 board[1,1] = 1 % let's place a white queen in the north-west corner
46 /\
47
48 % we have the same amount of white as black queens
49 sum(row, col in N) ( bool2int(board[row,col] = 1)) = amountOfQueens
50
51 /\
52
53 sum(row, col in N) ( bool2int(board[row,col] = 2) ) = amountOfQueens
54
55 /\
56
57
58 % if we have a white queen at position row and column
59 % there is no field on the same row/column/diagonal
60 % that holds a black queen
61 forall(row,col in N) (
62 (board[row, col] = 1) ->
63 (forall(i in N) (
64 ((i != row) ->
65 (board[i,col] < 2))
66 /\
67 ((i!=col) ->
68 (board[row,i] < 2))
69 /\
70 (((row+i <= n) /\ (col+i <= n)) ->
71 (board[row+i,col+i] < 2)
72 )
73 /\
74 (((row-i > 0) /\ (col-i > 0)) ->
75 (board[row-i,col-i] < 2)
76 )
77 /\
78 (((row+i <= n) /\ (col-i > 0)) ->
79 (board[row+i,col-i] < 2)
80 )
81 /\
82 (((row-i > 0) /\ (col+i <= n)) ->
83 (board[row-i,col+i] < 2)
84 ))
85 )
86 )
87
88 /\
89
90 % if we have a black queen at position row and column
91 % there is no field on the same row/column/diagonal
92 % that holds a white queen
93
94 % original ESSENCE' comment:
95 % we cannot use != 1 since diseq is not reifiable
96 forall(row,col in N) (
97 (board[row, col] = 2) ->
98 forall(j in N) (
99 ((j != row) ->
100 ((board[j,col] < 1) \/ (board[j,col] > 1) ))
101 /\
102 ((j!=col) ->
103 ((board[row,j] < 1) \/ (board[row,j] > 1)))
104 /\
105 (((row+j <= n) /\ (col+j <= n)) ->
106 ((board[row+j,col+j] < 1) \/ (board[row+j,col+j] > 1))
107 )
108 /\
109 (((row-j > 0) /\ (col-j > 0)) ->
110 ((board[row-j,col-j] < 1) \/ (board[row-j,col-j] > 1))
111 )
112 /\
113 (((row+j <= n) /\ (col-j > 0)) ->
114 ((board[row+j,col-j] < 1) \/ (board[row+j,col-j] > 1))
115 )
116 /\
117 (((row-j > 0) /\ (col+j <= n)) ->
118 ((board[row-j,col+j] < 1) \/ (board[row-j,col+j] > 1))
119 )
120 )
121 )
122
123;
124
125%
126% data
127%
128n = 5;
129% n = 6;
130
131output [
132 "board = ", show(board), ";\n",
133 "amountOfQueens = ", show(amountOfQueens), ";\n"
134];