OR-Tools  8.2
cumulative.cc
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
15
16#include <algorithm>
17#include <memory>
18
27#include "ortools/sat/sat_parameters.pb.h"
31
32namespace operations_research {
33namespace sat {
34
35std::function<void(Model*)> Cumulative(
36 const std::vector<IntervalVariable>& vars,
37 const std::vector<AffineExpression>& demands, AffineExpression capacity,
39 return [=](Model* model) mutable {
40 if (vars.empty()) return;
41
42 auto* intervals = model->GetOrCreate<IntervalsRepository>();
43 auto* encoder = model->GetOrCreate<IntegerEncoder>();
44 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
45 auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
46
47 // Redundant constraints to ensure that the resource capacity is high enough
48 // for each task. Also ensure that no task consumes more resource than what
49 // is available. This is useful because the subsequent propagators do not
50 // filter the capacity variable very well.
51 for (int i = 0; i < demands.size(); ++i) {
52 if (intervals->MaxSize(vars[i]) == 0) continue;
53
54 LinearConstraintBuilder builder(model, kMinIntegerValue, IntegerValue(0));
55 builder.AddTerm(demands[i], IntegerValue(1));
56 builder.AddTerm(capacity, IntegerValue(-1));
57 LinearConstraint ct = builder.Build();
58
59 std::vector<Literal> enforcement_literals;
60 if (intervals->IsOptional(vars[i])) {
61 enforcement_literals.push_back(intervals->PresenceLiteral(vars[i]));
62 }
63
64 // If the interval can be of size zero, it currently do not count towards
65 // the capacity. TODO(user): Change that since we have optional interval
66 // for this.
67 if (intervals->MinSize(vars[i]) == 0) {
68 enforcement_literals.push_back(encoder->GetOrCreateAssociatedLiteral(
69 intervals->Size(vars[i]).GreaterOrEqual(IntegerValue(1))));
70 }
71
72 if (enforcement_literals.empty()) {
74 } else {
75 LoadConditionalLinearConstraint(enforcement_literals, ct, model);
76 }
77 }
78
79 if (vars.size() == 1) return;
80
81 const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
82
83 // Detect a subset of intervals that needs to be in disjunction and add a
84 // Disjunctive() constraint over them.
85 if (parameters.use_disjunctive_constraint_in_cumulative_constraint()) {
86 // TODO(user): We need to exclude intervals that can be of size zero
87 // because the disjunctive do not "ignore" them like the cumulative
88 // does. That is, the interval [2,2) will be assumed to be in
89 // disjunction with [1, 3) for instance. We need to uniformize the
90 // handling of interval with size zero.
91 //
92 // TODO(user): improve the condition (see CL147454185).
93 std::vector<IntervalVariable> in_disjunction;
94 for (int i = 0; i < vars.size(); ++i) {
95 if (intervals->MinSize(vars[i]) > 0 &&
96 2 * integer_trail->LowerBound(demands[i]) >
97 integer_trail->UpperBound(capacity)) {
98 in_disjunction.push_back(vars[i]);
99 }
100 }
101
102 // Add a disjunctive constraint on the intervals in in_disjunction. Do not
103 // create the cumulative at all when all intervals must be in disjunction.
104 //
105 // TODO(user): Do proper experiments to see how beneficial this is, the
106 // disjunctive will propagate more but is also using slower algorithms.
107 // That said, this is more a question of optimizing the disjunctive
108 // propagation code.
109 //
110 // TODO(user): Another "known" idea is to detect pair of tasks that must
111 // be in disjunction and to create a Boolean to indicate which one is
112 // before the other. It shouldn't change the propagation, but may result
113 // in a faster one with smaller explanations, and the solver can also take
114 // decision on such Boolean.
115 //
116 // TODO(user): A better place for stuff like this could be in the
117 // presolver so that it is easier to disable and play with alternatives.
118 if (in_disjunction.size() > 1) model->Add(Disjunctive(in_disjunction));
119 if (in_disjunction.size() == vars.size()) return;
120 }
121
122 if (helper == nullptr) {
123 helper = new SchedulingConstraintHelper(vars, model);
124 model->TakeOwnership(helper);
125 }
126
127 // Propagator responsible for applying Timetabling filtering rule. It
128 // increases the minimum of the start variables, decrease the maximum of the
129 // end variables, and increase the minimum of the capacity variable.
130 TimeTablingPerTask* time_tabling =
131 new TimeTablingPerTask(demands, capacity, integer_trail, helper);
132 time_tabling->RegisterWith(watcher);
133 model->TakeOwnership(time_tabling);
134
135 // Propagator responsible for applying the Overload Checking filtering rule.
136 // It increases the minimum of the capacity variable.
137 if (parameters.use_overload_checker_in_cumulative_constraint()) {
139 }
140
141 // Propagator responsible for applying the Timetable Edge finding filtering
142 // rule. It increases the minimum of the start variables and decreases the
143 // maximum of the end variables,
144 if (parameters.use_timetable_edge_finding_in_cumulative_constraint()) {
145 TimeTableEdgeFinding* time_table_edge_finding =
146 new TimeTableEdgeFinding(demands, capacity, helper, integer_trail);
147 time_table_edge_finding->RegisterWith(watcher);
148 model->TakeOwnership(time_table_edge_finding);
149 }
150 };
151}
152
153std::function<void(Model*)> CumulativeTimeDecomposition(
154 const std::vector<IntervalVariable>& vars,
155 const std::vector<AffineExpression>& demands, AffineExpression capacity,
157 return [=](Model* model) {
158 if (vars.empty()) return;
159
160 IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
161 CHECK(integer_trail->IsFixed(capacity));
162 const Coefficient fixed_capacity(
163 integer_trail->UpperBound(capacity).value());
164
165 const int num_tasks = vars.size();
166 SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
167 IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
168 IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
169
170 std::vector<IntegerVariable> start_vars;
171 std::vector<IntegerVariable> end_vars;
172 std::vector<IntegerValue> fixed_demands;
173
174 for (int t = 0; t < num_tasks; ++t) {
175 start_vars.push_back(intervals->StartVar(vars[t]));
176 end_vars.push_back(intervals->EndVar(vars[t]));
177 CHECK(integer_trail->IsFixed(demands[t]));
178 fixed_demands.push_back(integer_trail->LowerBound(demands[t]));
179 }
180
181 // Compute time range.
182 IntegerValue min_start = kMaxIntegerValue;
183 IntegerValue max_end = kMinIntegerValue;
184 for (int t = 0; t < num_tasks; ++t) {
185 min_start = std::min(min_start, integer_trail->LowerBound(start_vars[t]));
186 max_end = std::max(max_end, integer_trail->UpperBound(end_vars[t]));
187 }
188
189 for (IntegerValue time = min_start; time < max_end; ++time) {
190 std::vector<LiteralWithCoeff> literals_with_coeff;
191 for (int t = 0; t < num_tasks; ++t) {
192 sat_solver->Propagate();
193 const IntegerValue start_min = integer_trail->LowerBound(start_vars[t]);
194 const IntegerValue end_max = integer_trail->UpperBound(end_vars[t]);
195 if (end_max <= time || time < start_min || fixed_demands[t] == 0) {
196 continue;
197 }
198
199 // Task t consumes the resource at time if consume_condition is true.
200 std::vector<Literal> consume_condition;
201 const Literal consume = Literal(model->Add(NewBooleanVariable()), true);
202
203 // Task t consumes the resource at time if it is present.
204 if (intervals->IsOptional(vars[t])) {
205 consume_condition.push_back(intervals->PresenceLiteral(vars[t]));
206 }
207
208 // Task t overlaps time.
209 consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral(
210 IntegerLiteral::LowerOrEqual(start_vars[t], IntegerValue(time))));
211 consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral(
213 IntegerValue(time + 1))));
214
215 model->Add(ReifiedBoolAnd(consume_condition, consume));
216
217 // TODO(user): this is needed because we currently can't create a
218 // boolean variable if the model is unsat.
219 if (sat_solver->IsModelUnsat()) return;
220
221 literals_with_coeff.push_back(
222 LiteralWithCoeff(consume, Coefficient(fixed_demands[t].value())));
223 }
224 // The profile cannot exceed the capacity at time.
225 sat_solver->AddLinearConstraint(false, Coefficient(0), true,
226 fixed_capacity, &literals_with_coeff);
227
228 // Abort if UNSAT.
229 if (sat_solver->IsModelUnsat()) return;
230 }
231 };
232}
233
234std::function<void(Model*)> CumulativeUsingReservoir(
235 const std::vector<IntervalVariable>& vars,
236 const std::vector<AffineExpression>& demands, AffineExpression capacity,
238 return [=](Model* model) {
239 if (vars.empty()) return;
240
241 auto* integer_trail = model->GetOrCreate<IntegerTrail>();
242 auto* encoder = model->GetOrCreate<IntegerEncoder>();
243 auto* intervals = model->GetOrCreate<IntervalsRepository>();
244
245 CHECK(integer_trail->IsFixed(capacity));
246 const IntegerValue fixed_capacity(
247 integer_trail->UpperBound(capacity).value());
248
249 std::vector<AffineExpression> times;
250 std::vector<IntegerValue> deltas;
251 std::vector<Literal> presences;
252
253 const int num_tasks = vars.size();
254 for (int t = 0; t < num_tasks; ++t) {
255 CHECK(integer_trail->IsFixed(demands[t]));
256 times.push_back(intervals->StartVar(vars[t]));
257 deltas.push_back(integer_trail->LowerBound(demands[t]));
258 times.push_back(intervals->EndVar(vars[t]));
259 deltas.push_back(-integer_trail->LowerBound(demands[t]));
260 if (intervals->IsOptional(vars[t])) {
261 presences.push_back(intervals->PresenceLiteral(vars[t]));
262 presences.push_back(intervals->PresenceLiteral(vars[t]));
263 } else {
264 presences.push_back(encoder->GetTrueLiteral());
265 presences.push_back(encoder->GetTrueLiteral());
266 }
267 }
268 AddReservoirConstraint(times, deltas, presences, 0, fixed_capacity.value(),
269 model);
270 };
271}
272
273} // namespace sat
274} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK(condition)
Definition: base/logging.h:495
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1308
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1304
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1300
void AddTerm(IntegerVariable var, IntegerValue coeff)
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
bool AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)
Definition: sat_solver.cc:299
void RegisterWith(GenericLiteralWatcher *watcher)
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: timetable.cc:313
SatParameters parameters
const Constraint * ct
int64 value
GRBmodel * model
void AddCumulativeOverloadChecker(const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper, Model *model)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< void(Model *)> Cumulative(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition: cumulative.cc:35
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
void AddReservoirConstraint(std::vector< AffineExpression > times, std::vector< IntegerValue > deltas, std::vector< Literal > presences, int64 min_level, int64 max_level, Model *model)
Definition: timetable.cc:27
std::function< void(Model *)> Disjunctive(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:30
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
Definition: integer_expr.h:572
std::function< void(Model *)> CumulativeTimeDecomposition(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition: cumulative.cc:153
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:968
std::function< void(Model *)> CumulativeUsingReservoir(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition: cumulative.cc:234
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1412
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 time
Definition: resource.cc:1683
int64 capacity
Rev< int64 > end_max
Rev< int64 > start_min
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1270
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1264