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

647 lines
24 KiB
C++
Raw Blame History

// Copyright 2010-2021 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 <algorithm>
#include <cstdint>
#include <limits>
#include <utility>
#include <vector>
#include "absl/container/flat_hash_set.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/sat/util.h"
#include "ortools/util/saturated_arithmetic.h"
#include "ortools/util/strong_integers.h"
namespace operations_research {
namespace sat {
namespace {
// TODO(user): Use the faster variable only version if all expressions reduce
// to a single variable?
void AddIsEqualToMinOf(IntegerVariable min_var,
const std::vector<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;
target.vars.push_back(min_var);
target.coeffs.push_back(IntegerValue(1));
model->Add(IsEqualToMinOf(target, converted));
}
void AddIsEqualToMaxOf(IntegerVariable max_var,
const std::vector<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;
target.vars.push_back(NegationOf(max_var));
target.coeffs.push_back(IntegerValue(1));
model->Add(IsEqualToMinOf(target, converted));
}
} // namespace
void AddDiffnCumulativeRelationOnX(
const std::vector<IntervalVariable>& x_intervals,
SchedulingConstraintHelper* x, SchedulingConstraintHelper* y,
Model* model) {
int64_t min_starts = std::numeric_limits<int64_t>::max();
int64_t max_ends = std::numeric_limits<int64_t>::min();
std::vector<AffineExpression> sizes;
for (int box = 0; box < y->NumTasks(); ++box) {
min_starts = std::min(min_starts, y->StartMin(box).value());
max_ends = std::max(max_ends, y->EndMax(box).value());
sizes.push_back(y->Sizes()[box]);
}
const IntegerVariable min_start_var =
model->Add(NewIntegerVariable(min_starts, max_ends));
AddIsEqualToMinOf(min_start_var, y->Starts(), model);
const IntegerVariable max_end_var =
model->Add(NewIntegerVariable(min_starts, max_ends));
AddIsEqualToMaxOf(max_end_var, y->Ends(), model);
// (max_end - min_start) >= capacity.
const AffineExpression capacity(
model->Add(NewIntegerVariable(0, CapSub(max_ends, min_starts))));
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()));
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
auto* watcher = model->GetOrCreate<GenericLiteralWatcher>();
// 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.
TimeTablingPerTask* time_tabling =
new TimeTablingPerTask(sizes, capacity, integer_trail, x);
time_tabling->RegisterWith(watcher);
model->TakeOwnership(time_tabling);
// Propagator responsible for applying the Overload Checking filtering rule.
// It increases the minimum of the capacity variable.
if (model->GetOrCreate<SatParameters>()
->use_overload_checker_in_cumulative_constraint()) {
AddCumulativeOverloadChecker(sizes, capacity, x, model);
}
}
#define RETURN_IF_FALSE(f) \
if (!(f)) return false;
NonOverlappingRectanglesEnergyPropagator::
~NonOverlappingRectanglesEnergyPropagator() {}
bool NonOverlappingRectanglesEnergyPropagator::Propagate() {
const int num_boxes = x_.NumTasks();
if (!x_.SynchronizeAndSetTimeDirection(true)) return false;
if (!y_.SynchronizeAndSetTimeDirection(true)) return false;
active_boxes_.clear();
cached_energies_.resize(num_boxes);
cached_rectangles_.resize(num_boxes);
for (int box = 0; box < num_boxes; ++box) {
cached_energies_[box] = x_.SizeMin(box) * y_.SizeMin(box);
if (cached_energies_[box] == 0) continue;
if (!x_.IsPresent(box) || !y_.IsPresent(box)) continue;
// The code needs the size min to be larger or equal to the mandatory part
// for it to works correctly. This is always enforced by the helper.
DCHECK_GE(x_.SizeMin(box), x_.EndMin(box) - x_.StartMax(box));
DCHECK_GE(y_.SizeMin(box), y_.EndMin(box) - y_.StartMax(box));
Rectangle& rectangle = cached_rectangles_[box];
rectangle.x_min = x_.ShiftedStartMin(box);
rectangle.x_max = x_.ShiftedEndMax(box);
rectangle.y_min = y_.ShiftedStartMin(box);
rectangle.y_max = y_.ShiftedEndMax(box);
active_boxes_.push_back(box);
}
absl::Span<int> initial_boxes = FilterBoxesThatAreTooLarge(
cached_rectangles_, cached_energies_, absl::MakeSpan(active_boxes_));
if (initial_boxes.size() <= 1) return true;
Rectangle conflicting_rectangle;
std::vector<absl::Span<int>> components =
GetOverlappingRectangleComponents(cached_rectangles_, initial_boxes);
for (absl::Span<int> boxes : components) {
// Computes the size on x and y past which there is no point doing any
// energetic reasonning. We do a few iterations since as we filter one size,
// we can potentially filter more on the transposed dimension.
threshold_x_ = kMaxIntegerValue;
threshold_y_ = kMaxIntegerValue;
for (int i = 0; i < 3; ++i) {
if (!AnalyzeIntervals(/*transpose=*/i == 1, boxes, cached_rectangles_,
cached_energies_, &threshold_x_, &threshold_y_,
&conflicting_rectangle)) {
return ReportEnergyConflict(conflicting_rectangle, boxes, &x_, &y_);
}
boxes = FilterBoxesAndRandomize(cached_rectangles_, boxes, threshold_x_,
threshold_y_, *random_);
if (boxes.size() <= 1) break;
}
if (boxes.size() <= 1) continue;
// Now that we removed boxes with a large domain, resplit everything.
const std::vector<absl::Span<int>> local_components =
GetOverlappingRectangleComponents(cached_rectangles_, boxes);
for (absl::Span<int> local_boxes : local_components) {
IntegerValue total_sum_of_areas(0);
for (const int box : local_boxes) {
total_sum_of_areas += cached_energies_[box];
}
for (const int box : local_boxes) {
RETURN_IF_FALSE(
FailWhenEnergyIsTooLarge(box, local_boxes, total_sum_of_areas));
}
}
}
return true;
}
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::SortBoxesIntoNeighbors(
int box, absl::Span<const int> local_boxes,
IntegerValue total_sum_of_areas) {
const Rectangle& box_dim = cached_rectangles_[box];
neighbors_.clear();
for (const int other_box : local_boxes) {
if (other_box == box) continue;
const Rectangle& other_dim = cached_rectangles_[other_box];
const IntegerValue span_x = std::max(box_dim.x_max, other_dim.x_max) -
std::min(box_dim.x_min, other_dim.x_min);
if (span_x > threshold_x_) continue;
const IntegerValue span_y = std::max(box_dim.y_max, other_dim.y_max) -
std::min(box_dim.y_min, other_dim.y_min);
if (span_y > threshold_y_) continue;
const IntegerValue bounding_area = span_x * span_y;
if (bounding_area < total_sum_of_areas) {
neighbors_.push_back({other_box, bounding_area});
}
}
std::sort(neighbors_.begin(), neighbors_.end());
}
bool NonOverlappingRectanglesEnergyPropagator::FailWhenEnergyIsTooLarge(
int box, absl::Span<const int> local_boxes,
IntegerValue total_sum_of_areas) {
SortBoxesIntoNeighbors(box, local_boxes, total_sum_of_areas);
CapacityProfile bounding_area;
IntegerValue sum_of_areas = cached_energies_[box];
Rectangle area = cached_rectangles_[box];
bounding_area.AddRectangle(
cached_rectangles_[box].x_min, cached_rectangles_[box].x_max,
cached_rectangles_[box].y_min, cached_rectangles_[box].y_max);
const auto add_box_energy_in_rectangle_reason = [&](int b) {
x_.AddEnergyMinInIntervalReason(b, area.x_min, area.x_max);
y_.AddEnergyMinInIntervalReason(b, area.y_min, area.y_max);
x_.AddPresenceReason(b);
y_.AddPresenceReason(b);
};
// TODO(user): using the bounding area profile we can relax this reason.
const auto add_precise_box_energy_reason = [&](int b) {
x_.AddStartMinReason(b, x_.StartMin(b));
x_.AddEndMaxReason(b, x_.EndMax(b));
x_.AddSizeMinReason(b, x_.SizeMin(b));
y_.AddStartMinReason(b, y_.StartMin(b));
y_.AddEndMaxReason(b, y_.EndMax(b));
y_.AddSizeMinReason(b, y_.SizeMin(b));
x_.AddPresenceReason(b);
y_.AddPresenceReason(b);
};
for (int i = 0; i < neighbors_.size(); ++i) {
const int other_box = neighbors_[i].box;
const Rectangle& other = cached_rectangles_[other_box];
CHECK_GT(cached_energies_[other_box], 0);
// Update Bounding box.
area.TakeUnionWith(other);
if (area.x_max - area.x_min > threshold_x_) break;
if (area.y_max - area.y_min > threshold_y_) break;
// Update precise bounding area.
// TODO(user): speed up (cache, maintain profile, ...)
bounding_area.AddRectangle(other.x_min, other.x_max, other.y_min,
other.y_max);
// Update sum of areas.
sum_of_areas += cached_energies_[other_box];
const IntegerValue bounding_rectangle_area =
(area.x_max - area.x_min) * (area.y_max - area.y_min);
const IntegerValue precise_area = bounding_area.GetBoundingArea();
if (precise_area >= total_sum_of_areas) {
// Nothing will be deduced. Exiting.
return true;
}
if (sum_of_areas > precise_area) {
x_.ClearReason();
y_.ClearReason();
if (sum_of_areas > bounding_rectangle_area) {
// Use the more general relaxation.
add_box_energy_in_rectangle_reason(box);
for (int j = 0; j <= i; ++j) {
add_box_energy_in_rectangle_reason(neighbors_[j].box);
}
} else {
add_precise_box_energy_reason(box);
for (int j = 0; j <= i; ++j) {
add_precise_box_energy_reason(neighbors_[j].box);
}
}
x_.ImportOtherReasons(y_);
return x_.ReportConflict();
}
}
return true;
}
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);
}
}
} // namespace
// Note that x_ and y_ must be initialized with enough intervals when passed
// to the disjunctive propagators.
NonOverlappingRectanglesDisjunctivePropagator::
NonOverlappingRectanglesDisjunctivePropagator(bool strict,
SchedulingConstraintHelper* x,
SchedulingConstraintHelper* y,
Model* model)
: global_x_(*x),
global_y_(*y),
x_(x->NumTasks(), model),
strict_(strict),
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_) {}
NonOverlappingRectanglesDisjunctivePropagator::
~NonOverlappingRectanglesDisjunctivePropagator() {}
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_intervals_.clear();
const std::vector<TaskTime>& temp = y->TaskByDecreasingStartMax();
for (int i = temp.size(); --i >= 0;) {
const int box = temp[i].task_index;
if (!strict_ && (x.SizeMin(box) == 0 || y->SizeMin(box) == 0)) continue;
// 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_intervals_.push_back({box, start_max, end_min});
}
}
// Less than 2 boxes, no propagation.
if (indexed_intervals_.size() < 2) return true;
ConstructOverlappingSets(/*already_sorted=*/true, &indexed_intervals_,
&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(PropagateTwoBoxes());
} 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 two boxes must overlap but do not have a mandatory line/column that
// crosses both of them, then the code above do not see it. So we manually
// propagate this case.
//
// TODO(user): Since we are at it, do more propagation even if no conflict?
// This rarely propagate, so disabled for now. Investigate if it is worth
// it.
if (/*DISABLES CODE*/ (false) && watcher_->GetCurrentId() == fast_id_) {
const int num_boxes = global_x_.NumTasks();
for (int box1 = 0; box1 < num_boxes; ++box1) {
if (!global_x_.IsPresent(box1)) continue;
for (int box2 = box1 + 1; box2 < num_boxes; ++box2) {
if (!global_x_.IsPresent(box2)) continue;
if (global_x_.EndMin(box1) <= global_x_.StartMax(box2)) continue;
if (global_x_.EndMin(box2) <= global_x_.StartMax(box1)) continue;
if (global_y_.EndMin(box1) <= global_y_.StartMax(box2)) continue;
if (global_y_.EndMin(box2) <= global_y_.StartMax(box1)) continue;
// X and Y must overlap. This is a conflict.
global_x_.ClearReason();
global_x_.AddPresenceReason(box1);
global_x_.AddPresenceReason(box2);
global_x_.AddReasonForBeingBefore(box1, box2);
global_x_.AddReasonForBeingBefore(box2, box1);
global_y_.ClearReason();
global_y_.AddPresenceReason(box1);
global_y_.AddPresenceReason(box2);
global_y_.AddReasonForBeingBefore(box1, box2);
global_y_.AddReasonForBeingBefore(box2, box1);
global_x_.ImportOtherReasons(global_y_);
return global_x_.ReportConflict();
}
}
}
return true;
}
// Specialized propagation on only two boxes that must intersect with the
// given y_line_for_reason.
bool NonOverlappingRectanglesDisjunctivePropagator::PropagateTwoBoxes() {
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));
const auto left_box_before_right_box = [this](int left, int right) {
// left box pushes right box.
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);
RETURN_IF_FALSE(x_.IncreaseStartMin(right, left_end_min));
}
// right box pushes left box.
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);
RETURN_IF_FALSE(x_.DecreaseEndMax(left, right_start_max));
}
return true;
};
switch (state) {
case 0: { // Conflict.
x_.ClearReason();
x_.AddPresenceReason(0);
x_.AddPresenceReason(1);
x_.AddReasonForBeingBefore(0, 1);
x_.AddReasonForBeingBefore(1, 0);
return x_.ReportConflict();
}
case 1: { // b1 is left of b2.
return left_box_before_right_box(0, 1);
}
case 2: { // b2 is left of b1.
return left_box_before_right_box(1, 0);
}
default: { // Nothing to deduce.
return true;
}
}
}
#undef RETURN_IF_FALSE
} // namespace sat
} // namespace operations_research
Reference in New Issue View Git Blame Copy Permalink