94b2b13d
 Pedro Roque
PHACT source
|
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
include "lex_lesseq.mzn";
%------------------------------------------------------------------------------%
% Parameters
int: n; % size
%------------------------------------------------------------------------------%
% Variables
array[1..n,1..n] of var bool: filled;
array[1..n,1..n] of var 0..1: f =
array2d(1..n,1..n,[bool2int(filled[i,j]) | i,j in 1..n]);
array[1..n] of var 0..n: q;
var 0..n: objective;
%------------------------------------------------------------------------------%
% Predicates for symmetry breaking
predicate rot_sqr_sym(array[int,int] of var int: x) =
let {
int: n = card(index_set_1of2(x)),
int: n2 = card(index_set_2of2(x)),
int: l = n * n,
array[1..l] of var int: y = [x[i,j] | i in index_set_1of2(x),
j in index_set_2of2(x) ],
array[1..4,1..l] of 1..l: p = array2d(1..4,1..l,
[ if k == 1 then i*n + j - n else
if k == 2 then (n - j)*n + i else
if k == 3 then (n - i)*n + (n - j)+1 else
i*n + (n - j) - n + 1 endif endif endif
| k in 1..4, i,j in 1..n ])
} in assert(n == n2, "rot_sqr_sym: rotation symmetry applied to" ++
" non square matrix",
var_perm_sym(y,p));
predicate var_perm_sym(array[int] of var int: x, array[int,int] of int: p) =
let { int: l = min(index_set_1of2(p)),
int: u = max(index_set_1of2(p)),
array[1..length(x)] of var int: y = [ x[i] | i in index_set(x)] } in
forall (i in l..u, j in l..u where i != j) (
var_perm_sym_pairwise(y, %% forces index 1..length(x)
[ p[i,k] | k in index_set_2of2(p)],
[ p[j,k] | k in index_set_2of2(p)]) );
predicate var_perm_sym_pairwise(array[int] of var int: x,
array[int] of int: p1, array[int] of int: p2) =
let { array[1..length(x)] of 1..length(x): invp1 =
[ j | i,j in 1..length(x) where p1[j] = i ] } in
lex_lesseq(x, [ x[p2[invp1[i]]] | i in 1..length(x) ]);
%------------------------------------------------------------------------------%
% Constraints
constraint forall(i, j in 1..n)(
filled[i,j] = not (
exists(j1 in 1..n where j1 != j)(filled[i,j1])
\/ exists(i1 in 1..n where i1 != i)(filled[i1,j])
\/ exists(k in 1..n-1)(
filled[i+k,j+k] \/ filled[i-k,j+k]
\/ filled[i+k,j-k] \/ filled[i-k,j-k]
)
)
);
constraint forall(i in 1..n)(
q[i] = sum(j in 1..n)(j * f[i,j])
);
constraint objective = sum(i in 1..n)(bool2int(q[i] > 0));
constraint rot_sqr_sym(f);
%------------------------------------------------------------------------------%
% Search
solve
:: int_search([f[i, j] | i, j in 1..n], input_order, indomain_min, complete)
minimize objective;
%------------------------------------------------------------------------------%
% Output
output [
"q = ", show(q), ";\n",
"objective = ", show(objective), ";\n"
]
|