A set of benchmarks to compare a new prototype MiniZinc implementation
dekker.one
1% Copyright (c) 2016, Jacopo Mauro. All rights reserved.
2% This file is licensed under the terms of the ISC License.
3
4
5% Please note that you will need to set the MiniZinc standard library
6% environment variable $MZN_STDLIB_PATH to share/minizinc to include
7% the MiniSearch builtins
8
9include "lex_greatereq.mzn";
10include "lex_less.mzn";
11
12int: MAX_INT = 4096;
13%%%%%%%%%%%%%%%%
14% Input parameters
15%%%%%%%%%%%%%%%%
16
17% components
18set of int: comps;
19% ports
20set of int: ports;
21% multiple provide port
22set of int: multi_provide_ports;
23
24% locations
25set of int: locations;
26% resources
27set of int: resources;
28
29% map of components with their requirements number
30array[ comps, ports] of int: requirement_port_nums;
31% map of components with their provided multi-ports
32% -1 means infinite multi-port provider
33array[ comps, multi_provide_ports] of int: provide_port_nums;
34% map of components with their conflicts
35array[ comps, ports] of bool: conflicts;
36% map of multi-ports with their ports
37array[ multi_provide_ports, ports] of bool: multi_provides;
38
39% map of location with their costs
40array[ locations ] of int: costs;
41% map of locations with the resouces they provide
42array[ locations, resources ] of int: resource_provisions;
43% map of components with the resources they consume
44array[ comps, resources ] of int: resource_consumptions;
45
46%%%%%%%%%%%%%%%%
47% variables
48%%%%%%%%%%%%%%%%
49% bindings number
50array[ multi_provide_ports, ports, comps, comps] of var 0..MAX_INT: bindings;
51% components number
52array[ comps ] of var 0..MAX_INT: comps_num;
53% location to number of component map
54array[ locations, comps] of var 0..MAX_INT: comp_locations;
55
56% total number of components
57var 0..MAX_INT: sum_comp;
58
59%%%%%%%%%%%%%%%%
60% constraints (no location)
61%%%%%%%%%%%%%%%%
62
63% bind the total number of components
64constraint sum_comp = sum( i in comps)(comps_num[i]);
65
66% bindings 0 if the multiprovide does not provide port
67constraint forall(mport in multi_provide_ports, port in ports) (
68 if multi_provides[mport,port]
69 then true
70 else forall(i in comps, j in comps) ( bindings[mport,port,i,j] = 0)
71 endif
72);
73
74% provides must be greater or equal to bindings & infinite provide port constraints
75constraint forall(mport in multi_provide_ports, pcomp in comps) (
76 if provide_port_nums[pcomp,mport]=0
77 then forall(port in ports, rcomp in comps) (
78 bindings[mport,port,pcomp,rcomp] = 0
79 )
80 else
81 if (provide_port_nums[pcomp,mport] = -1)
82 then forall(port in ports, rcomp in comps) (
83 (comps_num[pcomp] = 0) -> (bindings[mport,port,pcomp,rcomp]=0))
84 else sum( port in ports, rcomp in comps)(
85 bindings[mport,port,pcomp,rcomp] ) <= comps_num[pcomp] * provide_port_nums[pcomp,mport]
86 endif
87 endif
88);
89
90% requires must be equal to bindings
91% note: here is possible to require also smaller than or equal
92constraint forall(port in ports, rcomp in comps) (
93 sum( mport in multi_provide_ports, pcomp in comps)(
94 bindings[mport,port,pcomp,rcomp] ) = comps_num[rcomp] * requirement_port_nums[rcomp,port]
95);
96
97
98% conflict constraints if component provide same port
99constraint forall(port in ports, pcomp in comps) (
100 if (conflicts[pcomp,port] /\ exists(mport in multi_provide_ports) (
101 (multi_provides[mport,port]) /\ provide_port_nums[pcomp,mport] != 0))
102 then comps_num[pcomp] <= 1
103 else true
104 endif
105);
106
107% conflict constraints
108constraint forall(port in ports, pcomp in comps, rcomp in comps) (
109 if (conflicts[rcomp,port] /\ exists(mport in multi_provide_ports) (
110 (multi_provides[mport,port]) /\ provide_port_nums[pcomp,mport] != 0))
111 then comps_num[pcomp] > 0 -> comps_num[rcomp] = 0
112 else true
113 endif
114);
115
116% unicity constraint
117% note that we require that a component does not
118% require more than one port provided by a
119% multiple provide port
120constraint forall(mport in multi_provide_ports, pcomp in comps, rcomp in comps) (
121 let
122 { int: max_req = sum(port in ports) (
123 if multi_provides[mport,port]
124 then requirement_port_nums[rcomp,port]
125 else 0
126 endif
127 )
128 } in
129 if pcomp = rcomp
130 then
131 ( comps_num[pcomp] >= max_req ->
132 sum(port in ports)(bindings[mport,port,pcomp,rcomp])
133 <= max_req * (comps_num[rcomp] - 1))
134 /\
135 ( comps_num[pcomp] < max_req ->
136 forall (i in 1..max_req)( comps_num[pcomp] = i ->
137 sum(port in ports)(bindings[mport,port,pcomp,rcomp]) <= i * (i-1) ))
138 else
139 ( comps_num[pcomp] >= max_req ->
140 sum(port in ports)(bindings[mport,port,pcomp,rcomp])
141 <= max_req * comps_num[rcomp] )
142 /\
143 ( comps_num[pcomp] < max_req ->
144 forall (i in 0..max_req)( comps_num[pcomp] = i ->
145 sum(port in ports)(bindings[mport,port,pcomp,rcomp]) <= i * comps_num[rcomp] ) )
146 endif
147);
148
149%%%%%%%%%%%%%%%%
150% constraints for deciding locations
151%%%%%%%%%%%%%%%%
152
153% map location used or not used
154array[ locations ] of var 0..1: used_locations;
155constraint forall( l in locations)(
156 sum(c in comps)(comp_locations[l,c]) = 0 <-> used_locations[l] = 0
157);
158
159constraint forall( c in comps) (
160 sum( l in locations) ( comp_locations[l,c]) = comps_num[c]
161);
162
163
164constraint forall( res in resources, loc in locations) (
165 sum( comp in comps)( comp_locations[loc,comp] * resource_consumptions[comp,res] )
166 <= resource_provisions[loc,res]
167);
168
169% the number of locations can not be greater than the number of components
170% i.e, one component per location in the worst case
171constraint sum(i in locations) (used_locations[i]) <= sum_comp;
172
173%------------------------------------------------------------------------------%
174% symmetry constraints (wrap in a unique predicate following minizinc specs
175
176
177constraint symmetry_breaking_constraint(
178 %if location are equal then first location has more comps than the second
179 %in lexicographically order (based on the cost)
180 forall( l1 in locations, l2 in locations)(
181 if l1 < l2 /\ forall ( r in resources)(resource_provisions[l1,r] = resource_provisions[l2,r] )
182 then
183 if costs[l1] > costs[l2]
184 then lex_greatereq(
185 [comp_locations[l2,c] | c in comps],
186 [comp_locations[l1,c] | c in comps])
187 /\
188 (used_locations[l1] = 1 -> used_locations[l2] = 1)
189 else
190 lex_greatereq(
191 [comp_locations[l1,c] | c in comps],
192 [comp_locations[l2,c] | c in comps])
193 /\
194 (used_locations[l2] = 1 -> used_locations[l1] = 1)
195 endif
196 else
197 true
198 endif
199 ));
200
201
202%------------------------------------------------------------------------------%
203% Redundant constraints
204
205%constraint redundant_constraint(
206% % Ralf constraints
207% forall (rcomp in comps, port in ports)(
208% if requirement_port_nums[rcomp,port]!=0
209% then
210% comps_num[rcomp] > 0 -> sum( mport in multi_provide_ports, pcomp in comps)(
211% if provide_port_nums[pcomp,mport] != 0 /\ multi_provides[mport,port]
212% then comps_num[pcomp]
213% else 0
214% endif ) >= requirement_port_nums[rcomp,port]
215% else
216% true
217% endif
218% ));
219
220%------------------------------------------------------------------------------%
221% Constraints
222constraint
223 ( sum(l in locations)(comp_locations[l,1]) > 0
224 \/ sum(l in locations)(comp_locations[l,2]) > 0
225 )
226/\ forall(x in locations)(comp_locations[x,3] < 2)
227/\ forall(x in locations)(comp_locations[x,4] < 2)
228;
229
230int: obj_min = sum(l in locations)(if costs[l] < 0 then costs[l] else 0 endif);
231int: obj_max = sum(l in locations)(if costs[l] > 0 then costs[l] else 0 endif);
232var obj_min..obj_max: objective;
233
234constraint objective = sum(l in locations)(used_locations[l] * costs[l]);
235
236%------------------------------------------------------------------------------%
237% Solve item
238
239array [locations] of locations: costs_asc = arg_sort(costs);
240array [locations] of locations: costs_desc = reverse(costs_asc);
241
242solve
243 :: seq_search([
244 int_search([used_locations[costs_desc[i]] | i in locations],
245 input_order, indomain_min, complete),
246 int_search([comp_locations[l, i] | l in locations, i in comps],
247 first_fail, indomain_max, complete),
248 int_search(comps_num, first_fail, indomain_max, complete),
249 int_search([bindings[m,p,i,j] | m in multi_provide_ports, p in ports, i,j in comps],
250 first_fail, indomain_max, complete)
251 ])
252 minimize objective;
253
254%------------------------------------------------------------------------------%
255% Output item
256
257output [
258 "bindings = array4d(\(multi_provide_ports), \(ports), \(comps), \(comps), \(bindings));\n",
259 "comps_num = \(comps_num);\n",
260 "comp_locations = array2d(\(locations), \(comps), \(comp_locations));\n",
261 "used_locations = \(used_locations);\n",
262 "objective = \(objective);\n",
263 "% [\(objective), \(sum(x in locations)(sum(y in comps)(comp_locations[x,y])))]\n"
264];
265
266