this repo has no description
dekker.one
1% RUNS ON mzn20_fd
2% RUNS ON mzn-fzn_fd
3% RUNS ON mzn20_mip
4
5% Another regression test for the problem described in var_self_assign_bug.mzn.
6% (This model is from http://www.hakank.org/minizinc/cardinality_atmost_partition.mzn.)
7
8% From Global Constraint Catalogue
9% http://www.emn.fr/x-info/sdemasse/gccat/Ccardinality_atmost_partition.html
10% """
11% ATMOST is the maximum number of time that values of a same partition of
12% PARTITIONS are taken by the variables of the collection VARIABLES.
13%
14% Example
15% (
16% 2, <2, 3, 7, 1, 6, 0>,
17% <
18% p-<1, 3>,
19% p-<4>,
20% p-<2, 6>
21% >
22% )
23% In this example, two variables of the collection
24% VARIABLES = <2, 3, 7, 1, 6, 0>
25% are assigned to values of the first partition, no variable is assigned to
26% a value of the second partition, and finally two variables are assigned to
27% values of the last partition. As a consequence, the
28% cardinality_atmost_partition constraint holds since its first argument
29% ATMOST is assigned to the maximum number of occurrences 2.
30
31%
32% """
33%
34% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
35% See also my MiniZinc page: http://www.hakank.org/minizinc
36
37include "globals.mzn";
38
39
40int: n = 6;
41int: m = 3;
42array[1..n] of var 0..10: variables;
43array[1..m] of var set of 1..7: partitions;
44var 0..9: nvar;
45
46output [
47 "nvar = ", show(nvar), ";\n",
48 "partitions = ", show(partitions), ";\n",
49 "variables = ", show(variables), ";\n"
50];
51
52solve satisfy;
53
54% a variant of the partition_set from globals.mzn where universe is
55% a var set of int (instead of par set of int)
56predicate partition_set2(array[int] of var set of int: S,
57 var set of int: universe) =
58 all_disjoint(S) /\ universe == array_union(i in index_set(S)) ( S[i] )
59;
60
61
62%
63% cardinality_atmost_exclude_value
64%
65% as cardinality_atmost but we exclude the "rest partition" index (m+1)
66% (as a set for generality)
67% (cf. cardinality_atmost.mzn)
68%
69predicate cardinality_atmost_exclude_value(var int: nvar, array[int] of var int: variables, array[int] of var int: values, var set of int: exclude) =
70 forall(i in index_set(values)) (
71 sum(j in index_set(variables)) (bool2int(not(values[i] in exclude) /\ values[i] = variables[j])) <= nvar
72 )
73;
74
75%
76% cardinality_atmost_partition
77%
78% ("Unassigned" values are put in the m+1'th partition, the "rest partition,
79% and we don't care how many that are assigned to the rest partition.)
80%
81predicate cardinality_atmost_partition(var int: nvar, array[int] of var int: variables, array[int] of var set of int: partitions) =
82 let {
83 int: lbv = min(index_set(variables)),
84 int: ubv = max(index_set(variables)),
85 int: lbp = min(index_set(partitions)),
86 int: ubp = max(index_set(partitions)),
87 array[lbv..ubv] of var lbp..ubp+1: selected_partition
88 }
89 in
90
91 % the partitions must be partitioned
92 partition_set2(partitions, array_union(i in lbp..ubp) (partitions[i]))
93
94 /\ % assign a partition index to each value
95 forall(i in lbv..ubv) (
96 forall(j in lbp..ubp) (
97 selected_partition[i] = j <-> variables[i] in partitions[j]
98 )
99 )
100 /\ % assure that we have atmost nvar occurrences of each partition index
101 % (except the "rest partition")
102 cardinality_atmost_exclude_value(nvar, selected_partition, selected_partition, {m+1})
103;
104
105predicate cp1d(array[int] of int: x, array[int] of var int: y) =
106 assert(index_set(x) = index_set(y),
107 "cp1d: x and y have different sizes",
108 forall(i in index_set(x)) (
109 x[i] = y[i]
110 )
111 )
112;
113
114predicate cp1d(array[int] of set of int: x, array[int] of var set of int: y) =
115 assert(index_set(x) = index_set(y),
116 "cp1d: x and y have different sizes",
117 forall(i in index_set(x)) (
118 x[i] = y[i]
119 )
120 )
121;
122
123
124constraint
125
126 cp1d([2, 3, 7, 1, 6, 0], variables)
127 /\
128 cp1d([
129 {1,3},
130 {4},
131 {2,6}], partitions)
132 /\
133 nvar = 2
134 /\
135 cardinality_atmost_partition(nvar, variables, partitions)
136;
137