267 lines
8.7 KiB
MiniZinc
267 lines
8.7 KiB
MiniZinc
% Copyright (c) 2016, Jacopo Mauro. All rights reserved.
|
|
% This file is licensed under the terms of the ISC License.
|
|
|
|
|
|
% Please note that you will need to set the MiniZinc standard library
|
|
% environment variable $MZN_STDLIB_PATH to share/minizinc to include
|
|
% the MiniSearch builtins
|
|
|
|
include "lex_greatereq.mzn";
|
|
include "lex_less.mzn";
|
|
|
|
int: MAX_INT = 4096;
|
|
%%%%%%%%%%%%%%%%
|
|
% Input parameters
|
|
%%%%%%%%%%%%%%%%
|
|
|
|
% components
|
|
set of int: comps;
|
|
% ports
|
|
set of int: ports;
|
|
% multiple provide port
|
|
set of int: multi_provide_ports;
|
|
|
|
% locations
|
|
set of int: locations;
|
|
% resources
|
|
set of int: resources;
|
|
|
|
% map of components with their requirements number
|
|
array[ comps, ports] of int: requirement_port_nums;
|
|
% map of components with their provided multi-ports
|
|
% -1 means infinite multi-port provider
|
|
array[ comps, multi_provide_ports] of int: provide_port_nums;
|
|
% map of components with their conflicts
|
|
array[ comps, ports] of bool: conflicts;
|
|
% map of multi-ports with their ports
|
|
array[ multi_provide_ports, ports] of bool: multi_provides;
|
|
|
|
% map of location with their costs
|
|
array[ locations ] of int: costs;
|
|
% map of locations with the resouces they provide
|
|
array[ locations, resources ] of int: resource_provisions;
|
|
% map of components with the resources they consume
|
|
array[ comps, resources ] of int: resource_consumptions;
|
|
|
|
%%%%%%%%%%%%%%%%
|
|
% variables
|
|
%%%%%%%%%%%%%%%%
|
|
% bindings number
|
|
array[ multi_provide_ports, ports, comps, comps] of var 0..MAX_INT: bindings;
|
|
% components number
|
|
array[ comps ] of var 0..MAX_INT: comps_num;
|
|
% location to number of component map
|
|
array[ locations, comps] of var 0..MAX_INT: comp_locations;
|
|
|
|
% total number of components
|
|
var 0..MAX_INT: sum_comp;
|
|
|
|
%%%%%%%%%%%%%%%%
|
|
% constraints (no location)
|
|
%%%%%%%%%%%%%%%%
|
|
|
|
% bind the total number of components
|
|
constraint sum_comp = sum( i in comps)(comps_num[i]);
|
|
|
|
% bindings 0 if the multiprovide does not provide port
|
|
constraint forall(mport in multi_provide_ports, port in ports) (
|
|
if multi_provides[mport,port]
|
|
then true
|
|
else forall(i in comps, j in comps) ( bindings[mport,port,i,j] = 0)
|
|
endif
|
|
);
|
|
|
|
% provides must be greater or equal to bindings & infinite provide port constraints
|
|
constraint forall(mport in multi_provide_ports, pcomp in comps) (
|
|
if provide_port_nums[pcomp,mport]=0
|
|
then forall(port in ports, rcomp in comps) (
|
|
bindings[mport,port,pcomp,rcomp] = 0
|
|
)
|
|
else
|
|
if (provide_port_nums[pcomp,mport] = -1)
|
|
then forall(port in ports, rcomp in comps) (
|
|
(comps_num[pcomp] = 0) -> (bindings[mport,port,pcomp,rcomp]=0))
|
|
else sum( port in ports, rcomp in comps)(
|
|
bindings[mport,port,pcomp,rcomp] ) <= comps_num[pcomp] * provide_port_nums[pcomp,mport]
|
|
endif
|
|
endif
|
|
);
|
|
|
|
% requires must be equal to bindings
|
|
% note: here is possible to require also smaller than or equal
|
|
constraint forall(port in ports, rcomp in comps) (
|
|
sum( mport in multi_provide_ports, pcomp in comps)(
|
|
bindings[mport,port,pcomp,rcomp] ) = comps_num[rcomp] * requirement_port_nums[rcomp,port]
|
|
);
|
|
|
|
|
|
% conflict constraints if component provide same port
|
|
constraint forall(port in ports, pcomp in comps) (
|
|
if (conflicts[pcomp,port] /\ exists(mport in multi_provide_ports) (
|
|
(multi_provides[mport,port]) /\ provide_port_nums[pcomp,mport] != 0))
|
|
then comps_num[pcomp] <= 1
|
|
else true
|
|
endif
|
|
);
|
|
|
|
% conflict constraints
|
|
constraint forall(port in ports, pcomp in comps, rcomp in comps) (
|
|
if (conflicts[rcomp,port] /\ exists(mport in multi_provide_ports) (
|
|
(multi_provides[mport,port]) /\ provide_port_nums[pcomp,mport] != 0))
|
|
then comps_num[pcomp] > 0 -> comps_num[rcomp] = 0
|
|
else true
|
|
endif
|
|
);
|
|
|
|
% unicity constraint
|
|
% note that we require that a component does not
|
|
% require more than one port provided by a
|
|
% multiple provide port
|
|
constraint forall(mport in multi_provide_ports, pcomp in comps, rcomp in comps) (
|
|
let
|
|
{ int: max_req = sum(port in ports) (
|
|
if multi_provides[mport,port]
|
|
then requirement_port_nums[rcomp,port]
|
|
else 0
|
|
endif
|
|
)
|
|
} in
|
|
if pcomp = rcomp
|
|
then
|
|
( comps_num[pcomp] >= max_req ->
|
|
sum(port in ports)(bindings[mport,port,pcomp,rcomp])
|
|
<= max_req * (comps_num[rcomp] - 1))
|
|
/\
|
|
( comps_num[pcomp] < max_req ->
|
|
forall (i in 1..max_req)( comps_num[pcomp] = i ->
|
|
sum(port in ports)(bindings[mport,port,pcomp,rcomp]) <= i * (i-1) ))
|
|
else
|
|
( comps_num[pcomp] >= max_req ->
|
|
sum(port in ports)(bindings[mport,port,pcomp,rcomp])
|
|
<= max_req * comps_num[rcomp] )
|
|
/\
|
|
( comps_num[pcomp] < max_req ->
|
|
forall (i in 0..max_req)( comps_num[pcomp] = i ->
|
|
sum(port in ports)(bindings[mport,port,pcomp,rcomp]) <= i * comps_num[rcomp] ) )
|
|
endif
|
|
);
|
|
|
|
%%%%%%%%%%%%%%%%
|
|
% constraints for deciding locations
|
|
%%%%%%%%%%%%%%%%
|
|
|
|
% map location used or not used
|
|
array[ locations ] of var 0..1: used_locations;
|
|
constraint forall( l in locations)(
|
|
sum(c in comps)(comp_locations[l,c]) = 0 <-> used_locations[l] = 0
|
|
);
|
|
|
|
constraint forall( c in comps) (
|
|
sum( l in locations) ( comp_locations[l,c]) = comps_num[c]
|
|
);
|
|
|
|
|
|
constraint forall( res in resources, loc in locations) (
|
|
sum( comp in comps)( comp_locations[loc,comp] * resource_consumptions[comp,res] )
|
|
<= resource_provisions[loc,res]
|
|
);
|
|
|
|
% the number of locations can not be greater than the number of components
|
|
% i.e, one component per location in the worst case
|
|
constraint sum(i in locations) (used_locations[i]) <= sum_comp;
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% symmetry constraints (wrap in a unique predicate following minizinc specs
|
|
|
|
|
|
constraint symmetry_breaking_constraint(
|
|
%if location are equal then first location has more comps than the second
|
|
%in lexicographically order (based on the cost)
|
|
forall( l1 in locations, l2 in locations)(
|
|
if l1 < l2 /\ forall ( r in resources)(resource_provisions[l1,r] = resource_provisions[l2,r] )
|
|
then
|
|
if costs[l1] > costs[l2]
|
|
then lex_greatereq(
|
|
[comp_locations[l2,c] | c in comps],
|
|
[comp_locations[l1,c] | c in comps])
|
|
/\
|
|
(used_locations[l1] = 1 -> used_locations[l2] = 1)
|
|
else
|
|
lex_greatereq(
|
|
[comp_locations[l1,c] | c in comps],
|
|
[comp_locations[l2,c] | c in comps])
|
|
/\
|
|
(used_locations[l2] = 1 -> used_locations[l1] = 1)
|
|
endif
|
|
else
|
|
true
|
|
endif
|
|
));
|
|
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% Redundant constraints
|
|
|
|
%constraint redundant_constraint(
|
|
% % Ralf constraints
|
|
% forall (rcomp in comps, port in ports)(
|
|
% if requirement_port_nums[rcomp,port]!=0
|
|
% then
|
|
% comps_num[rcomp] > 0 -> sum( mport in multi_provide_ports, pcomp in comps)(
|
|
% if provide_port_nums[pcomp,mport] != 0 /\ multi_provides[mport,port]
|
|
% then comps_num[pcomp]
|
|
% else 0
|
|
% endif ) >= requirement_port_nums[rcomp,port]
|
|
% else
|
|
% true
|
|
% endif
|
|
% ));
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% Constraints
|
|
constraint
|
|
( sum(l in locations)(comp_locations[l,1]) > 0
|
|
\/ sum(l in locations)(comp_locations[l,2]) > 0
|
|
)
|
|
/\ forall(x in locations)(comp_locations[x,3] < 2)
|
|
/\ forall(x in locations)(comp_locations[x,4] < 2)
|
|
;
|
|
|
|
int: obj_min = sum(l in locations)(if costs[l] < 0 then costs[l] else 0 endif);
|
|
int: obj_max = sum(l in locations)(if costs[l] > 0 then costs[l] else 0 endif);
|
|
var obj_min..obj_max: objective;
|
|
|
|
constraint objective = sum(l in locations)(used_locations[l] * costs[l]);
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% Solve item
|
|
|
|
array [locations] of locations: costs_asc = arg_sort(costs);
|
|
array [locations] of locations: costs_desc = reverse(costs_asc);
|
|
|
|
solve
|
|
:: seq_search([
|
|
int_search([used_locations[costs_desc[i]] | i in locations],
|
|
input_order, indomain_min, complete),
|
|
int_search([comp_locations[l, i] | l in locations, i in comps],
|
|
first_fail, indomain_max, complete),
|
|
int_search(comps_num, first_fail, indomain_max, complete),
|
|
int_search([bindings[m,p,i,j] | m in multi_provide_ports, p in ports, i,j in comps],
|
|
first_fail, indomain_max, complete)
|
|
])
|
|
minimize objective;
|
|
|
|
%------------------------------------------------------------------------------%
|
|
% Output item
|
|
|
|
output [
|
|
"bindings = array4d(\(multi_provide_ports), \(ports), \(comps), \(comps), \(bindings));\n",
|
|
"comps_num = \(comps_num);\n",
|
|
"comp_locations = array2d(\(locations), \(comps), \(comp_locations));\n",
|
|
"used_locations = \(used_locations);\n",
|
|
"objective = \(objective);\n",
|
|
"% [\(objective), \(sum(x in locations)(sum(y in comps)(comp_locations[x,y])))]\n"
|
|
];
|
|
|
|
|