OR-Tools  8.1
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"
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  IntegerLiteral::GreaterOrEqual(intervals->SizeVar(vars[i]),
70  IntegerValue(1))));
71  }
72 
73  if (enforcement_literals.empty()) {
75  } else {
76  LoadConditionalLinearConstraint(enforcement_literals, ct, model);
77  }
78  }
79 
80  if (vars.size() == 1) return;
81 
82  const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
83 
84  // Detect a subset of intervals that needs to be in disjunction and add a
85  // Disjunctive() constraint over them.
86  if (parameters.use_disjunctive_constraint_in_cumulative_constraint()) {
87  // TODO(user): We need to exclude intervals that can be of size zero
88  // because the disjunctive do not "ignore" them like the cumulative
89  // does. That is, the interval [2,2) will be assumed to be in
90  // disjunction with [1, 3) for instance. We need to uniformize the
91  // handling of interval with size zero.
92  //
93  // TODO(user): improve the condition (see CL147454185).
94  std::vector<IntervalVariable> in_disjunction;
95  for (int i = 0; i < vars.size(); ++i) {
96  if (intervals->MinSize(vars[i]) > 0 &&
97  2 * integer_trail->LowerBound(demands[i]) >
98  integer_trail->UpperBound(capacity)) {
99  in_disjunction.push_back(vars[i]);
100  }
101  }
102 
103  // Add a disjunctive constraint on the intervals in in_disjunction. Do not
104  // create the cumulative at all when all intervals must be in disjunction.
105  //
106  // TODO(user): Do proper experiments to see how beneficial this is, the
107  // disjunctive will propagate more but is also using slower algorithms.
108  // That said, this is more a question of optimizing the disjunctive
109  // propagation code.
110  //
111  // TODO(user): Another "known" idea is to detect pair of tasks that must
112  // be in disjunction and to create a Boolean to indicate which one is
113  // before the other. It shouldn't change the propagation, but may result
114  // in a faster one with smaller explanations, and the solver can also take
115  // decision on such Boolean.
116  //
117  // TODO(user): A better place for stuff like this could be in the
118  // presolver so that it is easier to disable and play with alternatives.
119  if (in_disjunction.size() > 1) model->Add(Disjunctive(in_disjunction));
120  if (in_disjunction.size() == vars.size()) return;
121  }
122 
123  if (helper == nullptr) {
124  helper = new SchedulingConstraintHelper(vars, model);
125  model->TakeOwnership(helper);
126  }
127 
128  // Propagator responsible for applying Timetabling filtering rule. It
129  // increases the minimum of the start variables, decrease the maximum of the
130  // end variables, and increase the minimum of the capacity variable.
131  TimeTablingPerTask* time_tabling =
132  new TimeTablingPerTask(demands, capacity, integer_trail, helper);
133  time_tabling->RegisterWith(watcher);
134  model->TakeOwnership(time_tabling);
135 
136  // Propagator responsible for applying the Overload Checking filtering rule.
137  // It increases the minimum of the capacity variable.
138  if (parameters.use_overload_checker_in_cumulative_constraint()) {
139  AddCumulativeOverloadChecker(demands, capacity, helper, model);
140  }
141 
142  // Propagator responsible for applying the Timetable Edge finding filtering
143  // rule. It increases the minimum of the start variables and decreases the
144  // maximum of the end variables,
145  if (parameters.use_timetable_edge_finding_in_cumulative_constraint()) {
146  TimeTableEdgeFinding* time_table_edge_finding =
147  new TimeTableEdgeFinding(demands, capacity, helper, integer_trail);
148  time_table_edge_finding->RegisterWith(watcher);
149  model->TakeOwnership(time_table_edge_finding);
150  }
151  };
152 }
153 
154 std::function<void(Model*)> CumulativeTimeDecomposition(
155  const std::vector<IntervalVariable>& vars,
156  const std::vector<AffineExpression>& demands, AffineExpression capacity,
157  SchedulingConstraintHelper* helper) {
158  return [=](Model* model) {
159  if (vars.empty()) return;
160 
161  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
162  CHECK(integer_trail->IsFixed(capacity));
163  const Coefficient fixed_capacity(
164  integer_trail->UpperBound(capacity).value());
165 
166  const int num_tasks = vars.size();
167  SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
168  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
169  IntervalsRepository* intervals = model->GetOrCreate<IntervalsRepository>();
170 
171  std::vector<IntegerVariable> start_vars;
172  std::vector<IntegerVariable> end_vars;
173  std::vector<IntegerValue> fixed_demands;
174 
175  for (int t = 0; t < num_tasks; ++t) {
176  start_vars.push_back(intervals->StartVar(vars[t]));
177  end_vars.push_back(intervals->EndVar(vars[t]));
178  CHECK(integer_trail->IsFixed(demands[t]));
179  fixed_demands.push_back(integer_trail->LowerBound(demands[t]));
180  }
181 
182  // Compute time range.
183  IntegerValue min_start = kMaxIntegerValue;
184  IntegerValue max_end = kMinIntegerValue;
185  for (int t = 0; t < num_tasks; ++t) {
186  min_start = std::min(min_start, integer_trail->LowerBound(start_vars[t]));
187  max_end = std::max(max_end, integer_trail->UpperBound(end_vars[t]));
188  }
189 
190  for (IntegerValue time = min_start; time < max_end; ++time) {
191  std::vector<LiteralWithCoeff> literals_with_coeff;
192  for (int t = 0; t < num_tasks; ++t) {
193  sat_solver->Propagate();
194  const IntegerValue start_min = integer_trail->LowerBound(start_vars[t]);
195  const IntegerValue end_max = integer_trail->UpperBound(end_vars[t]);
196  if (end_max <= time || time < start_min || fixed_demands[t] == 0) {
197  continue;
198  }
199 
200  // Task t consumes the resource at time if consume_condition is true.
201  std::vector<Literal> consume_condition;
202  const Literal consume = Literal(model->Add(NewBooleanVariable()), true);
203 
204  // Task t consumes the resource at time if it is present.
205  if (intervals->IsOptional(vars[t])) {
206  consume_condition.push_back(intervals->PresenceLiteral(vars[t]));
207  }
208 
209  // Task t overlaps time.
210  consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral(
211  IntegerLiteral::LowerOrEqual(start_vars[t], IntegerValue(time))));
212  consume_condition.push_back(encoder->GetOrCreateAssociatedLiteral(
213  IntegerLiteral::GreaterOrEqual(end_vars[t],
214  IntegerValue(time + 1))));
215 
216  model->Add(ReifiedBoolAnd(consume_condition, consume));
217 
218  // TODO(user): this is needed because we currently can't create a
219  // boolean variable if the model is unsat.
220  if (sat_solver->IsModelUnsat()) return;
221 
222  literals_with_coeff.push_back(
223  LiteralWithCoeff(consume, Coefficient(fixed_demands[t].value())));
224  }
225  // The profile cannot exceed the capacity at time.
226  sat_solver->AddLinearConstraint(false, Coefficient(0), true,
227  fixed_capacity, &literals_with_coeff);
228 
229  // Abort if UNSAT.
230  if (sat_solver->IsModelUnsat()) return;
231  }
232  };
233 }
234 
235 } // namespace sat
236 } // namespace operations_research
cumulative_energy.h
min
int64 min
Definition: alldiff_cst.cc:138
operations_research::sat::AffineExpression
Definition: integer.h:205
operations_research::sat::IntegerTrail
Definition: integer.h:533
max
int64 max
Definition: alldiff_cst.cc:139
operations_research::sat::LinearConstraintBuilder::Build
LinearConstraint Build()
Definition: linear_constraint.cc:113
operations_research::sat::AddCumulativeOverloadChecker
void AddCumulativeOverloadChecker(const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper, Model *model)
Definition: cumulative_energy.cc:40
end_max
Rev< int64 > end_max
Definition: sched_constraints.cc:244
operations_research::sat::SatSolver::AddLinearConstraint
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
linear_constraint.h
start_min
Rev< int64 > start_min
Definition: sched_constraints.cc:241
logging.h
disjunctive.h
operations_research::sat::SatSolver
Definition: sat_solver.h:58
value
int64 value
Definition: demon_profiler.cc:43
operations_research
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Definition: dense_doubly_linked_list.h:21
operations_research::sat::IntegerLiteral::GreaterOrEqual
static IntegerLiteral GreaterOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1247
sat_solver.h
sat_base.h
operations_research::sat::LinearConstraintBuilder::AddTerm
void AddTerm(IntegerVariable var, IntegerValue coeff)
Definition: linear_constraint.cc:22
pb_constraint.h
timetable.h
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
operations_research::sat::LinearConstraint
Definition: linear_constraint.h:39
operations_research::sat::NewBooleanVariable
std::function< BooleanVariable(Model *)> NewBooleanVariable()
Definition: integer.h:1395
operations_research::sat::LinearConstraintBuilder
Definition: linear_constraint.h:87
sat_parameters.pb.h
operations_research::sat::SchedulingConstraintHelper
Definition: intervals.h:172
operations_research::sat::IntegerTrail::UpperBound
IntegerValue UpperBound(IntegerVariable i) const
Definition: integer.h:1287
int_type.h
precedences.h
operations_research::sat::kMaxIntegerValue
constexpr IntegerValue kMaxIntegerValue(std::numeric_limits< IntegerValue::ValueType >::max() - 1)
operations_research::sat::Cumulative
std::function< void(Model *)> Cumulative(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition: cumulative.cc:35
operations_research::sat::TimeTableEdgeFinding::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: timetable_edgefinding.cc:47
operations_research::sat::LoadLinearConstraint
void LoadLinearConstraint(const ConstraintProto &ct, Model *m)
Definition: cp_model_loader.cc:1055
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
ct
const Constraint * ct
Definition: demon_profiler.cc:42
operations_research::sat::TimeTableEdgeFinding
Definition: timetable_edgefinding.h:61
operations_research::sat::IntegerLiteral::LowerOrEqual
static IntegerLiteral LowerOrEqual(IntegerVariable i, IntegerValue bound)
Definition: integer.h:1253
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::Literal
Definition: sat_base.h:64
operations_research::sat::SatSolver::Propagate
bool Propagate()
Definition: sat_solver.cc:1622
operations_research::sat::kMinIntegerValue
constexpr IntegerValue kMinIntegerValue(-kMaxIntegerValue)
operations_research::sat::CumulativeTimeDecomposition
std::function< void(Model *)> CumulativeTimeDecomposition(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition: cumulative.cc:154
operations_research::sat::Disjunctive
std::function< void(Model *)> Disjunctive(const std::vector< IntervalVariable > &vars)
Definition: disjunctive.cc:30
operations_research::sat::IntervalsRepository
Definition: intervals.h:45
operations_research::sat::LiteralWithCoeff
Definition: pb_constraint.h:49
operations_research::sat::IntegerTrail::IsFixed
bool IsFixed(IntegerVariable i) const
Definition: integer.h:1291
timetable_edgefinding.h
capacity
int64 capacity
Definition: routing_flow.cc:129
operations_research::sat::IntegerTrail::LowerBound
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1283
operations_research::sat::LoadConditionalLinearConstraint
void LoadConditionalLinearConstraint(const absl::Span< const Literal > enforcement_literals, const LinearConstraint &cst, Model *model)
Definition: integer_expr.h:572
operations_research::sat::ReifiedBoolAnd
std::function< void(Model *)> ReifiedBoolAnd(const std::vector< Literal > &literals, Literal r)
Definition: sat_solver.h:969
cumulative.h
CHECK
#define CHECK(condition)
Definition: base/logging.h:495
operations_research::sat::SatSolver::IsModelUnsat
bool IsModelUnsat() const
Definition: sat_solver.h:137
parameters
SatParameters parameters
Definition: cp_model_fz_solver.cc:108
operations_research::sat::IntegerEncoder
Definition: integer.h:276
operations_research::sat::TimeTablingPerTask::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: timetable.cc:61
operations_research::sat::TimeTablingPerTask
Definition: timetable.h:29
time
int64 time
Definition: resource.cc:1683