this repo has no description
dekker.one
1/** @group globals.scheduling
2 Requires that a set of tasks given by start times \a s, durations \a d, and
3 resource requirements \a r, never require more than a global resource bound
4 \a b at any one time.
5
6 Assumptions:
7 - forall \p i, \a d[\p i] >= 0 and \a r[\p i] >= 0
8
9 Linear version.
10*/
11
12
13predicate fzn_cumulative(array[int] of var int: s,
14 array[int] of var int: d,
15 array[int] of var int: r, var int: b) =
16 if mzn_in_redundant_constraint() /\ fMZN__IgnoreRedundantCumulative then
17 true
18 else
19 let {
20 set of int: tasks =
21 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 },
22 set of int: times = dom_array( [ s[i] | i in tasks ] )
23 } in
24 if 0==card(tasks) then /*true*/ 0==card(index_set(s)) \/ b>=0
25 elseif MZN__Cumulative_Fixed_d_r /\
26 is_fixed(d) /\ is_fixed(r) /\ is_fixed(b) then
27 fzn_cumulative_fixed_d_r(s, fix(d), fix(r), fix(b))
28 elseif nMZN__UnarySizeMax_cumul>=card(times)*card(tasks) then
29 cumulative_time_decomp(s, d, r, b, times)
30 else
31 cumulative_task_decomp(s, d, r, b)
32 endif
33 endif;
34
35%% Can be called with a given set of times:
36predicate cumulative_set_times(array[int] of var int: s,
37 array[int] of var int: d,
38 array[int] of var int: r,
39 var int: b,
40 set of int: TIMES01) =
41 assert(index_set(s) == index_set(d) /\ index_set(s) == index_set(r),
42 "cumulative: the 3 array arguments must have identical index sets",
43 assert(lb_array(d) >= 0 /\ lb_array(r) >= 0,
44 "cumulative: durations and resource usages must be non-negative",
45 let {
46 set of int: tasks =
47 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 },
48 set of int: times = dom_array( [ s[i] | i in tasks ] )
49 intersect TIMES01
50 } in
51 if false then
52 cumulative_time_decomp(s, d, r, b, times)
53 else
54 cumulative_task_decomp(s, d, r, b)
55 endif ));
56
57predicate cumulative_time_decomp(array[int] of var int: s,
58 array[int] of var int: d,
59 array[int] of var int: r,
60 var int: b,
61 set of int: TIMES01) =
62let {
63 set of int: tasks =
64 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 },
65 set of int: times =
66 { i | i in min([ lb(s[i]) | i in tasks ]) ..
67 max([ ub(s[i]) + ub(d[i]) | i in tasks ]) where i in TIMES01 }
68}
69in
70 forall( t in times ) (
71 b >= sum( i in tasks ) (
72 if is_fixed(d[i]) then
73 bool2int( s[i] in t-fix(d[i])+1..t )
74 else
75 bool2int( s[i] <= t /\ t < s[i] + d[i] )
76 endif
77 * r[i]
78 )
79 );
80
81predicate cumulative_task_decomp(array[int] of var int: s,
82 array[int] of var int: d,
83 array[int] of var int: r,
84 var int: b) =
85let {
86 set of int: tasks =
87 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }
88}
89in
90 forall( j in tasks) (
91 b-r[j] >= sum( i in tasks where i != j
92 /\ lb(s[i])<=ub(s[j]) /\ lb(s[j])<ub(s[i]+d[i]) %% -- seems slower on mspsp ???
93 ) (
94 r[i] * %% r[i] * !
95 bool2int( s[i] <= s[j] /\ s[j] < s[i]+d[i] )) )
96 ;
97
98
99%% A global cumulative with SCIP: fixed d and r
100predicate fzn_cumulative_fixed_d_r(array[int] of var int: s,
101 array[int] of int: d,
102 array[int] of int: r, int: b);