OR-Tools  8.2
sat/diffn.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/diffn.h"
15
16#include <algorithm>
17
18#include "absl/container/flat_hash_map.h"
19#include "absl/strings/str_join.h"
28#include "ortools/util/sort.h"
29
30namespace operations_research {
31namespace sat {
32
33namespace {
34
35// TODO(user): Use the faster variable only version if all expressions reduce
36// to a single variable?
37void AddIsEqualToMinOf(IntegerVariable min_var,
38 const std::vector<AffineExpression>& exprs,
39 Model* model) {
40 std::vector<LinearExpression> converted;
41 for (const AffineExpression& affine : exprs) {
42 LinearExpression e;
43 e.offset = affine.constant;
44 if (affine.var != kNoIntegerVariable) {
45 e.vars.push_back(affine.var);
46 e.coeffs.push_back(affine.coeff);
47 }
48 converted.push_back(e);
49 }
50 LinearExpression target;
51 target.vars.push_back(min_var);
52 target.coeffs.push_back(IntegerValue(1));
53 model->Add(IsEqualToMinOf(target, converted));
54}
55
56void AddIsEqualToMaxOf(IntegerVariable max_var,
57 const std::vector<AffineExpression>& exprs,
58 Model* model) {
59 std::vector<LinearExpression> converted;
60 for (const AffineExpression& affine : exprs) {
61 LinearExpression e;
62 e.offset = affine.constant;
63 if (affine.var != kNoIntegerVariable) {
64 e.vars.push_back(affine.var);
65 e.coeffs.push_back(affine.coeff);
66 }
67 converted.push_back(NegationOf(e));
68 }
69 LinearExpression target;
70 target.vars.push_back(NegationOf(max_var));
71 target.coeffs.push_back(IntegerValue(1));
72 model->Add(IsEqualToMinOf(target, converted));
73}
74
75} // namespace
76
77void AddCumulativeRelaxation(const std::vector<IntervalVariable>& x_intervals,
80 int64 min_starts = kint64max;
81 int64 max_ends = kint64min;
82 std::vector<AffineExpression> sizes;
83 for (int box = 0; box < y->NumTasks(); ++box) {
84 min_starts = std::min(min_starts, y->StartMin(box).value());
85 max_ends = std::max(max_ends, y->EndMax(box).value());
86 sizes.push_back(y->Sizes()[box]);
87 }
88
89 const IntegerVariable min_start_var =
90 model->Add(NewIntegerVariable(min_starts, max_ends));
91 AddIsEqualToMinOf(min_start_var, y->Starts(), model);
92
93 const IntegerVariable max_end_var =
94 model->Add(NewIntegerVariable(min_starts, max_ends));
95 AddIsEqualToMaxOf(max_end_var, y->Ends(), model);
96
97 // (max_end - min_start) >= capacity.
99 model->Add(NewIntegerVariable(0, CapSub(max_ends, min_starts))));
100 const std::vector<int64> coeffs = {-capacity.coeff.value(), -1, 1};
101 model->Add(
102 WeightedSumGreaterOrEqual({capacity.var, min_start_var, max_end_var},
103 coeffs, capacity.constant.value()));
104
105 model->Add(Cumulative(x_intervals, sizes, capacity, x));
106}
107
108namespace {
109
110// We want for different propagation to reuse as much as possible the same
111// line. The idea behind this is to compute the 'canonical' line to use
112// when explaining that boxes overlap on the 'y_dim' dimension. We compute
113// the multiple of the biggest power of two that is common to all boxes.
114IntegerValue FindCanonicalValue(IntegerValue lb, IntegerValue ub) {
115 if (lb == ub) return lb;
116 if (lb <= 0 && ub > 0) return IntegerValue(0);
117 if (lb < 0 && ub <= 0) {
118 return -FindCanonicalValue(-ub, -lb);
119 }
120
121 int64 mask = 0;
122 IntegerValue candidate = ub;
123 for (int o = 0; o < 62; ++o) {
124 mask = 2 * mask + 1;
125 const IntegerValue masked_ub(ub.value() & ~mask);
126 if (masked_ub >= lb) {
127 candidate = masked_ub;
128 } else {
129 break;
130 }
131 }
132 return candidate;
133}
134
135void SplitDisjointBoxes(const SchedulingConstraintHelper& x,
136 absl::Span<int> boxes,
137 std::vector<absl::Span<int>>* result) {
138 result->clear();
139 std::sort(boxes.begin(), boxes.end(),
140 [&x](int a, int b) { return x.StartMin(a) < x.StartMin(b); });
141 int current_start = 0;
142 std::size_t current_length = 1;
143 IntegerValue current_max_end = x.EndMax(boxes[0]);
144
145 for (int b = 1; b < boxes.size(); ++b) {
146 const int box = boxes[b];
147 if (x.StartMin(box) < current_max_end) {
148 // Merge.
149 current_length++;
150 current_max_end = std::max(current_max_end, x.EndMax(box));
151 } else {
152 if (current_length > 1) { // Ignore lists of size 1.
153 result->emplace_back(&boxes[current_start], current_length);
154 }
155 current_start = b;
156 current_length = 1;
157 current_max_end = x.EndMax(box);
158 }
159 }
160
161 // Push last span.
162 if (current_length > 1) {
163 result->emplace_back(&boxes[current_start], current_length);
164 }
165}
166
167} // namespace
168
169#define RETURN_IF_FALSE(f) \
170 if (!(f)) return false;
171
174
176 const int num_boxes = x_.NumTasks();
179
180 active_boxes_.clear();
181 cached_areas_.resize(num_boxes);
182 cached_dimensions_.resize(num_boxes);
183 for (int box = 0; box < num_boxes; ++box) {
184 cached_areas_[box] = x_.SizeMin(box) * y_.SizeMin(box);
185 if (cached_areas_[box] == 0) continue;
186
187 // TODO(user): Also consider shifted end max.
188 Dimension& dimension = cached_dimensions_[box];
189 dimension.x_min = x_.ShiftedStartMin(box);
190 dimension.x_max = x_.EndMax(box);
191 dimension.y_min = y_.ShiftedStartMin(box);
192 dimension.y_max = y_.EndMax(box);
193
194 active_boxes_.push_back(box);
195 }
196 if (active_boxes_.size() <= 1) return true;
197
198 SplitDisjointBoxes(x_, absl::MakeSpan(active_boxes_), &x_split_);
199 for (absl::Span<int> x_boxes : x_split_) {
200 SplitDisjointBoxes(y_, x_boxes, &y_split_);
201 for (absl::Span<int> y_boxes : y_split_) {
202 IntegerValue total_sum_of_areas(0);
203 for (const int box : y_boxes) {
204 total_sum_of_areas += cached_areas_[box];
205 }
206 for (const int box : y_boxes) {
208 FailWhenEnergyIsTooLarge(box, y_boxes, total_sum_of_areas));
209 }
210 }
211 }
212
213 return true;
214}
215
217 GenericLiteralWatcher* watcher) {
218 const int id = watcher->Register(this);
219 x_.WatchAllTasks(id, watcher, /*watch_start_max=*/false,
220 /*watch_end_max=*/true);
221 y_.WatchAllTasks(id, watcher, /*watch_start_max=*/false,
222 /*watch_end_max=*/true);
223 return id;
224}
225
226void NonOverlappingRectanglesEnergyPropagator::SortBoxesIntoNeighbors(
227 int box, absl::Span<const int> local_boxes,
228 IntegerValue total_sum_of_areas) {
229 const Dimension& box_dim = cached_dimensions_[box];
230
231 neighbors_.clear();
232 for (const int other_box : local_boxes) {
233 if (other_box == box) continue;
234 const Dimension& other_dim = cached_dimensions_[other_box];
235 const IntegerValue span_x = std::max(box_dim.x_max, other_dim.x_max) -
236 std::min(box_dim.x_min, other_dim.x_min);
237 const IntegerValue span_y = std::max(box_dim.y_max, other_dim.y_max) -
238 std::min(box_dim.y_min, other_dim.y_min);
239 const IntegerValue bounding_area = span_x * span_y;
240 if (bounding_area < total_sum_of_areas) {
241 neighbors_.push_back({other_box, bounding_area});
242 }
243 }
244 std::sort(neighbors_.begin(), neighbors_.end());
245}
246
247bool NonOverlappingRectanglesEnergyPropagator::FailWhenEnergyIsTooLarge(
248 int box, absl::Span<const int> local_boxes,
249 IntegerValue total_sum_of_areas) {
250 SortBoxesIntoNeighbors(box, local_boxes, total_sum_of_areas);
251
252 Dimension area = cached_dimensions_[box];
253 IntegerValue sum_of_areas = cached_areas_[box];
254
255 const auto add_box_energy_in_rectangle_reason = [&](int b) {
256 x_.AddEnergyAfterReason(b, x_.SizeMin(b), area.x_min);
257 x_.AddEndMaxReason(b, area.x_max);
258 y_.AddEnergyAfterReason(b, y_.SizeMin(b), area.y_min);
259 y_.AddEndMaxReason(b, area.y_max);
260 };
261
262 for (int i = 0; i < neighbors_.size(); ++i) {
263 const int other_box = neighbors_[i].box;
264 CHECK_GT(cached_areas_[other_box], 0);
265
266 // Update Bounding box.
267 area.TakeUnionWith(cached_dimensions_[other_box]);
268
269 // Update sum of areas.
270 sum_of_areas += cached_areas_[other_box];
271 const IntegerValue bounding_area =
272 (area.x_max - area.x_min) * (area.y_max - area.y_min);
273 if (bounding_area >= total_sum_of_areas) {
274 // Nothing will be deduced. Exiting.
275 return true;
276 }
277
278 if (sum_of_areas > bounding_area) {
279 x_.ClearReason();
280 y_.ClearReason();
281 add_box_energy_in_rectangle_reason(box);
282 for (int j = 0; j <= i; ++j) {
283 add_box_energy_in_rectangle_reason(neighbors_[j].box);
284 }
285 x_.ImportOtherReasons(y_);
286 return x_.ReportConflict();
287 }
288 }
289 return true;
290}
291
292// Note that x_ and y_ must be initialized with enough intervals when passed
293// to the disjunctive propagators.
298 Model* model)
299 : global_x_(*x),
300 global_y_(*y),
301 x_(x->NumTasks(), model),
302 y_(y->NumTasks(), model),
303 strict_(strict),
304 watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
305 overload_checker_(&x_),
306 forward_detectable_precedences_(true, &x_),
307 backward_detectable_precedences_(false, &x_),
308 forward_not_last_(true, &x_),
309 backward_not_last_(false, &x_),
310 forward_edge_finding_(true, &x_),
311 backward_edge_finding_(false, &x_) {}
312
315
317 int fast_priority, int slow_priority) {
318 fast_id_ = watcher_->Register(this);
319 watcher_->SetPropagatorPriority(fast_id_, fast_priority);
320 global_x_.WatchAllTasks(fast_id_, watcher_);
321 global_y_.WatchAllTasks(fast_id_, watcher_);
322
323 const int slow_id = watcher_->Register(this);
324 watcher_->SetPropagatorPriority(slow_id, slow_priority);
325 global_x_.WatchAllTasks(slow_id, watcher_);
326 global_y_.WatchAllTasks(slow_id, watcher_);
327}
328
329bool NonOverlappingRectanglesDisjunctivePropagator::
330 FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
333 std::function<bool()> inner_propagate) {
334 // Compute relevant events (line in the y dimension).
335 active_boxes_.clear();
336 events_time_.clear();
337 for (int box = 0; box < x.NumTasks(); ++box) {
338 if (!strict_ && (x.SizeMin(box) == 0 || y.SizeMin(box) == 0)) {
339 continue;
340 }
341
342 const IntegerValue start_max = y.StartMax(box);
343 const IntegerValue end_min = y.EndMin(box);
344 if (start_max < end_min) {
345 events_time_.push_back(start_max);
346 active_boxes_.push_back(box);
347 }
348 }
349
350 // Less than 2 boxes, no propagation.
351 if (active_boxes_.size() < 2) return true;
352
353 // Add boxes to the event lists they always overlap with.
354 gtl::STLSortAndRemoveDuplicates(&events_time_);
355 events_overlapping_boxes_.resize(events_time_.size());
356 for (int i = 0; i < events_time_.size(); ++i) {
357 events_overlapping_boxes_[i].clear();
358 }
359 for (const int box : active_boxes_) {
360 const IntegerValue start_max = y.StartMax(box);
361 const IntegerValue end_min = y.EndMin(box);
362
363 for (int i = 0; i < events_time_.size(); ++i) {
364 const IntegerValue t = events_time_[i];
365 if (t < start_max) continue;
366 if (t >= end_min) break;
367 events_overlapping_boxes_[i].push_back(box);
368 }
369 }
370
371 // Scan events chronologically to remove events where there is only one
372 // mandatory box, or dominated events lists.
373 //
374 // Optimization: We do not resize the events_overlapping_boxes_ vector so that
375 // we do not free/realloc the memory of the inner vector from one propagate to
376 // the next. This save a bit more than 1%.
377 int new_size = 0;
378 {
379 for (std::vector<int>& overlapping_boxes : events_overlapping_boxes_) {
380 if (overlapping_boxes.size() < 2) {
381 continue; // Remove current event.
382 }
383 if (new_size > 0) {
384 const std::vector<int>& previous_overlapping_boxes =
385 events_overlapping_boxes_[new_size - 1];
386
387 // If the previous set of boxes is included in the current one, replace
388 // the old one by the new one.
389 //
390 // Note that because the events correspond to new boxes, there is no
391 // need to check for the other side (current set included in previous
392 // set).
393 if (std::includes(overlapping_boxes.begin(), overlapping_boxes.end(),
394 previous_overlapping_boxes.begin(),
395 previous_overlapping_boxes.end())) {
396 --new_size;
397 }
398 }
399
400 std::swap(events_overlapping_boxes_[new_size], overlapping_boxes);
401 ++new_size;
402 }
403 }
404
405 // Split lists of boxes into disjoint set of boxes (w.r.t. overlap).
406 boxes_to_propagate_.clear();
407 reduced_overlapping_boxes_.clear();
408 for (int i = 0; i < new_size; ++i) {
409 SplitDisjointBoxes(x, absl::MakeSpan(events_overlapping_boxes_[i]),
410 &disjoint_boxes_);
411 for (absl::Span<int> sub_boxes : disjoint_boxes_) {
412 // Boxes are sorted in a stable manner in the Split method.
413 // Note that we do not use reduced_overlapping_boxes_ directly so that
414 // the order of iteration is deterministic.
415 const auto& insertion = reduced_overlapping_boxes_.insert(sub_boxes);
416 if (insertion.second) boxes_to_propagate_.push_back(sub_boxes);
417 }
418 }
419
420 // And finally propagate.
421 // TODO(user): Sorting of boxes seems influential on the performance. Test.
422 for (const absl::Span<const int> boxes : boxes_to_propagate_) {
423 x_.ResetFromSubset(x, boxes);
424 y_.ResetFromSubset(y, boxes);
425
426 // Collect the common overlapping coordinates of all boxes.
427 IntegerValue lb(kint64min);
428 IntegerValue ub(kint64max);
429 for (int i = 0; i < y_.NumTasks(); ++i) {
430 lb = std::max(lb, y_.StartMax(i));
431 ub = std::min(ub, y_.EndMin(i) - 1);
432 }
433 CHECK_LE(lb, ub);
434
435 // TODO(user): We should scan the integer trail to find the oldest
436 // non-empty common interval. Then we can pick the canonical value within
437 // it.
438
439 // We want for different propagation to reuse as much as possible the same
440 // line. The idea behind this is to compute the 'canonical' line to use
441 // when explaining that boxes overlap on the 'y_dim' dimension. We compute
442 // the multiple of the biggest power of two that is common to all boxes.
443 const IntegerValue line_to_use_for_reason = FindCanonicalValue(lb, ub);
444
445 // Setup x_dim for propagation.
446 x_.SetOtherHelper(&y_, line_to_use_for_reason);
447
448 RETURN_IF_FALSE(inner_propagate());
449 }
450
451 return true;
452}
453
455 global_x_.SynchronizeAndSetTimeDirection(true);
456 global_y_.SynchronizeAndSetTimeDirection(true);
457
458 std::function<bool()> inner_propagate;
459 if (watcher_->GetCurrentId() == fast_id_) {
460 inner_propagate = [this]() {
461 if (x_.NumTasks() == 2) {
462 // In that case, we can use simpler algorithms.
463 // Note that this case happens frequently (~30% of all calls to this
464 // method according to our tests).
465 RETURN_IF_FALSE(PropagateTwoBoxes());
466 } else {
467 RETURN_IF_FALSE(overload_checker_.Propagate());
468 RETURN_IF_FALSE(forward_detectable_precedences_.Propagate());
469 RETURN_IF_FALSE(backward_detectable_precedences_.Propagate());
470 }
471 return true;
472 };
473 } else {
474 inner_propagate = [this]() {
475 if (x_.NumTasks() <= 2) return true;
476 RETURN_IF_FALSE(forward_not_last_.Propagate());
477 RETURN_IF_FALSE(backward_not_last_.Propagate());
478 RETURN_IF_FALSE(backward_edge_finding_.Propagate());
479 RETURN_IF_FALSE(forward_edge_finding_.Propagate());
480 return true;
481 };
482 }
483
484 RETURN_IF_FALSE(FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
485 global_x_, global_y_, inner_propagate));
486
487 // We can actually swap dimensions to propagate vertically.
488 RETURN_IF_FALSE(FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
489 global_y_, global_x_, inner_propagate));
490
491 return true;
492}
493
494// Specialized propagation on only two boxes that must intersect with the
495// given y_line_for_reason.
496bool NonOverlappingRectanglesDisjunctivePropagator::PropagateTwoBoxes() {
497 // For each direction and each order, we test if the boxes can be disjoint.
498 const int state =
499 (x_.EndMin(0) <= x_.StartMax(1)) + 2 * (x_.EndMin(1) <= x_.StartMax(0));
500
501 const auto left_box_before_right_box = [this](int left, int right) {
502 // left box pushes right box.
503 const IntegerValue left_end_min = x_.EndMin(left);
504 if (left_end_min > x_.StartMin(right)) {
505 x_.ClearReason();
506 x_.AddReasonForBeingBefore(left, right);
507 x_.AddEndMinReason(left, left_end_min);
508 RETURN_IF_FALSE(x_.IncreaseStartMin(right, left_end_min));
509 }
510
511 // right box pushes left box.
512 const IntegerValue right_start_max = x_.StartMax(right);
513 if (right_start_max < x_.EndMax(left)) {
514 x_.ClearReason();
515 x_.AddReasonForBeingBefore(left, right);
516 x_.AddStartMaxReason(right, right_start_max);
517 RETURN_IF_FALSE(x_.DecreaseEndMax(left, right_start_max));
518 }
519
520 return true;
521 };
522
523 switch (state) {
524 case 0: { // Conflict.
525 x_.ClearReason();
528 return x_.ReportConflict();
529 }
530 case 1: { // b1 is left of b2.
531 return left_box_before_right_box(0, 1);
532 }
533 case 2: { // b2 is left of b1.
534 return left_box_before_right_box(1, 0);
535 }
536 default: { // Nothing to deduce.
537 return true;
538 }
539 }
540}
541
542#undef RETURN_IF_FALSE
543} // namespace sat
544} // namespace operations_research
int64 min
Definition: alldiff_cst.cc:138
int64 max
Definition: alldiff_cst.cc:139
#define CHECK_GT(val1, val2)
Definition: base/logging.h:702
#define CHECK_LE(val1, val2)
Definition: base/logging.h:699
void SetPropagatorPriority(int id, int priority)
Definition: integer.cc:1962
int Register(PropagatorInterface *propagator)
Definition: integer.cc:1939
Class that owns everything related to a particular optimization model.
Definition: sat/model.h:38
NonOverlappingRectanglesDisjunctivePropagator(bool strict, SchedulingConstraintHelper *x, SchedulingConstraintHelper *y, Model *model)
Definition: sat/diffn.cc:295
const std::vector< AffineExpression > & Starts() const
Definition: intervals.h:319
void WatchAllTasks(int id, GenericLiteralWatcher *watcher, bool watch_start_max=true, bool watch_end_max=true) const
Definition: intervals.cc:460
void ResetFromSubset(const SchedulingConstraintHelper &other, absl::Span< const int > tasks)
Definition: intervals.cc:176
void AddEnergyAfterReason(int t, IntegerValue energy_min, IntegerValue time)
Definition: intervals.h:566
void AddEndMinReason(int t, IntegerValue lower_bound)
Definition: intervals.h:535
ABSL_MUST_USE_RESULT bool IncreaseStartMin(int t, IntegerValue new_start_min)
Definition: intervals.cc:405
const std::vector< AffineExpression > & Sizes() const
Definition: intervals.h:321
void ImportOtherReasons(const SchedulingConstraintHelper &other_helper)
Definition: intervals.cc:492
ABSL_MUST_USE_RESULT bool DecreaseEndMax(int t, IntegerValue new_start_max)
Definition: intervals.cc:414
void AddEndMaxReason(int t, IntegerValue upper_bound)
Definition: intervals.h:557
void SetOtherHelper(SchedulingConstraintHelper *other_helper, IntegerValue event)
Definition: intervals.h:338
void AddReasonForBeingBefore(int before, int after)
Definition: intervals.cc:334
void AddStartMaxReason(int t, IntegerValue upper_bound)
Definition: intervals.h:513
const std::vector< AffineExpression > & Ends() const
Definition: intervals.h:320
GRBmodel * model
static const int64 kint64max
int64_t int64
static const int64 kint64min
void STLSortAndRemoveDuplicates(T *v, const LessFunc &less_func)
Definition: stl_util.h:58
const IntegerVariable kNoIntegerVariable(-1)
std::function< void(Model *)> WeightedSumGreaterOrEqual(const std::vector< IntegerVariable > &vars, const VectorInt &coefficients, int64 lower_bound)
Definition: integer_expr.h:404
std::function< void(Model *)> Cumulative(const std::vector< IntervalVariable > &vars, const std::vector< AffineExpression > &demands, AffineExpression capacity, SchedulingConstraintHelper *helper)
Definition: cumulative.cc:35
std::function< void(Model *)> IsEqualToMinOf(IntegerVariable min_var, const std::vector< IntegerVariable > &vars)
Definition: integer_expr.h:672
std::function< IntegerVariable(Model *)> NewIntegerVariable(int64 lb, int64 ub)
Definition: integer.h:1426
std::vector< IntegerVariable > NegationOf(const std::vector< IntegerVariable > &vars)
Definition: integer.cc:27
void AddCumulativeRelaxation(const std::vector< IntervalVariable > &x_intervals, SchedulingConstraintHelper *x, SchedulingConstraintHelper *y, Model *model)
Definition: sat/diffn.cc:77
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
int64 CapSub(int64 x, int64 y)
int64 capacity
#define RETURN_IF_FALSE(f)
Definition: sat/diffn.cc:169
Rev< int64 > end_min
Rev< int64 > start_max