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 
14 #include "ortools/sat/cumulative.h"
15 
16 #include <algorithm>
17 #include <memory>
18 
19 #include "ortools/base/int_type.h"
20 #include "ortools/base/logging.h"
26 #include "ortools/sat/sat_base.h"
27 #include "ortools/sat/sat_parameters.pb.h"
28 #include "ortools/sat/sat_solver.h"
29 #include "ortools/sat/timetable.h"
31 
32 namespace operations_research {
33 namespace sat {
34 
35 std::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()) {
138  AddCumulativeOverloadChecker(demands, capacity, helper, model);
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 
153 std::function<void(Model*)> CumulativeTimeDecomposition(
154  const std::vector<IntervalVariable>& vars,
155  const std::vector<AffineExpression>& demands, AffineExpression capacity,
156  SchedulingConstraintHelper* helper) {
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(
212  IntegerLiteral::GreaterOrEqual(end_vars[t],
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 
234 std::function<void(Model*)> CumulativeUsingReservoir(
235  const std::vector<IntervalVariable>& vars,
236  const std::vector<AffineExpression>& demands, AffineExpression capacity,
237  SchedulingConstraintHelper* helper) {
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 kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1412
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
Definition: integer_expr.h:572
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
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:968
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 *)> CumulativeUsingReservoir(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition: cumulative.cc:234
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