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