always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] more work on precedences

Browse Source
This commit is contained in:
Laurent Perron
2025-06-12 11:11:26 +02:00
parent c229e9facd
commit d1c3c7f84b
11 changed files with 393 additions and 329 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
ortools/sat/2d_distances_propagator.cc
View File

@@ -180,15 +180,10 @@ bool Precedences2DPropagator::Propagate() {
if (j == 1) {
std::swap(b1, b2);
}
LinearExpression2 expr;
expr.vars[0] = helper->Starts()[b1].var;
expr.vars[1] = helper->Ends()[b2].var;
expr.coeffs[0] = helper->Starts()[b1].coeff;
expr.coeffs[1] = -helper->Ends()[b2].coeff;
const auto [expr, ub] = EncodeDifferenceLowerThan(
helper->Starts()[b1], helper->Ends()[b2], -1);
linear2_bounds_->AddReasonForUpperBoundLowerThan(
expr,
-(helper->Starts()[b1].constant - helper->Ends()[b2].constant) - 1,
helper_.x_helper().MutableLiteralReason(),
expr, ub, helper_.x_helper().MutableLiteralReason(),
helper_.x_helper().MutableIntegerReason());
}
}

2
ortools/sat/cp_model_solver_helpers.cc
View File

@@ -1155,7 +1155,7 @@ void FillBinaryRelationRepository(const CpModelProto& model_proto,
}
}
}
repository->Build(root_level_lin2_bounds);
repository->Build();
}
} // namespace

13
ortools/sat/disjunctive.cc
View File

@@ -1254,6 +1254,7 @@ bool DisjunctivePrecedences::PropagateSubwindow() {
int best_index = -1;
const IntegerValue current_var_lb = integer_trail_->LowerBound(var);
IntegerValue best_new_lb = current_var_lb;
IntegerValue min_offset_at_best = kMinIntegerValue;
IntegerValue min_offset = kMaxIntegerValue;
IntegerValue sum_of_duration = 0;
for (int i = num_before; --i >= 0;) {
@@ -1298,6 +1299,7 @@ bool DisjunctivePrecedences::PropagateSubwindow() {
const IntegerValue start = task_time.time;
const IntegerValue new_lb = start + sum_of_duration + min_offset;
if (new_lb > best_new_lb) {
min_offset_at_best = min_offset;
best_new_lb = new_lb;
best_index = i;
}
@@ -1315,14 +1317,13 @@ bool DisjunctivePrecedences::PropagateSubwindow() {
helper_->AddPresenceReason(ct);
helper_->AddEnergyAfterReason(ct, helper_->SizeMin(ct), window_start);
// Fetch the explanation.
// Fetch the explanation of (var - end) >= min_offset
// This is okay if a bit slow since we only do that when we push.
const AffineExpression& end_exp = helper_->Ends()[ct];
const LinearExpression2 expr =
LinearExpression2::Difference(end_exp.var, var);
const auto [expr, ub] = EncodeDifferenceLowerThan(
helper_->Ends()[ct], var, -min_offset_at_best);
linear2_bounds_->AddReasonForUpperBoundLowerThan(
expr, linear2_bounds_->UpperBound(expr),
helper_->MutableLiteralReason(), helper_->MutableIntegerReason());
expr, ub, helper_->MutableLiteralReason(),
helper_->MutableIntegerReason());
}
++stats_.num_propagations;
if (!helper_->PushIntegerLiteral(

18
ortools/sat/integer_base.h
View File

@@ -427,6 +427,24 @@ struct LinearExpression2 {
}
};
// Encodes (a - b <= ub) in (linear2 <= ub) format.
// Note that the returned expression is canonicalized and divided by its GCD.
inline std::pair<LinearExpression2, IntegerValue> EncodeDifferenceLowerThan(
AffineExpression a, AffineExpression b, IntegerValue ub) {
LinearExpression2 expr;
expr.vars[0] = a.var;
expr.coeffs[0] = a.coeff;
expr.vars[1] = b.var;
expr.coeffs[1] = -b.coeff;
IntegerValue rhs = ub + b.constant - a.constant;
// Canonicalize.
expr.SimpleCanonicalization();
const IntegerValue gcd = expr.DivideByGcd();
rhs = FloorRatio(rhs, gcd);
return {std::move(expr), rhs};
}
template <typename H>
H AbslHashValue(H h, const LinearExpression2& e) {
h = H::combine(std::move(h), e.vars[0]);

239
ortools/sat/precedences.cc
View File

@@ -57,6 +57,7 @@ namespace sat {
std::pair<bool, bool> RootLevelLinear2Bounds::Add(LinearExpression2 expr,
IntegerValue lb,
IntegerValue ub) {
using AddResult = BestBinaryRelationBounds::AddResult;
const IntegerValue zero_level_lb = integer_trail_->LevelZeroLowerBound(expr);
const IntegerValue zero_level_ub = integer_trail_->LevelZeroUpperBound(expr);
if (lb <= zero_level_lb && ub >= zero_level_ub) {
@@ -73,15 +74,14 @@ std::pair<bool, bool> RootLevelLinear2Bounds::Add(LinearExpression2 expr,
const auto [status_lb, status_ub] = root_level_relations_.Add(expr, lb, ub);
const bool lb_restricted =
status_lb == BestBinaryRelationBounds::AddResult::ADDED ||
status_lb == BestBinaryRelationBounds::AddResult::UPDATED;
status_lb == AddResult::ADDED || status_lb == AddResult::UPDATED;
const bool ub_restricted =
status_ub == BestBinaryRelationBounds::AddResult::ADDED ||
status_ub == BestBinaryRelationBounds::AddResult::UPDATED;
status_ub == AddResult::ADDED || status_ub == AddResult::UPDATED;
if (!lb_restricted && !ub_restricted) return {false, false};
++num_updates_;
// Update our special coeff=1 lookup table.
if (expr.coeffs[0] == 1 && expr.coeffs[1] == 1) {
// +2 to handle possible negation.
const int new_size =
@@ -89,19 +89,69 @@ std::pair<bool, bool> RootLevelLinear2Bounds::Add(LinearExpression2 expr,
if (new_size > coeff_one_var_lookup_.size()) {
coeff_one_var_lookup_.resize(new_size);
}
if (status_lb == BestBinaryRelationBounds::AddResult::ADDED) {
if (status_lb == AddResult::ADDED) {
// First time added to root_level_relations_.
coeff_one_var_lookup_[NegationOf(expr.vars[0])].push_back(
NegationOf(expr.vars[1]));
coeff_one_var_lookup_[NegationOf(expr.vars[1])].push_back(
NegationOf(expr.vars[0]));
}
if (status_ub == BestBinaryRelationBounds::AddResult::ADDED) {
if (status_ub == AddResult::ADDED) {
coeff_one_var_lookup_[expr.vars[0]].push_back(expr.vars[1]);
coeff_one_var_lookup_[expr.vars[1]].push_back(expr.vars[0]);
}
}
// Update our per-variable and per-pair lookup tables.
IntegerVariable var1 = PositiveVariable(expr.vars[0]);
IntegerVariable var2 = PositiveVariable(expr.vars[1]);
if (var1 > var2) std::swap(var1, var2);
auto [it_var, inserted] = var_to_bounds_vector_index_.insert({expr, {0, 0}});
for (const IntegerVariable var : {var1, var2}) {
auto& var_bounds = var_to_bounds_[var];
if (inserted) {
if (var == var1) {
it_var->second.first = var_bounds.size();
} else {
it_var->second.second = var_bounds.size();
}
var_bounds.push_back({expr, lb, ub});
} else {
const int index =
(var == var1) ? it_var->second.first : it_var->second.second;
DCHECK_LT(index, var_bounds.size());
std::tuple<LinearExpression2, IntegerValue, IntegerValue>& var_bound =
var_bounds[index];
if (status_lb == AddResult::ADDED || status_lb == AddResult::UPDATED) {
std::get<1>(var_bound) = lb;
}
if (status_ub == AddResult::ADDED || status_ub == AddResult::UPDATED) {
std::get<2>(var_bound) = ub;
}
}
}
auto [it_pair, pair_inserted] =
var_pair_to_bounds_vector_index_.insert({expr, 0});
DCHECK_EQ(inserted, pair_inserted);
auto& pair_bounds = var_pair_to_bounds_[{var1, var2}];
if (pair_inserted) {
it_pair->second = pair_bounds.size();
pair_bounds.push_back({expr, lb, ub});
} else {
const int index = it_pair->second;
DCHECK_LT(index, pair_bounds.size());
std::tuple<LinearExpression2, IntegerValue, IntegerValue>& pair_bound =
pair_bounds[index];
if (status_lb == AddResult::ADDED || status_lb == AddResult::UPDATED) {
std::get<1>(pair_bound) = lb;
}
if (status_ub == AddResult::ADDED || status_ub == AddResult::UPDATED) {
std::get<2>(pair_bound) = ub;
}
}
return {lb_restricted, ub_restricted};
}
@@ -142,6 +192,95 @@ IntegerValue RootLevelLinear2Bounds::GetUpperBoundNoTrail(
return root_level_relations_.UpperBoundWhenCanonicalized(expr);
}
std::vector<std::pair<LinearExpression2, IntegerValue>>
RootLevelLinear2Bounds::GetSortedNonTrivialUpperBounds() const {
std::vector<std::pair<LinearExpression2, IntegerValue>> result =
root_level_relations_.GetSortedNonTrivialUpperBounds();
int new_size = 0;
for (int i = 0; i < result.size(); ++i) {
const auto& [expr, ub] = result[i];
if (ub < integer_trail_->LevelZeroUpperBound(expr)) {
result[new_size] = {expr, ub};
++new_size;
}
}
result.resize(new_size);
return result;
}
// Return a list of (lb <= expr <= ub), with expr.vars[0] = var, where at
// least one of the bounds is non-trivial and the potential other non-trivial
// bound is tight.
std::vector<std::tuple<LinearExpression2, IntegerValue, IntegerValue>>
RootLevelLinear2Bounds::GetAllBoundsContainingVariable(
IntegerVariable var) const {
std::vector<std::tuple<LinearExpression2, IntegerValue, IntegerValue>> result;
auto it = var_to_bounds_.find(PositiveVariable(var));
if (it == var_to_bounds_.end()) return {};
for (const auto& [expr, lb, ub] : it->second) {
const IntegerValue trail_lb = integer_trail_->LevelZeroLowerBound(expr);
const IntegerValue trail_ub = integer_trail_->LevelZeroUpperBound(expr);
if (lb <= trail_lb && ub >= trail_ub) continue;
LinearExpression2 explicit_vars_expr = expr;
if (explicit_vars_expr.vars[0] == NegationOf(var)) {
explicit_vars_expr.vars[0] = NegationOf(explicit_vars_expr.vars[0]);
explicit_vars_expr.coeffs[0] = -explicit_vars_expr.coeffs[0];
}
if (explicit_vars_expr.vars[1] == NegationOf(var)) {
explicit_vars_expr.vars[1] = NegationOf(explicit_vars_expr.vars[1]);
explicit_vars_expr.coeffs[1] = -explicit_vars_expr.coeffs[1];
}
if (explicit_vars_expr.vars[1] == var) {
std::swap(explicit_vars_expr.vars[0], explicit_vars_expr.vars[1]);
std::swap(explicit_vars_expr.coeffs[0], explicit_vars_expr.coeffs[1]);
}
DCHECK(explicit_vars_expr.vars[0] == var);
result.push_back(
{explicit_vars_expr, std::max(lb, trail_lb), std::min(ub, trail_ub)});
}
return result;
}
// Return a list of (lb <= expr <= ub), with expr.vars = {var1, var2}, where
// at least one of the bounds is non-trivial and the potential other
// non-trivial bound is tight.
std::vector<std::tuple<LinearExpression2, IntegerValue, IntegerValue>>
RootLevelLinear2Bounds::GetAllBoundsContainingVariables(
IntegerVariable var1, IntegerVariable var2) const {
std::vector<std::tuple<LinearExpression2, IntegerValue, IntegerValue>> result;
std::pair<IntegerVariable, IntegerVariable> key = {PositiveVariable(var1),
PositiveVariable(var2)};
if (key.first > key.second) std::swap(key.first, key.second);
auto it = var_pair_to_bounds_.find(key);
if (it == var_pair_to_bounds_.end()) return {};
for (const auto& [expr, lb, ub] : it->second) {
const IntegerValue trail_lb = integer_trail_->LevelZeroLowerBound(expr);
const IntegerValue trail_ub = integer_trail_->LevelZeroUpperBound(expr);
if (lb <= trail_lb && ub >= trail_ub) continue;
LinearExpression2 explicit_vars_expr = expr;
if (explicit_vars_expr.vars[0] == NegationOf(var1) ||
explicit_vars_expr.vars[0] == NegationOf(var2)) {
explicit_vars_expr.vars[0] = NegationOf(explicit_vars_expr.vars[0]);
explicit_vars_expr.coeffs[0] = -explicit_vars_expr.coeffs[0];
}
if (explicit_vars_expr.vars[1] == NegationOf(var1) ||
explicit_vars_expr.vars[1] == NegationOf(var2)) {
explicit_vars_expr.vars[1] = NegationOf(explicit_vars_expr.vars[1]);
explicit_vars_expr.coeffs[1] = -explicit_vars_expr.coeffs[1];
}
if (explicit_vars_expr.vars[1] == var1) {
std::swap(explicit_vars_expr.vars[0], explicit_vars_expr.vars[1]);
std::swap(explicit_vars_expr.coeffs[0], explicit_vars_expr.coeffs[1]);
}
DCHECK(explicit_vars_expr.vars[0] == var1 &&
explicit_vars_expr.vars[1] == var2);
result.push_back(
{explicit_vars_expr, std::max(lb, trail_lb), std::min(ub, trail_ub)});
}
return result;
}
EnforcedLinear2Bounds::~EnforcedLinear2Bounds() {
if (!VLOG_IS_ON(1)) return;
std::vector<std::pair<std::string, int64_t>> stats;
@@ -244,7 +383,7 @@ void EnforcedLinear2Bounds::AddReasonForUpperBoundLowerThan(
std::vector<Literal>* literal_reason,
std::vector<IntegerLiteral>* /*unused*/) const {
expr.SimpleCanonicalization();
if (ub >= LevelZeroUpperBound(expr)) return;
if (ub >= root_level_bounds_->LevelZeroUpperBound(expr)) return;
const IntegerValue gcd = expr.DivideByGcd();
const auto it = conditional_relations_.find(expr);
DCHECK(it != conditional_relations_.end());
@@ -255,31 +394,12 @@ void EnforcedLinear2Bounds::AddReasonForUpperBoundLowerThan(
CHECK(trail_->Assignment().LiteralIsTrue(l));
}
}
DCHECK_EQ(CapProdI(gcd, entry.rhs), UpperBound(expr));
DCHECK_LE(CapProdI(gcd, entry.rhs), ub);
for (const Literal l : entry.enforcements) {
literal_reason->push_back(l.Negated());
}
}
IntegerValue EnforcedLinear2Bounds::UpperBound(LinearExpression2 expr) const {
expr.SimpleCanonicalization();
const IntegerValue gcd = expr.DivideByGcd();
const auto it = conditional_relations_.find(expr);
if (it != conditional_relations_.end()) {
const ConditionalEntry& entry = conditional_stack_[it->second];
if (DEBUG_MODE) {
for (const Literal l : entry.enforcements) {
CHECK(trail_->Assignment().LiteralIsTrue(l));
}
}
DCHECK_LT(entry.rhs, root_level_bounds_->LevelZeroUpperBound(expr));
return CapProdI(gcd, entry.rhs);
}
return CapProdI(gcd, root_level_bounds_->LevelZeroUpperBound(expr));
}
IntegerValue EnforcedLinear2Bounds::GetUpperBoundFromEnforced(
LinearExpression2 expr) const {
DCHECK_EQ(expr.DivideByGcd(), 1);
@@ -1241,48 +1361,22 @@ void BinaryRelationRepository::AddPartialRelation(Literal lit,
Add(lit, LinearExpression2(a, b, 1, 1), 0, 0);
}
void BinaryRelationRepository::Build(
const RootLevelLinear2Bounds* root_level_bounds) {
for (const auto& [expr, lb, ub] :
root_level_bounds->GetSortedNonTrivialBounds()) {
LinearExpression2 positive_expr = expr;
positive_expr.MakeVariablesPositive();
Relation r;
r.enforcement = Literal(kNoLiteralIndex);
r.expr = positive_expr;
r.rhs = root_level_bounds->LevelZeroUpperBound(positive_expr);
positive_expr.Negate();
r.lhs = -root_level_bounds->LevelZeroUpperBound(positive_expr);
relations_.push_back(r);
}
void BinaryRelationRepository::Build() {
DCHECK(!is_built_);
is_built_ = true;
std::vector<std::pair<LiteralIndex, int>> literal_key_values;
std::vector<std::pair<IntegerVariable, int>> var_key_values;
const int num_relations = relations_.size();
literal_key_values.reserve(num_enforced_relations_);
var_key_values.reserve(num_relations - num_enforced_relations_);
for (int i = 0; i < num_relations; ++i) {
const Relation& r = relations_[i];
if (r.enforcement.Index() == kNoLiteralIndex) {
var_key_values.emplace_back(r.expr.vars[0], i);
var_key_values.emplace_back(r.expr.vars[1], i);
std::pair<IntegerVariable, IntegerVariable> key(r.expr.vars[0],
r.expr.vars[1]);
if (relations_[i].expr.vars[0] > relations_[i].expr.vars[1]) {
std::swap(key.first, key.second);
}
var_pair_to_relations_[key].push_back(i);
} else {
literal_key_values.emplace_back(r.enforcement.Index(), i);
}
literal_key_values.emplace_back(r.enforcement.Index(), i);
}
lit_to_relations_.ResetFromPairs(literal_key_values);
var_to_relations_.ResetFromPairs(var_key_values);
}
bool BinaryRelationRepository::PropagateLocalBounds(
const IntegerTrail& integer_trail, Literal lit,
const IntegerTrail& integer_trail,
const RootLevelLinear2Bounds& root_level_bounds, Literal lit,
const absl::flat_hash_map<IntegerVariable, IntegerValue>& input,
absl::flat_hash_map<IntegerVariable, IntegerValue>* output) const {
DCHECK_NE(lit.Index(), kNoLiteralIndex);
@@ -1334,9 +1428,10 @@ bool BinaryRelationRepository::PropagateLocalBounds(
}
}
for (const auto& [var, _] : input) {
if (var >= var_to_relations_.size()) continue;
for (const int relation_index : var_to_relations_[var]) {
update_var_bounds_from_relation(relations_[relation_index]);
for (const auto& [expr, lb, ub] :
root_level_bounds.GetAllBoundsContainingVariable(var)) {
update_var_bounds_from_relation(
Relation{Literal(kNoLiteralIndex), expr, lb, ub});
}
}
@@ -1648,29 +1743,16 @@ Linear2BoundsFromLinear3::~Linear2BoundsFromLinear3() {
shared_stats_->AddStats(stats);
}
std::pair<LinearExpression2, IntegerValue> ReifiedLinear2Bounds::FromDifference(
const AffineExpression& a, const AffineExpression& b) const {
LinearExpression2 expr;
expr.vars[0] = a.var;
expr.vars[1] = b.var;
expr.coeffs[0] = a.coeff;
expr.coeffs[1] = -b.coeff;
IntegerValue lb = kMinIntegerValue; // unused.
IntegerValue ub = b.constant - a.constant;
expr.CanonicalizeAndUpdateBounds(lb, ub, /*allow_negation=*/false);
return {std::move(expr), ub};
}
RelationStatus ReifiedLinear2Bounds::GetLevelZeroPrecedenceStatus(
AffineExpression a, AffineExpression b) const {
const auto [expr, ub] = FromDifference(a, b);
const auto [expr, ub] = EncodeDifferenceLowerThan(a, b, 0);
return best_root_level_bounds_->GetLevelZeroStatus(expr, kMinIntegerValue,
ub);
}
void ReifiedLinear2Bounds::AddReifiedPrecedenceIfNonTrivial(
Literal l, AffineExpression a, AffineExpression b) {
const auto [expr, ub] = FromDifference(a, b);
const auto [expr, ub] = EncodeDifferenceLowerThan(a, b, 0);
const RelationStatus status =
best_root_level_bounds_->GetLevelZeroStatus(expr, kMinIntegerValue, ub);
if (status != RelationStatus::IS_UNKNOWN) return;
@@ -1683,7 +1765,7 @@ void ReifiedLinear2Bounds::AddReifiedPrecedenceIfNonTrivial(
LiteralIndex ReifiedLinear2Bounds::GetReifiedPrecedence(AffineExpression a,
AffineExpression b) {
const auto [expr, ub] = FromDifference(a, b);
const auto [expr, ub] = EncodeDifferenceLowerThan(a, b, 0);
const RelationStatus status =
best_root_level_bounds_->GetLevelZeroStatus(expr, kMinIntegerValue, ub);
if (status == RelationStatus::IS_TRUE) {
@@ -1872,10 +1954,15 @@ void Linear2Bounds::AddReasonForUpperBoundLowerThan(
LinearExpression2 expr, IntegerValue ub,
std::vector<Literal>* literal_reason,
std::vector<IntegerLiteral>* integer_reason) const {
expr.SimpleCanonicalization();
const IntegerValue gcd = expr.DivideByGcd();
ub = FloorRatio(ub, gcd);
DCHECK_LE(UpperBound(expr), ub);
if (root_level_bounds_->LevelZeroUpperBound(expr) <= ub) {
return;
}
if (enforced_bounds_->UpperBound(expr) <= ub) {
if (enforced_bounds_->GetUpperBoundFromEnforced(expr) <= ub) {
enforced_bounds_->AddReasonForUpperBoundLowerThan(expr, ub, literal_reason,
integer_reason);
} else {

114
ortools/sat/precedences.h
View File

@@ -45,12 +45,8 @@
namespace operations_research {
namespace sat {
struct FullIntegerPrecedence {
IntegerVariable var;
std::vector<int> indices;
std::vector<IntegerValue> offsets;
};
// This holds all the relation lhs <= linear2 <= rhs that are true at level
// zero. It is the source of truth across all the solver for such bounds.
class RootLevelLinear2Bounds {
public:
explicit RootLevelLinear2Bounds(Model* model)
@@ -75,17 +71,27 @@ class RootLevelLinear2Bounds {
int64_t num_bounds() const { return root_level_relations_.num_bounds(); }
// Return a list of (expr <= ub) sorted by expr.
// Return a list of (expr <= ub) sorted by expr. They are guaranteed to be
// better than the trivial upper bound.
std::vector<std::pair<LinearExpression2, IntegerValue>>
GetSortedNonTrivialUpperBounds() const {
return root_level_relations_.GetSortedNonTrivialUpperBounds();
}
GetSortedNonTrivialUpperBounds() const;
// Return a list of (lb <= expr <= ub) sorted by expr.
// Return a list of (lb <= expr <= ub), with expr.vars[0] = var, where at
// least one of the bounds is non-trivial and the potential other non-trivial
// bound is tight.
//
// As the class name indicates, all bounds are level zero ones.
std::vector<std::tuple<LinearExpression2, IntegerValue, IntegerValue>>
GetSortedNonTrivialBounds() const {
return root_level_relations_.GetSortedNonTrivialBounds();
}
GetAllBoundsContainingVariable(IntegerVariable var) const;
// Return a list of (lb <= expr <= ub), with expr.vars = {var1, var2}, where
// at least one of the bounds is non-trivial and the potential other
// non-trivial bound is tight.
//
// As the class name indicates, all bounds are level zero ones.
std::vector<std::tuple<LinearExpression2, IntegerValue, IntegerValue>>
GetAllBoundsContainingVariables(IntegerVariable var1,
IntegerVariable var2) const;
// For a given variable `var`, return all variables `other` so that
// LinearExpression2(var, other, 1, 1) has a non trivial upper bound.
@@ -115,12 +121,39 @@ class RootLevelLinear2Bounds {
util_intops::StrongVector<IntegerVariable, std::vector<IntegerVariable>>
coeff_one_var_lookup_;
// TODO(user): use data structures that consume less memory. A single
// std::vector<LinearExpression2> and hash maps having the index as value
// could be enough.
absl::flat_hash_map<
IntegerVariable,
absl::InlinedVector<
std::tuple<LinearExpression2, IntegerValue, IntegerValue>, 2>>
var_to_bounds_;
// Map to implement GetAllBoundsContainingVariables().
absl::flat_hash_map<
std::pair<IntegerVariable, IntegerVariable>,
absl::InlinedVector<
std::tuple<LinearExpression2, IntegerValue, IntegerValue>, 1>>
var_pair_to_bounds_;
// Data structure to quickly update var_to_bounds_. Return the index where
// this linear expression appear in the vector for the first and second
// variable.
absl::flat_hash_map<LinearExpression2, std::pair<int, int>>
var_to_bounds_vector_index_;
absl::flat_hash_map<LinearExpression2, int> var_pair_to_bounds_vector_index_;
// TODO(user): Also push them to a global shared repository after
// remapping IntegerVariable to proto indices.
BestBinaryRelationBounds root_level_relations_;
int64_t num_updates_ = 0;
};
struct FullIntegerPrecedence {
IntegerVariable var;
std::vector<int> indices;
std::vector<IntegerValue> offsets;
};
// This class is used to compute the transitive closure of the level-zero
// precedence relations.
//
@@ -223,6 +256,9 @@ class EnforcedLinear2Bounds : public ReversibleInterface {
//
// This method currently ignores all linear2 expressions with any coefficient
// different from 1.
//
// TODO(user): Ideally this should be moved to a new class and maybe augmented
// with other kind of precedences.
struct PrecedenceData {
IntegerVariable var;
int index;
@@ -230,21 +266,6 @@ class EnforcedLinear2Bounds : public ReversibleInterface {
void CollectPrecedences(absl::Span<const IntegerVariable> vars,
std::vector<PrecedenceData>* output);
IntegerValue LevelZeroUpperBound(LinearExpression2 expr) const {
return root_level_bounds_->LevelZeroUpperBound(expr);
}
// Returns the maximum value for expr, and the reason for it (all
// true). Note that we always check LevelZeroUpperBound() so if it is better,
// the returned literal reason will be empty.
//
// We separate the two because usually the reason is only needed when we push,
// which happen less often, so we don't mind doing two hash lookups, and we
// really want to optimize the UpperBound() instead.
//
// NOTE: most users will want to call Linear2Bounds::UpperBound() instead.
IntegerValue UpperBound(LinearExpression2 expr) const;
// Low-level function that returns the upper bound if there is some enforced
// relations only. Otherwise always returns kMaxIntegerValue.
// `expr` must be canonicalized and gcd-reduced.
@@ -325,8 +346,7 @@ struct Relation {
}
};
// A repository of all the enforced linear constraints of size 1 or 2, and of
// all the non-enforced linear constraints of size 2.
// A repository of all the enforced linear constraints of size 1 or 2.
//
// TODO(user): This is not always needed, find a way to clean this once we
// don't need it.
@@ -344,25 +364,6 @@ class BinaryRelationRepository {
return lit_to_relations_[lit];
}
// Returns the indices of the non-enforced relations that contain the given
// (positive) variable.
absl::Span<const int> IndicesOfRelationsContaining(
IntegerVariable var) const {
if (var >= var_to_relations_.size()) return {};
return var_to_relations_[var];
}
// Returns the indices of the non-enforced relations that contain the given
// (positive) variables.
absl::Span<const int> IndicesOfRelationsBetween(IntegerVariable var1,
IntegerVariable var2) const {
if (var1 > var2) std::swap(var1, var2);
const std::pair<IntegerVariable, IntegerVariable> key(var1, var2);
const auto it = var_pair_to_relations_.find(key);
if (it == var_pair_to_relations_.end()) return {};
return it->second;
}
// Adds a conditional relation lit => expr \in [lhs, rhs] (one of the coeffs
// can be zero).
void Add(Literal lit, LinearExpression2 expr, IntegerValue lhs,
@@ -374,7 +375,7 @@ class BinaryRelationRepository {
// Builds the literal to relations mapping. This should be called once all the
// relations have been added.
void Build(const RootLevelLinear2Bounds* root_level_bounds);
void Build();
// Assuming level-zero bounds + any (var >= value) in the input map,
// fills "output" with a "propagated" set of bounds assuming lit is true (by
@@ -386,7 +387,8 @@ class BinaryRelationRepository {
// Important: by default this does not call output->clear() so we can take
// the max with already inferred bounds.
bool PropagateLocalBounds(
const IntegerTrail& integer_trail, Literal lit,
const IntegerTrail& integer_trail,
const RootLevelLinear2Bounds& root_level_bounds, Literal lit,
const absl::flat_hash_map<IntegerVariable, IntegerValue>& input,
absl::flat_hash_map<IntegerVariable, IntegerValue>* output) const;
@@ -395,10 +397,6 @@ class BinaryRelationRepository {
int num_enforced_relations_ = 0;
std::vector<Relation> relations_;
CompactVectorVector<LiteralIndex, int> lit_to_relations_;
CompactVectorVector<IntegerVariable, int> var_to_relations_;
absl::flat_hash_map<std::pair<IntegerVariable, IntegerVariable>,
std::vector<int>>
var_pair_to_relations_;
};
// Class that keeps the best upper bound for a*x + b*y by using all the linear3
@@ -485,10 +483,6 @@ class ReifiedLinear2Bounds {
LiteralIndex GetReifiedPrecedence(AffineExpression a, AffineExpression b);
private:
// Return the pair (a - b) <= rhs.
std::pair<LinearExpression2, IntegerValue> FromDifference(
const AffineExpression& a, const AffineExpression& b) const;
IntegerEncoder* integer_encoder_;
RootLevelLinear2Bounds* best_root_level_bounds_;

220
ortools/sat/precedences_test.cc
View File

@@ -40,6 +40,7 @@ namespace {
using ::google::protobuf::contrib::parse_proto::ParseTestProto;
using ::testing::ElementsAre;
using ::testing::FieldsAre;
using ::testing::IsEmpty;
using ::testing::UnorderedElementsAre;
@@ -64,7 +65,7 @@ std::vector<IntegerVariable> AddVariables(IntegerTrail* integer_trail) {
TEST(EnforcedLinear2BoundsTest, BasicAPI) {
Model model;
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
auto* lin2_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* root_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* precedence_builder =
model.GetOrCreate<TransitivePrecedencesEvaluator>();
const std::vector<IntegerVariable> vars = AddVariables(integer_trail);
@@ -72,41 +73,40 @@ TEST(EnforcedLinear2BoundsTest, BasicAPI) {
// Note that odd indices are for the negation.
IntegerVariable a(0), b(2), c(4), d(6);
EnforcedLinear2Bounds precedences(&model);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(a, b), -10);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(d, c), -7);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(b, d), -5);
root_bounds->AddUpperBound(LinearExpression2::Difference(a, b), -10);
root_bounds->AddUpperBound(LinearExpression2::Difference(d, c), -7);
root_bounds->AddUpperBound(LinearExpression2::Difference(b, d), -5);
precedence_builder->Build();
EXPECT_EQ(
precedences.LevelZeroUpperBound(LinearExpression2::Difference(a, b)),
root_bounds->LevelZeroUpperBound(LinearExpression2::Difference(a, b)),
-10);
EXPECT_EQ(precedences.LevelZeroUpperBound(
EXPECT_EQ(root_bounds->LevelZeroUpperBound(
LinearExpression2::Difference(NegationOf(b), NegationOf(a))),
-10);
EXPECT_EQ(
precedences.LevelZeroUpperBound(LinearExpression2::Difference(a, c)),
root_bounds->LevelZeroUpperBound(LinearExpression2::Difference(a, c)),
-22);
EXPECT_EQ(precedences.LevelZeroUpperBound(
EXPECT_EQ(root_bounds->LevelZeroUpperBound(
LinearExpression2::Difference(NegationOf(c), NegationOf(a))),
-22);
EXPECT_EQ(
precedences.LevelZeroUpperBound(LinearExpression2::Difference(a, d)),
root_bounds->LevelZeroUpperBound(LinearExpression2::Difference(a, d)),
-15);
EXPECT_EQ(precedences.LevelZeroUpperBound(
EXPECT_EQ(root_bounds->LevelZeroUpperBound(
LinearExpression2::Difference(NegationOf(d), NegationOf(a))),
-15);
EXPECT_EQ(
precedences.LevelZeroUpperBound(LinearExpression2::Difference(d, a)),
root_bounds->LevelZeroUpperBound(LinearExpression2::Difference(d, a)),
100);
// Once built, we can update the offsets.
// Note however that this would not propagate through the precedence graphs.
lin2_bounds->AddUpperBound(LinearExpression2::Difference(a, b), -15);
root_bounds->AddUpperBound(LinearExpression2::Difference(a, b), -15);
EXPECT_EQ(
precedences.LevelZeroUpperBound(LinearExpression2::Difference(a, b)),
root_bounds->LevelZeroUpperBound(LinearExpression2::Difference(a, b)),
-15);
EXPECT_EQ(precedences.LevelZeroUpperBound(
EXPECT_EQ(root_bounds->LevelZeroUpperBound(
LinearExpression2::Difference(NegationOf(b), NegationOf(a))),
-15);
}
@@ -114,7 +114,7 @@ TEST(EnforcedLinear2BoundsTest, BasicAPI) {
TEST(EnforcedLinear2BoundsTest, CornerCase1) {
Model model;
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
auto* lin2_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* root_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* precedence_builder =
model.GetOrCreate<TransitivePrecedencesEvaluator>();
const std::vector<IntegerVariable> vars = AddVariables(integer_trail);
@@ -122,21 +122,20 @@ TEST(EnforcedLinear2BoundsTest, CornerCase1) {
// Note that odd indices are for the negation.
IntegerVariable a(0), b(2), c(4), d(6);
EnforcedLinear2Bounds precedences(&model);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(a, b), -10);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(b, c), -7);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(b, d), -5);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(NegationOf(b), a),
root_bounds->AddUpperBound(LinearExpression2::Difference(a, b), -10);
root_bounds->AddUpperBound(LinearExpression2::Difference(b, c), -7);
root_bounds->AddUpperBound(LinearExpression2::Difference(b, d), -5);
root_bounds->AddUpperBound(LinearExpression2::Difference(NegationOf(b), a),
-5);
precedence_builder->Build();
EXPECT_EQ(precedences.LevelZeroUpperBound(
EXPECT_EQ(root_bounds->LevelZeroUpperBound(
LinearExpression2::Difference(NegationOf(b), a)),
-5);
EXPECT_EQ(precedences.LevelZeroUpperBound(
EXPECT_EQ(root_bounds->LevelZeroUpperBound(
LinearExpression2::Difference(NegationOf(b), c)),
-22);
EXPECT_EQ(precedences.LevelZeroUpperBound(
EXPECT_EQ(root_bounds->LevelZeroUpperBound(
LinearExpression2::Difference(NegationOf(b), d)),
-20);
}
@@ -144,7 +143,7 @@ TEST(EnforcedLinear2BoundsTest, CornerCase1) {
TEST(EnforcedLinear2BoundsTest, CornerCase2) {
Model model;
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
auto* lin2_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* root_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* precedence_builder =
model.GetOrCreate<TransitivePrecedencesEvaluator>();
const std::vector<IntegerVariable> vars = AddVariables(integer_trail);
@@ -152,13 +151,12 @@ TEST(EnforcedLinear2BoundsTest, CornerCase2) {
// Note that odd indices are for the negation.
IntegerVariable a(0), b(2), c(4), d(6);
EnforcedLinear2Bounds precedences(&model);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(NegationOf(a), a),
root_bounds->AddUpperBound(LinearExpression2::Difference(NegationOf(a), a),
-10);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(a, b), -7);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(a, c), -5);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(a, d), -2);
EXPECT_EQ(precedences.LevelZeroUpperBound(
root_bounds->AddUpperBound(LinearExpression2::Difference(a, b), -7);
root_bounds->AddUpperBound(LinearExpression2::Difference(a, c), -5);
root_bounds->AddUpperBound(LinearExpression2::Difference(a, d), -2);
EXPECT_EQ(root_bounds->LevelZeroUpperBound(
LinearExpression2::Difference(NegationOf(b), NegationOf(a))),
-7);
@@ -168,7 +166,7 @@ TEST(EnforcedLinear2BoundsTest, CornerCase2) {
TEST(EnforcedLinear2BoundsTest, CoefficientGreaterThanOne) {
Model model;
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
auto* lin2_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* root_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* precedence_builder =
model.GetOrCreate<TransitivePrecedencesEvaluator>();
const std::vector<IntegerVariable> vars = AddVariables(integer_trail);
@@ -177,10 +175,10 @@ TEST(EnforcedLinear2BoundsTest, CoefficientGreaterThanOne) {
IntegerVariable a(0), b(2), c(4);
EnforcedLinear2Bounds precedences(&model);
lin2_bounds->AddUpperBound(LinearExpression2(a, b, 3, -4), 7);
lin2_bounds->AddUpperBound(LinearExpression2(a, c, 2, -3), -5);
lin2_bounds->AddUpperBound(LinearExpression2(a, b, 6, -8), 5);
EXPECT_EQ(precedences.LevelZeroUpperBound(LinearExpression2(a, b, 9, -12)),
root_bounds->AddUpperBound(LinearExpression2(a, b, 3, -4), 7);
root_bounds->AddUpperBound(LinearExpression2(a, c, 2, -3), -5);
root_bounds->AddUpperBound(LinearExpression2(a, b, 6, -8), 5);
EXPECT_EQ(root_bounds->LevelZeroUpperBound(LinearExpression2(a, b, 9, -12)),
6);
precedence_builder->Build();
@@ -189,7 +187,9 @@ TEST(EnforcedLinear2BoundsTest, CoefficientGreaterThanOne) {
TEST(EnforcedLinear2BoundsTest, ConditionalRelations) {
Model model;
auto* sat_solver = model.GetOrCreate<SatSolver>();
auto* lin2_bounds = model.GetOrCreate<Linear2Bounds>();
auto* integer_trail = model.GetOrCreate<IntegerTrail>();
auto* precedences = model.GetOrCreate<EnforcedLinear2Bounds>();
const std::vector<IntegerVariable> vars = AddVariables(integer_trail);
const Literal l(model.Add(NewBooleanVariable()), true);
@@ -197,17 +197,16 @@ TEST(EnforcedLinear2BoundsTest, ConditionalRelations) {
// Note that odd indices are for the negation.
IntegerVariable a(0), b(2);
EnforcedLinear2Bounds precedences(&model);
precedences.PushConditionalRelation({l}, LinearExpression2(a, b, 1, 1), 15);
precedences.PushConditionalRelation({l}, LinearExpression2(a, b, 1, 1), 20);
precedences->PushConditionalRelation({l}, LinearExpression2(a, b, 1, 1), 15);
precedences->PushConditionalRelation({l}, LinearExpression2(a, b, 1, 1), 20);
// We only keep the best one.
EXPECT_EQ(
precedences.UpperBound(LinearExpression2::Difference(a, NegationOf(b))),
lin2_bounds->UpperBound(LinearExpression2::Difference(a, NegationOf(b))),
15);
std::vector<Literal> literal_reason;
std::vector<IntegerLiteral> integer_reason;
precedences.AddReasonForUpperBoundLowerThan(
precedences->AddReasonForUpperBoundLowerThan(
LinearExpression2::Difference(a, NegationOf(b)), 15, &literal_reason,
&integer_reason);
EXPECT_THAT(literal_reason, ElementsAre(l.Negated()));
@@ -215,11 +214,11 @@ TEST(EnforcedLinear2BoundsTest, ConditionalRelations) {
// Backtrack works.
EXPECT_TRUE(sat_solver->ResetToLevelZero());
EXPECT_EQ(
precedences.UpperBound(LinearExpression2::Difference(a, NegationOf(b))),
lin2_bounds->UpperBound(LinearExpression2::Difference(a, NegationOf(b))),
200);
literal_reason.clear();
integer_reason.clear();
precedences.AddReasonForUpperBoundLowerThan(
precedences->AddReasonForUpperBoundLowerThan(
LinearExpression2::Difference(a, NegationOf(b)), kMaxIntegerValue,
&literal_reason, &integer_reason);
EXPECT_THAT(literal_reason, IsEmpty());
@@ -492,20 +491,20 @@ TEST(EnforcedLinear2BoundsTest, CollectPrecedences) {
Model model;
auto* integer_trail = model.GetOrCreate<IntegerTrail>();
auto* relations = model.GetOrCreate<EnforcedLinear2Bounds>();
auto* lin2_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
auto* root_bounds = model.GetOrCreate<RootLevelLinear2Bounds>();
std::vector<IntegerVariable> vars = AddVariables(integer_trail);
lin2_bounds->AddUpperBound(LinearExpression2::Difference(vars[0], vars[2]),
root_bounds->AddUpperBound(LinearExpression2::Difference(vars[0], vars[2]),
IntegerValue(-1));
lin2_bounds->AddUpperBound(LinearExpression2::Difference(vars[0], vars[5]),
root_bounds->AddUpperBound(LinearExpression2::Difference(vars[0], vars[5]),
IntegerValue(-1));
lin2_bounds->AddUpperBound(LinearExpression2::Difference(vars[1], vars[2]),
root_bounds->AddUpperBound(LinearExpression2::Difference(vars[1], vars[2]),
IntegerValue(-1));
lin2_bounds->AddUpperBound(LinearExpression2::Difference(vars[2], vars[4]),
root_bounds->AddUpperBound(LinearExpression2::Difference(vars[2], vars[4]),
IntegerValue(-1));
lin2_bounds->AddUpperBound(LinearExpression2::Difference(vars[3], vars[4]),
root_bounds->AddUpperBound(LinearExpression2::Difference(vars[3], vars[4]),
IntegerValue(-1));
lin2_bounds->AddUpperBound(LinearExpression2::Difference(vars[4], vars[5]),
root_bounds->AddUpperBound(LinearExpression2::Difference(vars[4], vars[5]),
IntegerValue(-1));
std::vector<EnforcedLinear2Bounds::PrecedenceData> p;
@@ -543,7 +542,7 @@ TEST(BinaryRelationRepositoryTest, Build) {
root_level_bounds->Add(LinearExpression2(x, y, 3, -1), 5, 15);
root_level_bounds->Add(LinearExpression2::Difference(x, z), 0, 10);
repository.AddPartialRelation(lit_b, x, z);
repository.Build(root_level_bounds);
repository.Build();
auto get_rel = [&](absl::Span<const int> indexes) {
std::vector<Relation> result;
@@ -558,12 +557,6 @@ TEST(BinaryRelationRepositoryTest, Build) {
get_rel(all),
UnorderedElementsAre(
Relation{lit_a, LinearExpression2(x, y, -1, 1), 2, 8},
Relation{Literal(kNoLiteralIndex), LinearExpression2(x, y, 1, -1), 0,
5},
Relation{Literal(kNoLiteralIndex), LinearExpression2(x, y, 3, -1), 5,
15},
Relation{Literal(kNoLiteralIndex), LinearExpression2(x, z, 1, -1), 0,
10},
Relation{lit_a, LinearExpression2(x, y, -3, -2), 1, 15},
Relation{lit_b, LinearExpression2(kNoIntegerVariable, x, 0, -3), 3,
5},
@@ -578,41 +571,32 @@ TEST(BinaryRelationRepositoryTest, Build) {
Relation{lit_b, LinearExpression2(kNoIntegerVariable, x, 0, -3), 3,
5},
Relation{lit_b, LinearExpression2(x, z, 1, 1), 0, 0}));
EXPECT_THAT(root_level_bounds->GetAllBoundsContainingVariable(x),
UnorderedElementsAre(
FieldsAre(LinearExpression2(x, NegationOf(y), 1, 1), 0, 5),
FieldsAre(LinearExpression2(x, NegationOf(y), 3, 1), 5, 15),
FieldsAre(LinearExpression2(x, NegationOf(z), 1, 1), 0, 10)));
EXPECT_THAT(
get_rel(repository.IndicesOfRelationsContaining(x)),
UnorderedElementsAre(Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, y, 1, -1), 0, 5},
Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, y, 3, -1), 5, 15},
Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, z, 1, -1), 0, 10}));
root_level_bounds->GetAllBoundsContainingVariable(y),
UnorderedElementsAre(FieldsAre(LinearExpression2(y, x, -1, 1), 0, 5),
FieldsAre(LinearExpression2(y, x, -1, 3), 5, 15)));
EXPECT_THAT(
get_rel(repository.IndicesOfRelationsContaining(y)),
UnorderedElementsAre(Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, y, 1, -1), 0, 5},
Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, y, 3, -1), 5, 15}));
root_level_bounds->GetAllBoundsContainingVariable(z),
UnorderedElementsAre(FieldsAre(LinearExpression2(z, x, -1, 1), 0, 10)));
EXPECT_THAT(
get_rel(repository.IndicesOfRelationsContaining(z)),
UnorderedElementsAre(Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, z, 1, -1), 0, 10}));
root_level_bounds->GetAllBoundsContainingVariables(x, y),
UnorderedElementsAre(FieldsAre(LinearExpression2(x, y, 1, -1), 0, 5),
FieldsAre(LinearExpression2(x, y, 3, -1), 5, 15)));
EXPECT_THAT(
get_rel(repository.IndicesOfRelationsBetween(x, y)),
UnorderedElementsAre(Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, y, 1, -1), 0, 5},
Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, y, 3, -1), 5, 15}));
root_level_bounds->GetAllBoundsContainingVariables(y, x),
UnorderedElementsAre(FieldsAre(LinearExpression2(y, x, -1, 1), 0, 5),
FieldsAre(LinearExpression2(y, x, -1, 3), 5, 15)));
EXPECT_THAT(
get_rel(repository.IndicesOfRelationsBetween(y, x)),
UnorderedElementsAre(Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, y, 1, -1), 0, 5},
Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, y, 3, -1), 5, 15}));
EXPECT_THAT(
get_rel(repository.IndicesOfRelationsBetween(x, z)),
UnorderedElementsAre(Relation{Literal(kNoLiteralIndex),
LinearExpression2(x, z, 1, -1), 0, 10}));
EXPECT_THAT(repository.IndicesOfRelationsBetween(z, y), IsEmpty());
root_level_bounds->GetAllBoundsContainingVariables(x, z),
UnorderedElementsAre(FieldsAre(LinearExpression2(x, z, 1, -1), 0, 10)));
EXPECT_THAT(root_level_bounds->GetAllBoundsContainingVariables(z, y),
IsEmpty());
}
std::vector<Relation> GetRelations(Model& model) {
@@ -683,20 +667,16 @@ TEST(BinaryRelationRepositoryTest, LoadCpModelAddUnaryAndBinaryRelations) {
LoadCpModel(model_proto, &model);
const CpModelMapping& mapping = *model.GetOrCreate<CpModelMapping>();
EXPECT_THAT(GetRelations(model),
UnorderedElementsAre(
Relation{mapping.Literal(0),
LinearExpression2::Difference(mapping.Integer(2),
mapping.Integer(3)),
0, 10},
Relation{mapping.Literal(1),
LinearExpression2(kNoIntegerVariable,
mapping.Integer(2), 0, 1),
5, 10},
Relation{Literal(kNoLiteralIndex),
LinearExpression2(mapping.Integer(2),
mapping.Integer(3), 3, -2),
-10, 10}));
EXPECT_THAT(
GetRelations(model),
UnorderedElementsAre(Relation{mapping.Literal(0),
LinearExpression2::Difference(
mapping.Integer(2), mapping.Integer(3)),
0, 10},
Relation{mapping.Literal(1),
LinearExpression2(kNoIntegerVariable,
mapping.Integer(2), 0, 1),
5, 10}));
}
TEST(BinaryRelationRepositoryTest,
@@ -861,13 +841,13 @@ TEST(BinaryRelationRepositoryTest, PropagateLocalBounds_EnforcedRelation) {
model.GetOrCreate<RootLevelLinear2Bounds>();
repository.Add(lit_a, LinearExpression2::Difference(y, x), 2,
10); // lit_a => y => x + 2
repository.Build(root_level_bounds);
repository.Build();
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
absl::flat_hash_map<IntegerVariable, IntegerValue> input = {{x, 3}};
absl::flat_hash_map<IntegerVariable, IntegerValue> output;
const bool result =
repository.PropagateLocalBounds(*integer_trail, lit_a, input, &output);
const bool result = repository.PropagateLocalBounds(
*integer_trail, *root_level_bounds, lit_a, input, &output);
EXPECT_TRUE(result);
EXPECT_THAT(output, UnorderedElementsAre(std::make_pair(NegationOf(x), -8),
@@ -886,13 +866,13 @@ TEST(BinaryRelationRepositoryTest, PropagateLocalBounds_UnenforcedRelation) {
10); // lit_a => y => x - 5
root_level_bounds->Add(LinearExpression2(x, y, -1, 1), 2,
10); // y => x + 2
repository.Build(root_level_bounds);
repository.Build();
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
absl::flat_hash_map<IntegerVariable, IntegerValue> input = {{x, 3}};
absl::flat_hash_map<IntegerVariable, IntegerValue> output;
const bool result =
repository.PropagateLocalBounds(*integer_trail, lit_a, input, &output);
const bool result = repository.PropagateLocalBounds(
*integer_trail, *root_level_bounds, lit_a, input, &output);
EXPECT_TRUE(result);
EXPECT_THAT(output, UnorderedElementsAre(std::make_pair(NegationOf(x), -98),
@@ -913,13 +893,13 @@ TEST(BinaryRelationRepositoryTest,
10); // lit_a => y => x - 5
repository.Add(lit_b, LinearExpression2::Difference(y, x), 2,
10); // lit_b => y => x + 2
repository.Build(root_level_bounds);
repository.Build();
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
absl::flat_hash_map<IntegerVariable, IntegerValue> input = {{x, 3}};
absl::flat_hash_map<IntegerVariable, IntegerValue> output;
const bool result =
repository.PropagateLocalBounds(*integer_trail, lit_a, input, &output);
const bool result = repository.PropagateLocalBounds(
*integer_trail, *root_level_bounds, lit_a, input, &output);
EXPECT_TRUE(result);
EXPECT_THAT(output, IsEmpty());
@@ -936,13 +916,13 @@ TEST(BinaryRelationRepositoryTest,
model.GetOrCreate<RootLevelLinear2Bounds>();
repository.Add(lit_a, LinearExpression2::Difference(y, x), 2,
10); // lit_a => y => x + 2
repository.Build(root_level_bounds);
repository.Build();
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
absl::flat_hash_map<IntegerVariable, IntegerValue> input = {{x, 3}};
absl::flat_hash_map<IntegerVariable, IntegerValue> output = {{y, 8}};
const bool result =
repository.PropagateLocalBounds(*integer_trail, lit_a, input, &output);
const bool result = repository.PropagateLocalBounds(
*integer_trail, *root_level_bounds, lit_a, input, &output);
EXPECT_TRUE(result);
EXPECT_THAT(output, UnorderedElementsAre(std::make_pair(NegationOf(x), -8),
@@ -959,13 +939,13 @@ TEST(BinaryRelationRepositoryTest, PropagateLocalBounds_Infeasible) {
model.GetOrCreate<RootLevelLinear2Bounds>();
repository.Add(lit_a, LinearExpression2::Difference(y, x), 8,
10); // lit_a => y => x + 8
repository.Build(root_level_bounds);
repository.Build();
IntegerTrail* integer_trail = model.GetOrCreate<IntegerTrail>();
absl::flat_hash_map<IntegerVariable, IntegerValue> input = {{x, 3}};
absl::flat_hash_map<IntegerVariable, IntegerValue> output;
const bool result =
repository.PropagateLocalBounds(*integer_trail, lit_a, input, &output);
const bool result = repository.PropagateLocalBounds(
*integer_trail, *root_level_bounds, lit_a, input, &output);
EXPECT_FALSE(result);
EXPECT_THAT(output, UnorderedElementsAre(std::make_pair(NegationOf(x), -2),
@@ -984,15 +964,13 @@ TEST(GreaterThanAtLeastOneOfDetectorTest, AddGreaterThanAtLeastOneOf) {
model.Add(ClauseConstraint({lit_a, lit_b, lit_c}));
auto* repository = model.GetOrCreate<BinaryRelationRepository>();
RootLevelLinear2Bounds* root_level_bounds =
model.GetOrCreate<RootLevelLinear2Bounds>();
repository->Add(lit_a, LinearExpression2::Difference(d, a), 2,
1000); // d >= a + 2
repository->Add(lit_b, LinearExpression2::Difference(d, b), -1,
1000); // d >= b -1
repository->Add(lit_c, LinearExpression2::Difference(d, c), 0,
1000); // d >= c
repository->Build(root_level_bounds);
repository->Build();
auto* detector = model.GetOrCreate<GreaterThanAtLeastOneOfDetector>();
auto* solver = model.GetOrCreate<SatSolver>();
@@ -1017,14 +995,12 @@ TEST(GreaterThanAtLeastOneOfDetectorTest,
model.Add(ClauseConstraint({lit_a, lit_b, lit_c}));
auto* repository = model.GetOrCreate<BinaryRelationRepository>();
RootLevelLinear2Bounds* root_level_bounds =
model.GetOrCreate<RootLevelLinear2Bounds>();
repository->Add(lit_a, LinearExpression2(a, d, -1, 1), 2,
1000); // d >= a + 2
repository->Add(lit_b, LinearExpression2(b, d, -1, 1), -1,
1000); // d >= b -1
repository->Add(lit_c, LinearExpression2(c, d, -1, 1), 0, 1000); // d >= c
repository->Build(root_level_bounds);
repository->Build();
auto* detector = model.GetOrCreate<GreaterThanAtLeastOneOfDetector>();
auto* solver = model.GetOrCreate<SatSolver>();

33
ortools/sat/routing_cuts.cc
View File

@@ -124,6 +124,7 @@ MinOutgoingFlowHelper::MinOutgoingFlowHelper(
trail_(*model->GetOrCreate<Trail>()),
integer_trail_(*model->GetOrCreate<IntegerTrail>()),
integer_encoder_(*model->GetOrCreate<IntegerEncoder>()),
root_level_bounds_(*model->GetOrCreate<RootLevelLinear2Bounds>()),
shared_stats_(model->GetOrCreate<SharedStatistics>()),
in_subset_(num_nodes, false),
index_in_subset_(num_nodes, -1),
@@ -629,7 +630,8 @@ int MinOutgoingFlowHelper::ComputeMinOutgoingFlow(
// If this arc cannot be taken skip.
tmp_lbs.clear();
if (!binary_relation_repository_.PropagateLocalBounds(
integer_trail_, lit, node_var_lower_bounds_[tail], &tmp_lbs)) {
integer_trail_, root_level_bounds_, lit,
node_var_lower_bounds_[tail], &tmp_lbs)) {
continue;
}
@@ -755,8 +757,8 @@ int MinOutgoingFlowHelper::ComputeTightMinOutgoingFlow(
// If this arc cannot be taken skip.
tmp_lbs.clear();
if (!binary_relation_repository_.PropagateLocalBounds(
integer_trail_, literals_[outgoing_arc_index], path_bounds,
&tmp_lbs)) {
integer_trail_, root_level_bounds_,
literals_[outgoing_arc_index], path_bounds, &tmp_lbs)) {
continue;
}
@@ -916,7 +918,7 @@ bool MinOutgoingFlowHelper::SubsetMightBeServedWithKRoutes(
absl::flat_hash_map<IntegerVariable, IntegerValue> copy = state.lbs;
return binary_relation_repository_.PropagateLocalBounds(
integer_trail_, unique_lit, copy, &state.lbs);
integer_trail_, root_level_bounds_, unique_lit, copy, &state.lbs);
};
// We always start with the first node in this case.
@@ -1011,7 +1013,8 @@ bool MinOutgoingFlowHelper::SubsetMightBeServedWithKRoutes(
}
} else {
if (!binary_relation_repository_.PropagateLocalBounds(
integer_trail_, literal, from_state.lbs, &to_state.lbs)) {
integer_trail_, root_level_bounds_, literal, from_state.lbs,
&to_state.lbs)) {
continue;
}
}
@@ -1409,6 +1412,8 @@ class RouteRelationsBuilder {
const auto& integer_encoder = *model->GetOrCreate<IntegerEncoder>();
const auto& trail = *model->GetOrCreate<Trail>();
const auto& integer_trail = *model->GetOrCreate<IntegerTrail>();
const auto& root_level_bounds =
*model->GetOrCreate<RootLevelLinear2Bounds>();
DCHECK_EQ(trail.CurrentDecisionLevel(), 0);
flat_arc_dim_relations_ = std::vector<HeadMinusTailBounds>(
@@ -1532,13 +1537,12 @@ class RouteRelationsBuilder {
// Check if we can use non-enforced relations to improve the relations.
if (!tail_expr.IsEmpty() && !head_expr.IsEmpty()) {
for (const int relation_index :
binary_relation_repository_.IndicesOfRelationsBetween(
for (const auto& [expr, lb, ub] :
root_level_bounds.GetAllBoundsContainingVariables(
tail_expr.var, head_expr.var)) {
ComputeArcRelation(
i, dimension, tail_expr, head_expr,
binary_relation_repository_.relation(relation_index),
integer_trail);
ComputeArcRelation(i, dimension, tail_expr, head_expr,
Relation{Literal(kNoLiteralIndex), expr, lb, ub},
integer_trail);
}
}
@@ -1858,7 +1862,7 @@ BinaryRelationRepository ComputePartialBinaryRelationRepository(
ToPositiveIntegerVariable(vars[1]));
}
Model empty_model;
repository.Build(empty_model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
return repository;
}
@@ -1945,6 +1949,7 @@ class RoutingCutHelper {
*model->GetOrCreate<BinaryRelationRepository>()),
random_(model->GetOrCreate<ModelRandomGenerator>()),
encoder_(model->GetOrCreate<IntegerEncoder>()),
root_level_bounds_(*model->GetOrCreate<RootLevelLinear2Bounds>()),
in_subset_(num_nodes, false),
self_arc_literal_(num_nodes_),
self_arc_lp_value_(num_nodes_),
@@ -2078,6 +2083,7 @@ class RoutingCutHelper {
const BinaryRelationRepository& binary_relation_repository_;
ModelRandomGenerator* random_;
IntegerEncoder* encoder_;
const RootLevelLinear2Bounds& root_level_bounds_;
std::vector<bool> in_subset_;
@@ -2783,7 +2789,8 @@ void RoutingCutHelper::GenerateCutsForInfeasiblePaths(
const Literal next_literal = literals_[arc_index];
next_state.bounds = state.bounds;
if (binary_relation_repository_.PropagateLocalBounds(
integer_trail_, next_literal, state.bounds, &next_state.bounds)) {
integer_trail_, root_level_bounds_, next_literal, state.bounds,
&next_state.bounds)) {
// Do not explore "long" paths to keep the search time bounded.
if (path_length < max_path_length) {
path_nodes[next_state.last_node] = true;

1
ortools/sat/routing_cuts.h
View File

@@ -545,6 +545,7 @@ class MinOutgoingFlowHelper {
const Trail& trail_;
const IntegerTrail& integer_trail_;
const IntegerEncoder& integer_encoder_;
const RootLevelLinear2Bounds& root_level_bounds_;
SharedStatistics* shared_stats_;
// Temporary data used by ComputeMinOutgoingFlow(). Always contain default

52
ortools/sat/routing_cuts_test.cc
View File

@@ -164,7 +164,7 @@ TEST(MinOutgoingFlowHelperTest, CapacityConstraints) {
repository->Add(literal, LinearExpression2(loads[head], loads[tail], 1, -1),
head_load, 1000);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
// Subject under test.
MinOutgoingFlowHelper helper(num_nodes, tails, heads, literals, &model);
@@ -239,7 +239,7 @@ TEST_P(DimensionBasedMinOutgoingFlowHelperTest, BasicCapacities) {
demands[use_outgoing_load ? head : tail], 1000);
}
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, *repository);
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
@@ -312,7 +312,7 @@ TEST_P(DimensionBasedMinOutgoingFlowHelperTest,
demands[use_outgoing_load ? head : tail], 1000);
}
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, *repository);
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
@@ -362,7 +362,7 @@ TEST(MinOutgoingFlowHelperTest, NodeExpressionWithConstant) {
// Capacity constraint: (offset_load2 + offset) - load1 >= demand1
repository->Add(literals[0], LinearExpression2(offset_load2, load1, 1, -1),
demand1 - offset, 1000);
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
RouteRelationsHelper::Create(num_nodes, tails, heads, literals,
{AffineExpression(), AffineExpression(load1),
@@ -404,7 +404,7 @@ TEST(MinOutgoingFlowHelperTest, ConstantNodeExpression) {
repository->Add(literals[0],
LinearExpression2(kNoIntegerVariable, load1, 0, -1),
demand1 - load2, 1000);
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
RouteRelationsHelper::Create(num_nodes, tails, heads, literals,
{AffineExpression(), AffineExpression(load1),
@@ -461,7 +461,7 @@ TEST(MinOutgoingFlowHelperTest, NodeExpressionUsingArcLiteralAsVariable) {
// Capacity constraint: load3 - load2 >= demand2. This expands to
// (capacity - demand3) - (capacity - demand2 - demand3 * l) >= demand2 which,
// when l is 1, simplifies to 0 >= 0. Hence this constraint is ignored.
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
RouteRelationsHelper::Create(num_nodes, tails, heads, literals,
{AffineExpression(), AffineExpression(load1),
@@ -520,7 +520,7 @@ TEST(MinOutgoingFlowHelperTest,
// (capacity - demand3) - (capacity - demand2 - demand3 + demand3 * l) >=
// demand2 which, when l is 0, simplifies to 0 >= 0. Hence this constraint is
// ignored.
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
RouteRelationsHelper::Create(num_nodes, tails, heads, literals,
{AffineExpression(), AffineExpression(load1),
@@ -577,7 +577,7 @@ TEST(MinOutgoingFlowHelperTest, ArcNodeExpressionsWithSharedVariable) {
// Capacity constraint: load3 - load2 >= demand2. This expands to
// (capacity - demand3) - (capacity - demand2 - demand3) >= demand2, which
// simplifies to 0 >= 0. Hence this constraint is ignored.
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
RouteRelationsHelper::Create(
num_nodes, tails, heads, literals,
@@ -643,7 +643,7 @@ TEST(MinOutgoingFlowHelperTest, UnaryRelationForTwoNodeExpressions) {
// demand1 * x >= capacity
repository->Add(literals[1], LinearExpression2(load3, x, 1, demand1),
capacity, 1000);
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
RouteRelationsHelper::Create(num_nodes, tails, heads, literals,
{AffineExpression(), AffineExpression(load1),
@@ -700,7 +700,7 @@ TEST(MinOutgoingFlowHelperTest, NodeMustBeInnerNode) {
LinearExpression2(loads[heads[i]], loads[tails[i]], 1, -1),
demands[i], 1000);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, *repository);
@@ -760,7 +760,7 @@ TEST(MinOutgoingFlowHelperTest, BetterUseOfUpperBound) {
LinearExpression2::Difference(loads[heads[i]], loads[tails[i]]),
demands[i], 1000);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
loads.size(), tails, heads, literals, *repository);
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
@@ -799,7 +799,7 @@ TEST(MinOutgoingFlowHelperTest, DimensionBasedMinOutgoingFlow_IsolatedNodes) {
LinearExpression2(variables[head], variables[0], 1, -1), 1,
100);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, *repository);
std::unique_ptr<RouteRelationsHelper> route_relations_helper =
@@ -850,7 +850,7 @@ TEST(MinOutgoingFlowHelperTest, TimeWindows) {
repository->Add(literal, LinearExpression2(times[head], times[tail], 1, -1),
travel_time, 1000);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
// Subject under test.
MinOutgoingFlowHelper helper(num_nodes, tails, heads, literals, &model);
@@ -985,7 +985,7 @@ TEST(MinOutgoingFlowHelperTest, SubsetMightBeServedWithKRoutes) {
LinearExpression2(cumul_vars_2[head], cumul_vars_2[tail], 1, -1),
load2[head], 10000);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
const int optimal = SolveTwoDimensionBinPacking(capacity, load1, load2);
EXPECT_EQ(optimal, 2);
@@ -1057,7 +1057,7 @@ TEST(MinOutgoingFlowHelperTest, SubsetMightBeServedWithKRoutesRandom) {
LinearExpression2::Difference(cumul_vars_2[head], cumul_vars_2[tail]),
load2[head], 10000);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
// To check our indices mapping, lets remove a random nodes from the subset
std::vector<int> subset;
@@ -1186,7 +1186,7 @@ TEST(MinOutgoingFlowHelperTest,
LinearExpression2::Difference(cumul_vars[head], cumul_vars[tail]),
travel_times[arc], 10000);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
// Serve everyone but the depot.
std::vector<int> subset;
@@ -1420,7 +1420,7 @@ TEST(RouteRelationsHelperTest, Basic) {
repository.Add(literals[2], LinearExpression2(w, v, -1, 1), -100, -3);
repository.Add(literals[3], LinearExpression2::Difference(x, w), 5, 100);
repository.Add(literals[4], LinearExpression2::Difference(z, y), 7, 100);
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, repository);
@@ -1515,7 +1515,7 @@ TEST(RouteRelationsHelperTest, UnenforcedRelations) {
bounds->Add(LinearExpression2(c, a, 3, -2), 1, 9);
bounds->Add(LinearExpression2(c, a, 1, -1), 5, 5);
bounds->Add(LinearExpression2(c, a, 2, -3), 3, 8);
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, repository);
@@ -1562,7 +1562,7 @@ TEST(RouteRelationsHelperTest, SeveralVariablesPerNode) {
// Weird relation linking time and load variables, causing all the variables
// to be in a single "dimension".
repository.Add(literals[0], LinearExpression2::Difference(x, a), 0, 100);
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, repository);
@@ -1588,7 +1588,7 @@ TEST(RouteRelationsHelperTest, ComplexVariableRelations) {
BinaryRelationRepository repository;
// "complex" relation with non +1/-1 coefficients.
repository.Add(literals[0], LinearExpression2(b, a, 10, 1), 0, 150);
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = {
.num_dimensions = 0,
@@ -1621,7 +1621,7 @@ TEST(RouteRelationsHelperTest, TwoUnaryRelationsPerArc) {
encoder.AssociateToIntegerEqualValue(literals[0], a, 20);
encoder.AssociateToIntegerLiteral(literals[0], {b, 50});
BinaryRelationRepository repository;
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = {
.num_dimensions = 0,
@@ -1655,7 +1655,7 @@ TEST(RouteRelationsHelperTest, SeveralRelationsPerArc) {
repository.Add(literals[1], LinearExpression2::Difference(c, b), 70, 1000);
// Add a second relation for some arc.
repository.Add(literals[1], LinearExpression2(c, b, 2, -3), 100, 200);
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, repository);
@@ -1689,7 +1689,7 @@ TEST(RouteRelationsHelperTest, SeveralArcsPerLiteral) {
BinaryRelationRepository repository;
repository.Add(literals[0], LinearExpression2::Difference(b, a), 50, 1000);
repository.Add(literals[0], LinearExpression2::Difference(c, b), 40, 1000);
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, repository);
@@ -1736,7 +1736,7 @@ TEST(RouteRelationsHelperTest, InconsistentRelationIsSkipped) {
repository.Add(literals[4], LinearExpression2::Difference(f, b), 4, 4);
// Inconsistent relation for arc 5->3 (should be between f and d).
repository.Add(literals[5], LinearExpression2(f, b, 2, -1), 5, 5);
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, repository);
@@ -1799,7 +1799,7 @@ TEST(RouteRelationsHelperTest, InconsistentRelationWithMultipleArcsPerLiteral) {
// be true at the same time, hence the crossed bounds below.
repository.Add(literals[4], LinearExpression2::Difference(e, d), 4, 4);
repository.Add(literals[5], LinearExpression2::Difference(e, d), 5, 5);
repository.Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository.Build();
const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions(
num_nodes, tails, heads, literals, repository);
@@ -2436,7 +2436,7 @@ TEST(CreateCVRPCutGeneratorTest, InfeasiblePathCuts) {
LinearExpression2(loads[head], loads[tail], 1, -1),
demands[tail], 10000);
}
repository->Build(model.GetOrCreate<RootLevelLinear2Bounds>());
repository->Build();
// Enable the cut generator.
model.GetOrCreate<SatParameters>()
->set_routing_cut_max_infeasible_path_length(10);

19
ortools/sat/scheduling_helpers.cc
View File

@@ -371,23 +371,8 @@ bool SchedulingConstraintHelper::NotifyLevelZeroPrecedence(int a, int b) {
CHECK(IsPresent(b));
CHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
// Convert before <= after to linear2 <= rhs.
LinearExpression2 expr;
IntegerValue rhs;
{
const AffineExpression before = ends_[a];
const AffineExpression after = starts_[b];
expr.vars[0] = before.var;
expr.coeffs[0] = before.coeff;
expr.vars[1] = after.var;
expr.coeffs[1] = -after.coeff;
rhs = after.constant - before.constant;
}
// Canonicalization.
expr.SimpleCanonicalization();
const IntegerValue gcd = expr.DivideByGcd();
rhs = FloorRatio(rhs, gcd);
// Convert ends_[a] <= starts[b] to linear2 <= rhs and canonicalize.
const auto [expr, rhs] = EncodeDifferenceLowerThan(ends_[a], starts_[b], 0);
// Trivial case.
if (expr.coeffs[0] == 0 && expr.coeffs[1] == 0) {