OR-Tools  8.1
cumulative_energy.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 <memory>
17 #include <utility>
18 
19 #include "ortools/base/int_type.h"
21 #include "ortools/base/logging.h"
22 #include "ortools/sat/sat_base.h"
23 
24 namespace operations_research {
25 namespace sat {
26 
27 void AddCumulativeEnergyConstraint(std::vector<AffineExpression> energies,
30  Model* model) {
31  auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
32  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
33 
35  std::move(energies), capacity, integer_trail, helper);
36  constraint->RegisterWith(watcher);
37  model->TakeOwnership(constraint);
38 }
39 
40 void AddCumulativeOverloadChecker(const std::vector<AffineExpression>& demands,
43  Model* model) {
44  auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
45  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
46 
47  std::vector<AffineExpression> energies;
48  const int num_tasks = helper->NumTasks();
49  CHECK_EQ(demands.size(), num_tasks);
50  for (int t = 0; t < num_tasks; ++t) {
51  const AffineExpression size = helper->Sizes()[t];
52  const AffineExpression demand = demands[t];
53 
54  if (demand.var == kNoIntegerVariable && size.var == kNoIntegerVariable) {
55  CHECK_GE(demand.constant, 0);
56  CHECK_GE(size.constant, 0);
57  energies.emplace_back(demand.constant * size.constant);
58  } else if (demand.var == kNoIntegerVariable) {
59  CHECK_GE(demand.constant, 0);
60  energies.push_back(size);
61  energies.back().coeff *= demand.constant;
62  energies.back().constant *= demand.constant;
63  } else if (size.var == kNoIntegerVariable) {
64  CHECK_GE(size.constant, 0);
65  energies.push_back(demand);
66  energies.back().coeff *= size.constant;
67  energies.back().constant *= size.constant;
68  } else {
69  // The case where both demand and size are variable should be rare.
70  //
71  // TODO(user): Handle when needed by creating an intermediate product
72  // variable equal to demand * size. Note that because of the affine
73  // expression, we do need some custom code for this.
74  LOG(INFO) << "Overload checker with variable demand and variable size "
75  "is currently not implemented. Skipping.";
76  return;
77  }
78  }
79 
80  CumulativeEnergyConstraint* constraint =
81  new CumulativeEnergyConstraint(energies, capacity, integer_trail, helper);
82  constraint->RegisterWith(watcher);
83  model->TakeOwnership(constraint);
84 }
85 
87  std::vector<AffineExpression> energies, AffineExpression capacity,
88  IntegerTrail* integer_trail, SchedulingConstraintHelper* helper)
89  : energies_(std::move(energies)),
90  capacity_(capacity),
91  integer_trail_(integer_trail),
92  helper_(helper),
93  theta_tree_() {
94  const int num_tasks = helper_->NumTasks();
95  CHECK_EQ(energies_.size(), num_tasks);
96  task_to_start_event_.resize(num_tasks);
97 }
98 
100  const int id = watcher->Register(this);
101  helper_->WatchAllTasks(id, watcher);
103 }
104 
106  // This only uses one time direction, but the helper might be used elsewhere.
107  // TODO(user): just keep the current direction?
108  helper_->SynchronizeAndSetTimeDirection(true);
109 
110  const IntegerValue capacity_max = integer_trail_->UpperBound(capacity_);
111  // TODO(user): force capacity_max >= 0, fail/remove optionals when 0.
112  if (capacity_max <= 0) return true;
113 
114  // Set up theta tree.
115  start_event_task_time_.clear();
116  int num_events = 0;
117  for (const auto task_time : helper_->TaskByIncreasingStartMin()) {
118  const int task = task_time.task_index;
119  if (helper_->IsAbsent(task) ||
120  integer_trail_->UpperBound(energies_[task]) == 0) {
121  task_to_start_event_[task] = -1;
122  continue;
123  }
124  start_event_task_time_.emplace_back(task_time);
125  task_to_start_event_[task] = num_events;
126  num_events++;
127  }
128  start_event_is_present_.assign(num_events, false);
129  theta_tree_.Reset(num_events);
130 
131  bool tree_has_mandatory_intervals = false;
132 
133  // Main loop: insert tasks by increasing end_max, check for overloads.
134  for (const auto task_time :
136  const int current_task = task_time.task_index;
137  const IntegerValue current_end = task_time.time;
138  if (task_to_start_event_[current_task] == -1) continue;
139 
140  // Add the current task to the tree.
141  {
142  const int current_event = task_to_start_event_[current_task];
143  const IntegerValue start_min = start_event_task_time_[current_event].time;
144  const bool is_present = helper_->IsPresent(current_task);
145  start_event_is_present_[current_event] = is_present;
146  if (is_present) {
147  tree_has_mandatory_intervals = true;
148  theta_tree_.AddOrUpdateEvent(
149  current_event, start_min * capacity_max,
150  integer_trail_->LowerBound(energies_[current_task]),
151  integer_trail_->UpperBound(energies_[current_task]));
152  } else {
153  theta_tree_.AddOrUpdateOptionalEvent(
154  current_event, start_min * capacity_max,
155  integer_trail_->UpperBound(energies_[current_task]));
156  }
157  }
158 
159  if (tree_has_mandatory_intervals) {
160  // Find the critical interval.
161  const IntegerValue envelope = theta_tree_.GetEnvelope();
162  const int critical_event =
163  theta_tree_.GetMaxEventWithEnvelopeGreaterThan(envelope - 1);
164  const IntegerValue window_start =
165  start_event_task_time_[critical_event].time;
166  const IntegerValue window_end = current_end;
167  const IntegerValue window_size = window_end - window_start;
168  if (window_size == 0) continue;
169  const IntegerValue new_capacity_min =
170  CeilRatio(envelope - window_start * capacity_max, window_size);
171 
172  // Push the new capacity min, note that this can fail if it go above the
173  // maximum capacity.
174  //
175  // TODO(user): We do not need the capacity max in the reason, but by using
176  // a lower one, we could maybe have propagated more the minimum capacity.
177  // investigate.
178  if (new_capacity_min > integer_trail_->LowerBound(capacity_)) {
179  helper_->ClearReason();
180  for (int event = critical_event; event < num_events; event++) {
181  if (start_event_is_present_[event]) {
182  const int task = start_event_task_time_[event].task_index;
183  helper_->AddPresenceReason(task);
184  if (energies_[task].var != kNoIntegerVariable) {
185  helper_->MutableIntegerReason()->push_back(
186  integer_trail_->LowerBoundAsLiteral(energies_[task].var));
187  }
188  helper_->AddStartMinReason(task, window_start);
189  helper_->AddEndMaxReason(task, window_end);
190  }
191  }
192  if (capacity_.var == kNoIntegerVariable) {
193  return helper_->ReportConflict();
194  } else {
195  if (!helper_->PushIntegerLiteral(
196  capacity_.GreaterOrEqual(new_capacity_min))) {
197  return false;
198  }
199  }
200  }
201  }
202 
203  // Reduce energy of all tasks whose max energy would exceed an interval
204  // ending at current_end.
205  while (theta_tree_.GetOptionalEnvelope() > current_end * capacity_max) {
206  // Some task's max energy is too high, reduce its maximal energy.
207  // Explain with tasks present in the critical interval.
208  // If it is optional, it might get excluded, in that case,
209  // remove it from the tree.
210  // TODO(user): This could be done lazily.
211  // TODO(user): the same required task can have its energy pruned
212  // several times, making this algorithm O(n^2 log n). Is there a way
213  // to get the best pruning in one go? This looks like edge-finding not
214  // being able to converge in one pass, so it might not be easy.
215  helper_->ClearReason();
216  int critical_event;
217  int event_with_new_energy_max;
218  IntegerValue new_energy_max;
220  current_end * capacity_max, &critical_event,
221  &event_with_new_energy_max, &new_energy_max);
222 
223  const IntegerValue window_start =
224  start_event_task_time_[critical_event].time;
225 
226  // TODO(user): Improve window_end using envelope of critical event.
227  const IntegerValue window_end = current_end;
228  for (int event = critical_event; event < num_events; event++) {
229  if (start_event_is_present_[event]) {
230  if (event == event_with_new_energy_max) continue;
231  const int task = start_event_task_time_[event].task_index;
232  helper_->AddPresenceReason(task);
233  helper_->AddStartMinReason(task, window_start);
234  helper_->AddEndMaxReason(task, window_end);
235  if (energies_[task].var != kNoIntegerVariable) {
236  helper_->MutableIntegerReason()->push_back(
237  integer_trail_->LowerBoundAsLiteral(energies_[task].var));
238  }
239  }
240  }
241  if (capacity_.var != kNoIntegerVariable) {
242  helper_->MutableIntegerReason()->push_back(
243  integer_trail_->UpperBoundAsLiteral(capacity_.var));
244  }
245 
246  const int task_with_new_energy_max =
247  start_event_task_time_[event_with_new_energy_max].task_index;
248  helper_->AddStartMinReason(task_with_new_energy_max, window_start);
249  helper_->AddEndMaxReason(task_with_new_energy_max, window_end);
250 
251  if (new_energy_max <
252  integer_trail_->LowerBound(energies_[task_with_new_energy_max])) {
253  if (helper_->IsOptional(task_with_new_energy_max)) {
254  return helper_->PushTaskAbsence(task_with_new_energy_max);
255  } else {
256  return helper_->ReportConflict();
257  }
258  } else {
259  const IntegerLiteral deduction =
260  energies_[task_with_new_energy_max].LowerOrEqual(new_energy_max);
261  if (!helper_->PushIntegerLiteralIfTaskPresent(task_with_new_energy_max,
262  deduction)) {
263  return false;
264  }
265  }
266 
267  if (helper_->IsPresent(task_with_new_energy_max)) {
268  theta_tree_.AddOrUpdateEvent(
269  task_to_start_event_[task_with_new_energy_max],
270  start_event_task_time_[event_with_new_energy_max].time *
271  capacity_max,
272  integer_trail_->LowerBound(energies_[task_with_new_energy_max]),
273  new_energy_max);
274  } else {
275  theta_tree_.RemoveEvent(event_with_new_energy_max);
276  }
277  }
278  }
279  return true;
280 }
281 
282 } // namespace sat
283 } // namespace operations_research
var
IntVar * var
Definition: expr_array.cc:1858
INFO
const int INFO
Definition: log_severity.h:31
operations_research::sat::AffineExpression::constant
IntegerValue constant
Definition: integer.h:242
operations_research::sat::GenericLiteralWatcher::Register
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1910
cumulative_energy.h
operations_research::sat::AffineExpression
Definition: integer.h:205
operations_research::sat::IntegerTrail
Definition: integer.h:533
operations_research::sat::kNoIntegerVariable
const IntegerVariable kNoIntegerVariable(-1)
operations_research::sat::AddCumulativeOverloadChecker
void AddCumulativeOverloadChecker(const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper, Model *model)
Definition: cumulative_energy.cc:40
LOG
#define LOG(severity)
Definition: base/logging.h:420
operations_research::sat::CeilRatio
IntegerValue CeilRatio(IntegerValue dividend, IntegerValue positive_divisor)
Definition: integer.h:81
operations_research::sat::SchedulingConstraintHelper::WatchAllTasks
void WatchAllTasks(int id, GenericLiteralWatcher *watcher, bool watch_start_max=true, bool watch_end_max=true) const
Definition: intervals.cc:471
CHECK_GE
#define CHECK_GE(val1, val2)
Definition: base/logging.h:701
operations_research::sat::ThetaLambdaTree::AddOrUpdateOptionalEvent
void AddOrUpdateOptionalEvent(int event, IntegerType initial_envelope_opt, IntegerType energy_max)
Definition: theta_tree.cc:124
start_min
Rev< int64 > start_min
Definition: sched_constraints.cc:241
logging.h
operations_research::sat::SchedulingConstraintHelper::IsOptional
bool IsOptional(int t) const
Definition: intervals.h:449
operations_research::sat::SchedulingConstraintHelper::TaskByDecreasingEndMax
const std::vector< TaskTime > & TaskByDecreasingEndMax()
Definition: intervals.cc:302
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::CumulativeEnergyConstraint::CumulativeEnergyConstraint
CumulativeEnergyConstraint(std::vector< AffineExpression > energies, AffineExpression capacity, IntegerTrail *integer_trail, SchedulingConstraintHelper *helper)
Definition: cumulative_energy.cc:86
operations_research::sat::SchedulingConstraintHelper::AddStartMinReason
void AddStartMinReason(int t, IntegerValue lower_bound)
Definition: intervals.h:504
operations_research::sat::CumulativeEnergyConstraint
Definition: cumulative_energy.h:50
sat_base.h
operations_research::sat::SchedulingConstraintHelper::TaskByIncreasingStartMin
const std::vector< TaskTime > & TaskByIncreasingStartMin()
Definition: intervals.cc:265
operations_research::sat::GenericLiteralWatcher
Definition: integer.h:1091
demand
int64 demand
Definition: resource.cc:123
operations_research::sat::AddCumulativeEnergyConstraint
void AddCumulativeEnergyConstraint(std::vector< AffineExpression > energies, AffineExpression capacity, SchedulingConstraintHelper *helper, Model *model)
Definition: cumulative_energy.cc:27
operations_research::sat::IntegerTrail::UpperBoundAsLiteral
IntegerLiteral UpperBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1318
operations_research::sat::SchedulingConstraintHelper::MutableIntegerReason
std::vector< IntegerLiteral > * MutableIntegerReason()
Definition: intervals.h:296
operations_research::sat::SchedulingConstraintHelper::ClearReason
void ClearReason()
Definition: intervals.h:463
operations_research::sat::SchedulingConstraintHelper::ReportConflict
ABSL_MUST_USE_RESULT bool ReportConflict()
Definition: intervals.cc:466
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
operations_research::sat::ThetaLambdaTree::RemoveEvent
void RemoveEvent(int event)
Definition: theta_tree.cc:147
operations_research::sat::GenericLiteralWatcher::NotifyThatPropagatorMayNotReachFixedPointInOnePass
void NotifyThatPropagatorMayNotReachFixedPointInOnePass(int id)
Definition: integer.cc:1940
operations_research::sat::ThetaLambdaTree::AddOrUpdateEvent
void AddOrUpdateEvent(int event, IntegerType initial_envelope, IntegerType energy_min, IntegerType energy_max)
Definition: theta_tree.cc:111
CHECK_EQ
#define CHECK_EQ(val1, val2)
Definition: base/logging.h:697
operations_research::sat::ThetaLambdaTree::GetMaxEventWithEnvelopeGreaterThan
int GetMaxEventWithEnvelopeGreaterThan(IntegerType target_envelope) const
Definition: theta_tree.cc:179
operations_research::sat::SchedulingConstraintHelper::IsAbsent
bool IsAbsent(int t) const
Definition: intervals.h:458
operations_research::sat::Model
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
operations_research::sat::SchedulingConstraintHelper::NumTasks
int NumTasks() const
Definition: intervals.h:202
operations_research::sat::IntegerTrail::LowerBoundAsLiteral
IntegerLiteral LowerBoundAsLiteral(IntegerVariable i) const
Definition: integer.h:1313
operations_research::sat::AffineExpression::GreaterOrEqual
IntegerLiteral GreaterOrEqual(IntegerValue bound) const
Definition: integer.h:1268
operations_research::sat::IntegerLiteral
Definition: integer.h:153
operations_research::sat::SchedulingConstraintHelper::SynchronizeAndSetTimeDirection
void SynchronizeAndSetTimeDirection(bool is_forward)
Definition: intervals.cc:234
operations_research::sat::CumulativeEnergyConstraint::RegisterWith
void RegisterWith(GenericLiteralWatcher *watcher)
Definition: cumulative_energy.cc:99
operations_research::sat::CumulativeEnergyConstraint::Propagate
bool Propagate() final
Definition: cumulative_energy.cc:105
model
GRBmodel * model
Definition: gurobi_interface.cc:269
operations_research::sat::ThetaLambdaTree::GetEnvelope
IntegerType GetEnvelope() const
Definition: theta_tree.cc:168
gtl::reversed_view
ReverseView< Container > reversed_view(const Container &c)
Definition: iterator_adaptors.h:33
iterator_adaptors.h
operations_research::sat::ThetaLambdaTree::GetOptionalEnvelope
IntegerType GetOptionalEnvelope() const
Definition: theta_tree.cc:173
operations_research::sat::SchedulingConstraintHelper::IsPresent
bool IsPresent(int t) const
Definition: intervals.h:453
operations_research::sat::ThetaLambdaTree::Reset
void Reset(int num_events)
Definition: theta_tree.cc:40
operations_research::sat::SchedulingConstraintHelper::Sizes
const std::vector< AffineExpression > & Sizes() const
Definition: intervals.h:321
operations_research::sat::AffineExpression::var
IntegerVariable var
Definition: integer.h:240
capacity
int64 capacity
Definition: routing_flow.cc:129
operations_research::sat::SchedulingConstraintHelper::PushTaskAbsence
ABSL_MUST_USE_RESULT bool PushTaskAbsence(int t)
Definition: intervals.cc:434
operations_research::sat::IntegerTrail::LowerBound
IntegerValue LowerBound(IntegerVariable i) const
Definition: integer.h:1283
operations_research::sat::ThetaLambdaTree::GetEventsWithOptionalEnvelopeGreaterThan
void GetEventsWithOptionalEnvelopeGreaterThan(IntegerType target_envelope, int *critical_event, int *optional_event, IntegerType *available_energy) const
Definition: theta_tree.cc:189
operations_research::sat::SchedulingConstraintHelper::AddEndMaxReason
void AddEndMaxReason(int t, IntegerValue upper_bound)
Definition: intervals.h:557
time
int64 time
Definition: resource.cc:1683
operations_research::sat::SchedulingConstraintHelper::AddPresenceReason
void AddPresenceReason(int t)
Definition: intervals.h:472
operations_research::sat::SchedulingConstraintHelper::PushIntegerLiteral
ABSL_MUST_USE_RESULT bool PushIntegerLiteral(IntegerLiteral lit)
Definition: intervals.cc:378
operations_research::sat::SchedulingConstraintHelper::PushIntegerLiteralIfTaskPresent
ABSL_MUST_USE_RESULT bool PushIntegerLiteralIfTaskPresent(int t, IntegerLiteral lit)
Definition: intervals.cc:383