always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
5bd09c376eac20a92f97f39875fa79158f8fa3ab
ortools-clone/ortools/sat/diffn.cc

910 lines
34 KiB
C++
Raw Blame History

// Copyright 2010-2022 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
#include "ortools/sat/diffn.h"
#include <stddef.h>
#include <algorithm>
#include <cstddef>
#include <cstdint>
#include <limits>
#include <optional>
#include <string>
#include <utility>
#include <vector>
#include "absl/container/flat_hash_set.h"
#include "absl/log/check.h"
#include "absl/types/span.h"
#include "ortools/base/logging.h"
#include "ortools/sat/cumulative_energy.h"
#include "ortools/sat/diffn_util.h"
#include "ortools/sat/disjunctive.h"
#include "ortools/sat/integer.h"
#include "ortools/sat/integer_expr.h"
#include "ortools/sat/intervals.h"
#include "ortools/sat/linear_constraint.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_base.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/sat/timetable.h"
#include "ortools/util/saturated_arithmetic.h"
#include "ortools/util/strong_integers.h"
namespace operations_research {
namespace sat {
namespace {
IntegerVariable CreateVariableWithTightDomain(
absl::Span<const AffineExpression> exprs, Model* model) {
IntegerValue min = kMaxIntegerValue;
IntegerValue max = kMinIntegerValue;
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
for (const AffineExpression& e : exprs) {
min = std::min(min, integer_trail->LevelZeroLowerBound(e));
max = std::max(max, integer_trail->LevelZeroUpperBound(e));
}
return integer_trail->AddIntegerVariable(min, max);
}
// TODO(user): Use the faster variable only version if all expressions reduce
// to a single variable?
IntegerVariable CreateVariableEqualToMinOf(
absl::Span<const AffineExpression> exprs, Model* model) {
std::vector<LinearExpression> converted;
for (const AffineExpression& affine : exprs) {
LinearExpression e;
e.offset = affine.constant;
if (affine.var != kNoIntegerVariable) {
e.vars.push_back(affine.var);
e.coeffs.push_back(affine.coeff);
}
converted.push_back(e);
}
LinearExpression target;
const IntegerVariable var = CreateVariableWithTightDomain(exprs, model);
target.vars.push_back(var);
target.coeffs.push_back(IntegerValue(1));
model->Add(IsEqualToMinOf(target, converted));
return var;
}
IntegerVariable CreateVariableEqualToMaxOf(
absl::Span<const AffineExpression> exprs, Model* model) {
std::vector<LinearExpression> converted;
for (const AffineExpression& affine : exprs) {
LinearExpression e;
e.offset = affine.constant;
if (affine.var != kNoIntegerVariable) {
e.vars.push_back(affine.var);
e.coeffs.push_back(affine.coeff);
}
converted.push_back(NegationOf(e));
}
LinearExpression target;
const IntegerVariable var = CreateVariableWithTightDomain(exprs, model);
target.vars.push_back(NegationOf(var));
target.coeffs.push_back(IntegerValue(1));
model->Add(IsEqualToMinOf(target, converted));
return var;
}
// Add a cumulative relaxation. That is, on one dimension, it does not enforce
// the rectangle aspect, allowing vertical slices to move freely.
void AddDiffnCumulativeRelationOnX(SchedulingConstraintHelper* x,
SchedulingConstraintHelper* y,
Model* model) {
// TODO(user): Use conditional affine min/max !!
const IntegerVariable min_start_var =
CreateVariableEqualToMinOf(y->Starts(), model);
const IntegerVariable max_end_var =
CreateVariableEqualToMaxOf(y->Ends(), model);
// (max_end - min_start) >= capacity.
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
const AffineExpression capacity(model->Add(NewIntegerVariable(
0, CapSub(integer_trail->UpperBound(max_end_var).value(),
integer_trail->LowerBound(min_start_var).value()))));
const std::vector<int64_t> coeffs = {-capacity.coeff.value(), -1, 1};
model->Add(
WeightedSumGreaterOrEqual({capacity.var, min_start_var, max_end_var},
coeffs, capacity.constant.value()));
SchedulingDemandHelper* demands =
model->GetOrCreate<IntervalsRepository>()->GetOrCreateDemandHelper(
x, y->Sizes());
// Propagator responsible for applying Timetabling filtering rule. It
// increases the minimum of the start variables, decrease the maximum of the
// end variables, and increase the minimum of the capacity variable.
const SatParameters& params = *model->GetOrCreate<SatParameters>();
if (params.use_timetabling_in_no_overlap_2d()) {
TimeTablingPerTask* time_tabling =
new TimeTablingPerTask(capacity, x, demands, model);
time_tabling->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(time_tabling);
}
// Propagator responsible for applying the Overload Checking filtering rule.
// It increases the minimum of the capacity variable.
if (params.use_energetic_reasoning_in_no_overlap_2d()) {
AddCumulativeOverloadChecker(capacity, x, demands, model);
}
}
// This function will fill the helper why the two boxes always overlap on that
// dimension.
void ClearAndAddMandatoryOverlapReason(int box1, int box2,
SchedulingConstraintHelper* helper) {
helper->ClearReason();
helper->AddPresenceReason(box1);
helper->AddPresenceReason(box2);
helper->AddReasonForBeingBefore(box1, box2);
helper->AddReasonForBeingBefore(box2, box1);
}
bool ClearAndAddTwoBoxesConflictReason(int box1, int box2,
SchedulingConstraintHelper* x,
SchedulingConstraintHelper* y) {
ClearAndAddMandatoryOverlapReason(box1, box2, x);
ClearAndAddMandatoryOverlapReason(box1, box2, y);
x->ImportOtherReasons(*y);
return x->ReportConflict();
}
} // namespace
void AddNonOverlappingRectangles(const std::vector<IntervalVariable>& x,
const std::vector<IntervalVariable>& y,
Model* model) {
IntervalsRepository* repository = model->GetOrCreate<IntervalsRepository>();
SchedulingConstraintHelper* x_helper = repository->GetOrCreateHelper(x);
SchedulingConstraintHelper* y_helper = repository->GetOrCreateHelper(y);
NonOverlappingRectanglesDisjunctivePropagator* constraint =
new NonOverlappingRectanglesDisjunctivePropagator(x_helper, y_helper,
model);
constraint->Register(/*fast_priority=*/3, /*slow_priority=*/4);
model->TakeOwnership(constraint);
const SatParameters& params = *model->GetOrCreate<SatParameters>();
const bool add_cumulative_relaxation =
params.use_timetabling_in_no_overlap_2d() ||
params.use_energetic_reasoning_in_no_overlap_2d();
if (add_cumulative_relaxation) {
// We must first check if the cumulative relaxation is possible.
bool some_boxes_are_only_optional_on_x = false;
bool some_boxes_are_only_optional_on_y = false;
for (int i = 0; i < x.size(); ++i) {
if (x_helper->IsOptional(i) && y_helper->IsOptional(i) &&
x_helper->PresenceLiteral(i) != y_helper->PresenceLiteral(i)) {
// Abort as the task would be conditioned by two literals.
return;
}
if (x_helper->IsOptional(i) && !y_helper->IsOptional(i)) {
// We cannot use x_size as the demand of the cumulative based on
// the y_intervals.
some_boxes_are_only_optional_on_x = true;
}
if (y_helper->IsOptional(i) && !x_helper->IsOptional(i)) {
// We cannot use y_size as the demand of the cumulative based on
// the y_intervals.
some_boxes_are_only_optional_on_y = true;
}
}
if (!some_boxes_are_only_optional_on_y) {
AddDiffnCumulativeRelationOnX(x_helper, y_helper, model);
}
if (!some_boxes_are_only_optional_on_x) {
AddDiffnCumulativeRelationOnX(y_helper, x_helper, model);
}
}
if (params.use_area_energetic_reasoning_in_no_overlap_2d()) {
NonOverlappingRectanglesEnergyPropagator* energy_constraint =
new NonOverlappingRectanglesEnergyPropagator(x_helper, y_helper, model);
GenericLiteralWatcher* const watcher =
model->GetOrCreate<GenericLiteralWatcher>();
watcher->SetPropagatorPriority(energy_constraint->RegisterWith(watcher), 5);
model->TakeOwnership(energy_constraint);
}
}
#define RETURN_IF_FALSE(f) \
if (!(f)) return false;
NonOverlappingRectanglesEnergyPropagator::
~NonOverlappingRectanglesEnergyPropagator() {
if (!VLOG_IS_ON(1)) return;
std::vector<std::pair<std::string, int64_t>> stats;
stats.push_back(
{"NonOverlappingRectanglesEnergyPropagator/called", num_calls_});
stats.push_back(
{"NonOverlappingRectanglesEnergyPropagator/conflicts", num_conflicts_});
stats.push_back(
{"NonOverlappingRectanglesEnergyPropagator/multiple_conflicts",
num_multiple_conflicts_});
stats.push_back(
{"NonOverlappingRectanglesEnergyPropagator/conflicts_two_boxes",
num_conflicts_two_boxes_});
shared_stats_->AddStats(stats);
}
bool NonOverlappingRectanglesEnergyPropagator::Propagate() {
// TODO(user): double-check/revisit the algo for box of variable sizes.
const int num_boxes = x_.NumTasks();
if (!x_.SynchronizeAndSetTimeDirection(true)) return false;
if (!y_.SynchronizeAndSetTimeDirection(true)) return false;
num_calls_++;
Rectangle bounding_box = {.x_min = std::numeric_limits<IntegerValue>::max(),
.x_max = std::numeric_limits<IntegerValue>::min(),
.y_min = std::numeric_limits<IntegerValue>::max(),
.y_max = std::numeric_limits<IntegerValue>::min()};
std::vector<RectangleInRange> active_box_ranges;
active_box_ranges.reserve(num_boxes);
for (int box = 0; box < num_boxes; ++box) {
if (x_.SizeMin(box) == 0 || y_.SizeMin(box) == 0) continue;
if (!x_.IsPresent(box) || !y_.IsPresent(box)) continue;
bounding_box.x_min = std::min(bounding_box.x_min, x_.StartMin(box));
bounding_box.x_max = std::max(bounding_box.x_max, x_.EndMax(box));
bounding_box.y_min = std::min(bounding_box.y_min, y_.StartMin(box));
bounding_box.y_max = std::max(bounding_box.y_max, y_.EndMax(box));
active_box_ranges.push_back(RectangleInRange{
.box_index = box,
.bounding_area = {.x_min = x_.StartMin(box),
.x_max = x_.StartMax(box) + x_.SizeMin(box),
.y_min = y_.StartMin(box),
.y_max = y_.StartMax(box) + y_.SizeMin(box)},
.x_size = x_.SizeMin(box),
.y_size = y_.SizeMin(box)});
}
if (active_box_ranges.size() <= 2) {
return true;
}
// Our algo is quadratic, so we don't want to run it on really large problems.
if (active_box_ranges.size() > 1000) {
return true;
}
if (std::max(bounding_box.SizeX(), bounding_box.SizeY()) *
active_box_ranges.size() >
std::numeric_limits<int32_t>::max()) {
// Avoid integer overflows if the area of the boxes get comparable with
// INT64_MAX
return true;
}
const std::vector<Rectangle> rectangles_too_much_energy =
FindRectanglesWithEnergyConflictMC(active_box_ranges, *random_, 1.0);
if (rectangles_too_much_energy.empty()) return true;
num_conflicts_++;
num_multiple_conflicts_ += rectangles_too_much_energy.size() > 1;
std::optional<std::vector<RectangleInRange>> best_explanation;
for (const auto& r : rectangles_too_much_energy) {
std::vector<RectangleInRange> range_for_explanation =
GetEnergyConflictForRectangle(r, active_box_ranges);
CheckPropagationIsValid(range_for_explanation, r);
if (!best_explanation ||
best_explanation->size() > range_for_explanation.size()) {
best_explanation = range_for_explanation;
}
}
return BuildAndReportEnergyTooLarge(*best_explanation);
}
std::vector<RectangleInRange>
NonOverlappingRectanglesEnergyPropagator::GetEnergyConflictForRectangle(
const Rectangle& rectangle,
const std::vector<RectangleInRange>& active_box_ranges) {
struct OverlapPerBox {
IntegerValue energy;
IntegerValue overlap_x_size;
IntegerValue overlap_y_size;
int index;
};
// First select the minimum amount of elements that would be enough to exceed
// the energy.
std::vector<OverlapPerBox> energy_per_box(active_box_ranges.size());
for (int i = 0; i < active_box_ranges.size(); ++i) {
const Rectangle overlap =
active_box_ranges[i].GetMinimumIntersection(rectangle);
OverlapPerBox& box = energy_per_box[i];
box.overlap_x_size = overlap.SizeX();
box.overlap_y_size = overlap.SizeY();
box.index = i;
box.energy = box.overlap_x_size * box.overlap_y_size;
}
std::sort(energy_per_box.begin(), energy_per_box.end(),
[](const OverlapPerBox& a, const OverlapPerBox& b) {
return a.energy > b.energy;
});
IntegerValue available_energy = rectangle.Area();
IntegerValue used_energy = 0;
std::vector<RectangleInRange> ranges_for_explanation;
ranges_for_explanation.reserve(energy_per_box.size());
for (int i = 0; i < energy_per_box.size(); ++i) {
const OverlapPerBox& box = energy_per_box[i];
used_energy += box.energy;
ranges_for_explanation.push_back(
RectangleInRange::BiggestWithMinIntersection(
rectangle, active_box_ranges[box.index], box.overlap_x_size,
box.overlap_y_size));
if (used_energy > available_energy) {
break;
}
}
// Now use the energy slack to make the intervals even bigger.
IntegerValue slack = used_energy - available_energy - 1;
VLOG_EVERY_N_SEC(2, 3) << "Rectangle with energy overflow: " << rectangle
<< " (" << used_energy << "/" << available_energy
<< "), with " << ranges_for_explanation.size()
<< " boxes inside.";
for (auto& range : ranges_for_explanation) {
Rectangle overlap = range.GetMinimumIntersection(rectangle);
DCHECK_GT(overlap.SizeX(), 0);
DCHECK_GT(overlap.SizeY(), 0);
if (overlap.SizeX() < slack) {
IntegerValue y_slack = slack / overlap.SizeX();
// We know we can remove an area as big as y_slack * x_size. That means
// we can reduce the start of an interval of y_slack or increase the end
// by the same amount. But there is no point wasting the slack on a
// interval larger than the zero-level interval, so we check for that.
const IntegerValue y_min_slack = std::max(
IntegerValue(0),
std::min(y_slack, range.bounding_area.y_min -
y_.LevelZeroStartMin(range.box_index)));
if (y_min_slack > 0) {
range.bounding_area.y_min -= y_min_slack;
slack -= y_min_slack * overlap.SizeX();
y_slack -= y_min_slack;
}
const IntegerValue y_max_slack =
std::min(y_slack, y_.LevelZeroStartMax(range.box_index) -
range.bounding_area.y_max);
if (y_max_slack > 0) {
range.bounding_area.y_max += y_max_slack;
slack -= y_max_slack * overlap.SizeX();
}
// Recompute the overlap, since we changed the item dimensions.
overlap = range.GetMinimumIntersection(rectangle);
}
if (overlap.SizeY() < slack) {
IntegerValue x_slack = slack / overlap.SizeY();
const IntegerValue x_min_slack = std::max(
IntegerValue(0),
std::min(x_slack, range.bounding_area.x_min -
x_.LevelZeroStartMax(range.box_index)));
if (x_min_slack > 0) {
range.bounding_area.x_min -= x_min_slack;
slack -= x_min_slack * overlap.SizeY();
x_slack -= x_min_slack;
}
const IntegerValue x_max_slack =
std::min(x_slack, x_.LevelZeroStartMax(range.box_index) -
range.bounding_area.x_max);
if (x_max_slack > 0) {
range.bounding_area.x_max += x_max_slack;
slack -= x_max_slack * overlap.SizeY();
}
}
}
CHECK_GT(used_energy, available_energy);
CHECK_GT(available_energy, 0);
return ranges_for_explanation;
}
int NonOverlappingRectanglesEnergyPropagator::RegisterWith(
GenericLiteralWatcher* watcher) {
const int id = watcher->Register(this);
x_.WatchAllTasks(id, watcher, /*watch_start_max=*/true,
/*watch_end_max=*/true);
y_.WatchAllTasks(id, watcher, /*watch_start_max=*/true,
/*watch_end_max=*/true);
return id;
}
void NonOverlappingRectanglesEnergyPropagator::CheckPropagationIsValid(
const std::vector<RectangleInRange>& ranges,
const Rectangle& rectangle_too_much_energy) {
const IntegerValue available_energy = rectangle_too_much_energy.Area();
IntegerValue used_energy = 0;
for (const auto& range : ranges) {
const int b = range.box_index;
// Check that we are explaining intervals at least as large as the current.
CHECK_GE(x_.StartMin(b), range.bounding_area.x_min);
CHECK_GE(range.bounding_area.x_max - range.x_size, x_.StartMax(b));
CHECK_GE(y_.StartMin(b), range.bounding_area.y_min);
CHECK_GE(range.bounding_area.y_max - range.y_size, y_.StartMax(b));
// Each one of the boxes-in-range that we found on the cut does intersect
// the rectangle we found.
const auto intersection =
range.GetMinimumIntersection(rectangle_too_much_energy);
CHECK_GT(intersection.Area(), 0);
// It cannot intersect more than the size of the object.
CHECK_GE(x_.SizeMin(b), intersection.SizeX());
CHECK_GE(y_.SizeMin(b), intersection.SizeY());
used_energy += intersection.Area();
}
// We have more area inside the rectangle than the area of the rectangle.
CHECK_GT(used_energy, available_energy);
}
bool NonOverlappingRectanglesEnergyPropagator::BuildAndReportEnergyTooLarge(
const std::vector<RectangleInRange>& ranges) {
if (ranges.size() == 2) {
num_conflicts_two_boxes_++;
return ClearAndAddTwoBoxesConflictReason(ranges[0].box_index,
ranges[1].box_index, &x_, &y_);
}
x_.ClearReason();
y_.ClearReason();
for (const auto& range : ranges) {
const int b = range.box_index;
x_.AddStartMinReason(b, range.bounding_area.x_min);
y_.AddStartMinReason(b, range.bounding_area.y_min);
x_.AddStartMaxReason(b, range.bounding_area.x_max - range.x_size);
y_.AddStartMaxReason(b, range.bounding_area.y_max - range.y_size);
x_.AddSizeMinReason(b);
y_.AddSizeMinReason(b);
x_.AddPresenceReason(b);
y_.AddPresenceReason(b);
}
x_.ImportOtherReasons(y_);
return x_.ReportConflict();
}
namespace {
// We want for different propagation to reuse as much as possible the same
// line. The idea behind this is to compute the 'canonical' line to use
// when explaining that boxes overlap on the 'y_dim' dimension. We compute
// the multiple of the biggest power of two that is common to all boxes.
IntegerValue FindCanonicalValue(IntegerValue lb, IntegerValue ub) {
if (lb == ub) return lb;
if (lb <= 0 && ub > 0) return IntegerValue(0);
if (lb < 0 && ub <= 0) {
return -FindCanonicalValue(-ub, -lb);
}
int64_t mask = 0;
IntegerValue candidate = ub;
for (int o = 0; o < 62; ++o) {
mask = 2 * mask + 1;
const IntegerValue masked_ub(ub.value() & ~mask);
if (masked_ub >= lb) {
candidate = masked_ub;
} else {
break;
}
}
return candidate;
}
void SplitDisjointBoxes(const SchedulingConstraintHelper& x,
absl::Span<int> boxes,
std::vector<absl::Span<int>>* result) {
result->clear();
std::sort(boxes.begin(), boxes.end(), [&x](int a, int b) {
return x.ShiftedStartMin(a) < x.ShiftedStartMin(b);
});
int current_start = 0;
std::size_t current_length = 1;
IntegerValue current_max_end = x.EndMax(boxes[0]);
for (int b = 1; b < boxes.size(); ++b) {
const int box = boxes[b];
if (x.ShiftedStartMin(box) < current_max_end) {
// Merge.
current_length++;
current_max_end = std::max(current_max_end, x.EndMax(box));
} else {
if (current_length > 1) { // Ignore lists of size 1.
result->emplace_back(&boxes[current_start], current_length);
}
current_start = b;
current_length = 1;
current_max_end = x.EndMax(box);
}
}
// Push last span.
if (current_length > 1) {
result->emplace_back(&boxes[current_start], current_length);
}
}
// This function assumes that the left and right boxes overlap on the second
// dimension, and that left cannot be after right.
// It checks and pushes the lower bound of the right box and the upper bound
// of the left box if need.
//
// If y is not null, it import the mandatory reason for the overlap on y in
// the x helper.
bool LeftBoxBeforeRightBoxOnFirstDimension(int left, int right,
SchedulingConstraintHelper* x,
SchedulingConstraintHelper* y) {
// left box2 pushes right box2.
const IntegerValue left_end_min = x->EndMin(left);
if (left_end_min > x->StartMin(right)) {
x->ClearReason();
x->AddPresenceReason(left);
x->AddPresenceReason(right);
x->AddReasonForBeingBefore(left, right);
x->AddEndMinReason(left, left_end_min);
if (y != nullptr) {
// left and right must overlap on y.
ClearAndAddMandatoryOverlapReason(left, right, y);
// Propagate with the complete reason.
x->ImportOtherReasons(*y);
}
RETURN_IF_FALSE(x->IncreaseStartMin(right, left_end_min));
}
// right box2 pushes left box2.
const IntegerValue right_start_max = x->StartMax(right);
if (right_start_max < x->EndMax(left)) {
x->ClearReason();
x->AddPresenceReason(left);
x->AddPresenceReason(right);
x->AddReasonForBeingBefore(left, right);
x->AddStartMaxReason(right, right_start_max);
if (y != nullptr) {
// left and right must overlap on y.
ClearAndAddMandatoryOverlapReason(left, right, y);
// Propagate with the complete reason.
x->ImportOtherReasons(*y);
}
RETURN_IF_FALSE(x->DecreaseEndMax(left, right_start_max));
}
return true;
}
} // namespace
// Note that x_ and y_ must be initialized with enough intervals when passed
// to the disjunctive propagators.
NonOverlappingRectanglesDisjunctivePropagator::
NonOverlappingRectanglesDisjunctivePropagator(SchedulingConstraintHelper* x,
SchedulingConstraintHelper* y,
Model* model)
: global_x_(*x),
global_y_(*y),
x_(x->NumTasks(), model),
watcher_(model->GetOrCreate<GenericLiteralWatcher>()),
overload_checker_(&x_),
forward_detectable_precedences_(true, &x_),
backward_detectable_precedences_(false, &x_),
forward_not_last_(true, &x_),
backward_not_last_(false, &x_),
forward_edge_finding_(true, &x_),
backward_edge_finding_(false, &x_),
pairwise_propagation_(model->GetOrCreate<SatParameters>()
->use_pairwise_reasoning_in_no_overlap_2d()) {
// Checks the presence of potential zero area boxes.
for (int b = 0; b < global_x_.NumTasks(); ++b) {
if (global_x_.SizeMin(b) == 0 || global_y_.SizeMin(b) == 0) {
has_zero_area_boxes_ = true;
break;
}
}
}
NonOverlappingRectanglesDisjunctivePropagator::
~NonOverlappingRectanglesDisjunctivePropagator() = default;
void NonOverlappingRectanglesDisjunctivePropagator::Register(
int fast_priority, int slow_priority) {
fast_id_ = watcher_->Register(this);
watcher_->SetPropagatorPriority(fast_id_, fast_priority);
global_x_.WatchAllTasks(fast_id_, watcher_);
global_y_.WatchAllTasks(fast_id_, watcher_);
// This propagator is the one making sure our propagation is complete, so
// we do need to make sure it is called again if it modified some bounds.
watcher_->NotifyThatPropagatorMayNotReachFixedPointInOnePass(fast_id_);
const int slow_id = watcher_->Register(this);
watcher_->SetPropagatorPriority(slow_id, slow_priority);
global_x_.WatchAllTasks(slow_id, watcher_);
global_y_.WatchAllTasks(slow_id, watcher_);
}
bool NonOverlappingRectanglesDisjunctivePropagator::
FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
bool fast_propagation, const SchedulingConstraintHelper& x,
SchedulingConstraintHelper* y) {
// Note that since we only push bounds on x, we cache the value for y just
// once.
if (!y->SynchronizeAndSetTimeDirection(true)) return false;
// Compute relevant boxes, the one with a mandatory part of y. Because we will
// need to sort it this way, we consider them by increasing start max.
indexed_boxes_.clear();
const auto temp = y->TaskByDecreasingStartMax();
for (int i = temp.size(); --i >= 0;) {
const int box = temp[i].task_index;
// Ignore absent boxes.
if (x.IsAbsent(box) || y->IsAbsent(box)) continue;
// Ignore boxes where the relevant presence literal is only on the y
// dimension, or if both intervals are optionals with different literals.
if (x.IsPresent(box) && !y->IsPresent(box)) continue;
if (!x.IsPresent(box) && !y->IsPresent(box) &&
x.PresenceLiteral(box) != y->PresenceLiteral(box)) {
continue;
}
const IntegerValue start_max = temp[i].time;
const IntegerValue end_min = y->EndMin(box);
if (start_max < end_min) {
indexed_boxes_.push_back({box, start_max, end_min});
}
}
// Less than 2 boxes, no propagation.
if (indexed_boxes_.size() < 2) return true;
ConstructOverlappingSets(/*already_sorted=*/true, &indexed_boxes_,
&events_overlapping_boxes_);
// Split lists of boxes into disjoint set of boxes (w.r.t. overlap).
boxes_to_propagate_.clear();
reduced_overlapping_boxes_.clear();
for (int i = 0; i < events_overlapping_boxes_.size(); ++i) {
SplitDisjointBoxes(x, absl::MakeSpan(events_overlapping_boxes_[i]),
&disjoint_boxes_);
for (absl::Span<int> sub_boxes : disjoint_boxes_) {
// Boxes are sorted in a stable manner in the Split method.
// Note that we do not use reduced_overlapping_boxes_ directly so that
// the order of iteration is deterministic.
const auto& insertion = reduced_overlapping_boxes_.insert(sub_boxes);
if (insertion.second) boxes_to_propagate_.push_back(sub_boxes);
}
}
// And finally propagate.
//
// TODO(user): Sorting of boxes seems influential on the performance. Test.
for (const absl::Span<const int> boxes : boxes_to_propagate_) {
// The case of two boxes should be taken care of during "fast" propagation,
// so we can skip it here.
if (!fast_propagation && boxes.size() <= 2) continue;
x_.ClearOtherHelper();
if (!x_.ResetFromSubset(x, boxes)) return false;
// Collect the common overlapping coordinates of all boxes.
IntegerValue lb(std::numeric_limits<int64_t>::min());
IntegerValue ub(std::numeric_limits<int64_t>::max());
for (const int b : boxes) {
lb = std::max(lb, y->StartMax(b));
ub = std::min(ub, y->EndMin(b) - 1);
}
CHECK_LE(lb, ub);
// We want for different propagation to reuse as much as possible the same
// line. The idea behind this is to compute the 'canonical' line to use
// when explaining that boxes overlap on the 'y_dim' dimension. We compute
// the multiple of the biggest power of two that is common to all boxes.
//
// TODO(user): We should scan the integer trail to find the oldest
// non-empty common interval. Then we can pick the canonical value within
// it.
const IntegerValue line_to_use_for_reason = FindCanonicalValue(lb, ub);
// Setup x_dim for propagation.
x_.SetOtherHelper(y, boxes, line_to_use_for_reason);
if (fast_propagation) {
if (x_.NumTasks() == 2) {
// In that case, we can use simpler algorithms.
// Note that this case happens frequently (~30% of all calls to this
// method according to our tests).
RETURN_IF_FALSE(PropagateOnXWhenOnlyTwoBoxes());
} else {
RETURN_IF_FALSE(overload_checker_.Propagate());
RETURN_IF_FALSE(forward_detectable_precedences_.Propagate());
RETURN_IF_FALSE(backward_detectable_precedences_.Propagate());
}
} else {
DCHECK_GT(x_.NumTasks(), 2);
RETURN_IF_FALSE(forward_not_last_.Propagate());
RETURN_IF_FALSE(backward_not_last_.Propagate());
RETURN_IF_FALSE(backward_edge_finding_.Propagate());
RETURN_IF_FALSE(forward_edge_finding_.Propagate());
}
}
return true;
}
bool NonOverlappingRectanglesDisjunctivePropagator::Propagate() {
global_x_.SetTimeDirection(true);
global_y_.SetTimeDirection(true);
// Note that the code assumes that this was registered twice in fast and slow
// mode. So we will not redo some propagation in slow mode that was already
// done by the fast mode.
const bool fast_propagation = watcher_->GetCurrentId() == fast_id_;
RETURN_IF_FALSE(FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
fast_propagation, global_x_, &global_y_));
// We can actually swap dimensions to propagate vertically.
RETURN_IF_FALSE(FindBoxesThatMustOverlapAHorizontalLineAndPropagate(
fast_propagation, global_y_, &global_x_));
if (!fast_propagation && (has_zero_area_boxes_ || pairwise_propagation_)) {
RETURN_IF_FALSE(PropagateAllPairsOfBoxes());
}
return true;
}
// Specialized propagation on only two boxes that must intersect with the
// given y_line_for_reason.
bool NonOverlappingRectanglesDisjunctivePropagator::
PropagateOnXWhenOnlyTwoBoxes() {
if (!x_.IsPresent(0) || !x_.IsPresent(1)) return true;
// For each direction and each order, we test if the boxes can be disjoint.
const int state =
(x_.EndMin(0) <= x_.StartMax(1)) + 2 * (x_.EndMin(1) <= x_.StartMax(0));
switch (state) {
case 0: { // Conflict.
ClearAndAddMandatoryOverlapReason(0, 1, &x_);
// Note that the secondary helper is set on x.
return x_.ReportConflict();
}
case 1: { // b1 is left of b2.
return LeftBoxBeforeRightBoxOnFirstDimension(0, 1, &x_, /*y=*/nullptr);
}
case 2: { // b2 is left of b1.
return LeftBoxBeforeRightBoxOnFirstDimension(1, 0, &x_, /*y=*/nullptr);
}
default: { // Nothing to deduce.
return true;
}
}
}
// TODO(user): Use box splitting to speed up.
bool NonOverlappingRectanglesDisjunctivePropagator::PropagateAllPairsOfBoxes() {
// Extra propagation code for zero-area boxes, and for all pairs of boxes in
// pairwise_propagation_ mode.
DCHECK(pairwise_propagation_ || has_zero_area_boxes_);
horizontal_zero_area_boxes_.clear();
vertical_zero_area_boxes_.clear();
point_zero_area_boxes_.clear();
non_zero_area_boxes_.clear();
for (int b = 0; b < global_x_.NumTasks(); ++b) {
if (!global_x_.IsPresent(b) || !global_y_.IsPresent(b)) continue;
const IntegerValue x_size_max = global_x_.SizeMax(b);
const IntegerValue y_size_max = global_y_.SizeMax(b);
if (x_size_max == 0) {
if (y_size_max == 0) {
point_zero_area_boxes_.push_back(b);
} else {
vertical_zero_area_boxes_.push_back(b);
}
} else if (y_size_max == 0) {
horizontal_zero_area_boxes_.push_back(b);
} else {
non_zero_area_boxes_.push_back(b);
}
}
if (pairwise_propagation_) {
for (int i1 = 0; i1 + 1 < non_zero_area_boxes_.size(); ++i1) {
for (int i2 = i1 + 1; i2 < non_zero_area_boxes_.size(); ++i2) {
RETURN_IF_FALSE(PropagateTwoBoxes(non_zero_area_boxes_[i1],
non_zero_area_boxes_[i2]));
}
}
}
// Propagates zero area boxes against non-zero area boxes.
for (const int nz : non_zero_area_boxes_) {
for (const int z : horizontal_zero_area_boxes_) {
RETURN_IF_FALSE(PropagateTwoBoxes(z, nz));
}
for (const int z : vertical_zero_area_boxes_) {
RETURN_IF_FALSE(PropagateTwoBoxes(z, nz));
}
for (const int z : point_zero_area_boxes_) {
RETURN_IF_FALSE(PropagateTwoBoxes(z, nz));
}
}
// Propagates vertical zero area boxes against horizontal zero area boxes.
for (const int i1 : horizontal_zero_area_boxes_) {
for (const int i2 : vertical_zero_area_boxes_) {
RETURN_IF_FALSE(PropagateTwoBoxes(i1, i2));
}
}
return true;
}
bool NonOverlappingRectanglesDisjunctivePropagator::PropagateTwoBoxes(
int box1, int box2) {
// We use the global helpers, without the mechanism of sub-helpers.
// So any reason will need to be computed on both dimensions, and imported in
// the helper doing the modification.
DCHECK(!global_x_.HasOtherHelper());
DCHECK(!global_y_.HasOtherHelper());
const int state =
// box1 can be left of box2.
(global_x_.EndMin(box1) <= global_x_.StartMax(box2)) +
// box1 can be right of box2.
2 * (global_x_.EndMin(box2) <= global_x_.StartMax(box1)) +
// box1 can be below box2.
4 * (global_y_.EndMin(box1) <= global_y_.StartMax(box2)) +
// box1 can be up of box2.
8 * (global_y_.EndMin(box2) <= global_y_.StartMax(box1));
switch (state) {
case 0: { // Conflict. The two boxes must overlap in both dimensions.
return ClearAndAddTwoBoxesConflictReason(box1, box2, &global_x_,
&global_y_);
}
case 1: { // box2 can only be after box1 on x.
return LeftBoxBeforeRightBoxOnFirstDimension(box1, box2, &global_x_,
&global_y_);
}
case 2: { // box1 an only be after box2 on x.
return LeftBoxBeforeRightBoxOnFirstDimension(box2, box1, &global_x_,
&global_y_);
}
case 4: { // box2 an only be after box1 on y.
return LeftBoxBeforeRightBoxOnFirstDimension(box1, box2, &global_y_,
&global_x_);
}
case 8: { // box1 an only be after box2 on y.
return LeftBoxBeforeRightBoxOnFirstDimension(box2, box1, &global_y_,
&global_x_);
}
default: {
break;
}
}
return true;
}
#undef RETURN_IF_FALSE
} // namespace sat
} // namespace operations_research
Reference in New Issue View Git Blame Copy Permalink