From d1c3c7f84b4cce37ce3f178bfcffca00a901937c Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 12 Jun 2025 11:11:26 +0200 Subject: [PATCH] [CP-SAT] more work on precedences --- ortools/sat/2d_distances_propagator.cc | 11 +- ortools/sat/cp_model_solver_helpers.cc | 2 +- ortools/sat/disjunctive.cc | 13 +- ortools/sat/integer_base.h | 18 ++ ortools/sat/precedences.cc | 239 +++++++++++++++++-------- ortools/sat/precedences.h | 114 ++++++------ ortools/sat/precedences_test.cc | 220 ++++++++++------------- ortools/sat/routing_cuts.cc | 33 ++-- ortools/sat/routing_cuts.h | 1 + ortools/sat/routing_cuts_test.cc | 52 +++--- ortools/sat/scheduling_helpers.cc | 19 +- 11 files changed, 393 insertions(+), 329 deletions(-) diff --git a/ortools/sat/2d_distances_propagator.cc b/ortools/sat/2d_distances_propagator.cc index e6d2658635..7cf521400f 100644 --- a/ortools/sat/2d_distances_propagator.cc +++ b/ortools/sat/2d_distances_propagator.cc @@ -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()); } } diff --git a/ortools/sat/cp_model_solver_helpers.cc b/ortools/sat/cp_model_solver_helpers.cc index 1be370ab37..083d657587 100644 --- a/ortools/sat/cp_model_solver_helpers.cc +++ b/ortools/sat/cp_model_solver_helpers.cc @@ -1155,7 +1155,7 @@ void FillBinaryRelationRepository(const CpModelProto& model_proto, } } } - repository->Build(root_level_lin2_bounds); + repository->Build(); } } // namespace diff --git a/ortools/sat/disjunctive.cc b/ortools/sat/disjunctive.cc index d92ae5ac59..fd4e6b4e58 100644 --- a/ortools/sat/disjunctive.cc +++ b/ortools/sat/disjunctive.cc @@ -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( diff --git a/ortools/sat/integer_base.h b/ortools/sat/integer_base.h index a148a91cf6..572f62a906 100644 --- a/ortools/sat/integer_base.h +++ b/ortools/sat/integer_base.h @@ -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 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 H AbslHashValue(H h, const LinearExpression2& e) { h = H::combine(std::move(h), e.vars[0]); diff --git a/ortools/sat/precedences.cc b/ortools/sat/precedences.cc index d7ffd981d8..2e2a5bcf47 100644 --- a/ortools/sat/precedences.cc +++ b/ortools/sat/precedences.cc @@ -57,6 +57,7 @@ namespace sat { std::pair 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 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 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& 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& 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> +RootLevelLinear2Bounds::GetSortedNonTrivialUpperBounds() const { + std::vector> 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> +RootLevelLinear2Bounds::GetAllBoundsContainingVariable( + IntegerVariable var) const { + std::vector> 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> +RootLevelLinear2Bounds::GetAllBoundsContainingVariables( + IntegerVariable var1, IntegerVariable var2) const { + std::vector> result; + std::pair 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> stats; @@ -244,7 +383,7 @@ void EnforcedLinear2Bounds::AddReasonForUpperBoundLowerThan( std::vector* literal_reason, std::vector* /*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> literal_key_values; - std::vector> 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 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& input, absl::flat_hash_map* 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 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_reason, std::vector* 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 { diff --git a/ortools/sat/precedences.h b/ortools/sat/precedences.h index cf192933a6..6b75d0b9d9 100644 --- a/ortools/sat/precedences.h +++ b/ortools/sat/precedences.h @@ -45,12 +45,8 @@ namespace operations_research { namespace sat { -struct FullIntegerPrecedence { - IntegerVariable var; - std::vector indices; - std::vector 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> - 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> - 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> + 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> coeff_one_var_lookup_; + // TODO(user): use data structures that consume less memory. A single + // std::vector and hash maps having the index as value + // could be enough. + absl::flat_hash_map< + IntegerVariable, + absl::InlinedVector< + std::tuple, 2>> + var_to_bounds_; + // Map to implement GetAllBoundsContainingVariables(). + absl::flat_hash_map< + std::pair, + absl::InlinedVector< + std::tuple, 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> + var_to_bounds_vector_index_; + absl::flat_hash_map 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 indices; + std::vector 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 vars, std::vector* 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 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 IndicesOfRelationsBetween(IntegerVariable var1, - IntegerVariable var2) const { - if (var1 > var2) std::swap(var1, var2); - const std::pair 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& input, absl::flat_hash_map* output) const; @@ -395,10 +397,6 @@ class BinaryRelationRepository { int num_enforced_relations_ = 0; std::vector relations_; CompactVectorVector lit_to_relations_; - CompactVectorVector var_to_relations_; - absl::flat_hash_map, - std::vector> - 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 FromDifference( - const AffineExpression& a, const AffineExpression& b) const; - IntegerEncoder* integer_encoder_; RootLevelLinear2Bounds* best_root_level_bounds_; diff --git a/ortools/sat/precedences_test.cc b/ortools/sat/precedences_test.cc index 0579923c9a..c9c9dbf993 100644 --- a/ortools/sat/precedences_test.cc +++ b/ortools/sat/precedences_test.cc @@ -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 AddVariables(IntegerTrail* integer_trail) { TEST(EnforcedLinear2BoundsTest, BasicAPI) { Model model; IntegerTrail* integer_trail = model.GetOrCreate(); - auto* lin2_bounds = model.GetOrCreate(); + auto* root_bounds = model.GetOrCreate(); auto* precedence_builder = model.GetOrCreate(); const std::vector 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(); - auto* lin2_bounds = model.GetOrCreate(); + auto* root_bounds = model.GetOrCreate(); auto* precedence_builder = model.GetOrCreate(); const std::vector 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(); - auto* lin2_bounds = model.GetOrCreate(); + auto* root_bounds = model.GetOrCreate(); auto* precedence_builder = model.GetOrCreate(); const std::vector 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(); - auto* lin2_bounds = model.GetOrCreate(); + auto* root_bounds = model.GetOrCreate(); auto* precedence_builder = model.GetOrCreate(); const std::vector 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(); + auto* lin2_bounds = model.GetOrCreate(); auto* integer_trail = model.GetOrCreate(); + auto* precedences = model.GetOrCreate(); const std::vector 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_reason; std::vector 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(); auto* relations = model.GetOrCreate(); - auto* lin2_bounds = model.GetOrCreate(); + auto* root_bounds = model.GetOrCreate(); std::vector 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 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 indexes) { std::vector 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 GetRelations(Model& model) { @@ -683,20 +667,16 @@ TEST(BinaryRelationRepositoryTest, LoadCpModelAddUnaryAndBinaryRelations) { LoadCpModel(model_proto, &model); const CpModelMapping& mapping = *model.GetOrCreate(); - 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(); 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(); absl::flat_hash_map input = {{x, 3}}; absl::flat_hash_map 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(); absl::flat_hash_map input = {{x, 3}}; absl::flat_hash_map 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(); absl::flat_hash_map input = {{x, 3}}; absl::flat_hash_map 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(); 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(); absl::flat_hash_map input = {{x, 3}}; absl::flat_hash_map 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(); 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(); absl::flat_hash_map input = {{x, 3}}; absl::flat_hash_map 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(); - RootLevelLinear2Bounds* root_level_bounds = - model.GetOrCreate(); 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(); auto* solver = model.GetOrCreate(); @@ -1017,14 +995,12 @@ TEST(GreaterThanAtLeastOneOfDetectorTest, model.Add(ClauseConstraint({lit_a, lit_b, lit_c})); auto* repository = model.GetOrCreate(); - RootLevelLinear2Bounds* root_level_bounds = - model.GetOrCreate(); 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(); auto* solver = model.GetOrCreate(); diff --git a/ortools/sat/routing_cuts.cc b/ortools/sat/routing_cuts.cc index cdf96d1edb..1da0ac49e1 100644 --- a/ortools/sat/routing_cuts.cc +++ b/ortools/sat/routing_cuts.cc @@ -124,6 +124,7 @@ MinOutgoingFlowHelper::MinOutgoingFlowHelper( trail_(*model->GetOrCreate()), integer_trail_(*model->GetOrCreate()), integer_encoder_(*model->GetOrCreate()), + root_level_bounds_(*model->GetOrCreate()), shared_stats_(model->GetOrCreate()), 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 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(); const auto& trail = *model->GetOrCreate(); const auto& integer_trail = *model->GetOrCreate(); + const auto& root_level_bounds = + *model->GetOrCreate(); DCHECK_EQ(trail.CurrentDecisionLevel(), 0); flat_arc_dim_relations_ = std::vector( @@ -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()); + repository.Build(); return repository; } @@ -1945,6 +1949,7 @@ class RoutingCutHelper { *model->GetOrCreate()), random_(model->GetOrCreate()), encoder_(model->GetOrCreate()), + root_level_bounds_(*model->GetOrCreate()), 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 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; diff --git a/ortools/sat/routing_cuts.h b/ortools/sat/routing_cuts.h index 584e0cca19..0713f01bc4 100644 --- a/ortools/sat/routing_cuts.h +++ b/ortools/sat/routing_cuts.h @@ -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 diff --git a/ortools/sat/routing_cuts_test.cc b/ortools/sat/routing_cuts_test.cc index 707b9f8b37..39bb0469ee 100644 --- a/ortools/sat/routing_cuts_test.cc +++ b/ortools/sat/routing_cuts_test.cc @@ -164,7 +164,7 @@ TEST(MinOutgoingFlowHelperTest, CapacityConstraints) { repository->Add(literal, LinearExpression2(loads[head], loads[tail], 1, -1), head_load, 1000); } - repository->Build(model.GetOrCreate()); + 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()); + repository->Build(); const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions( num_nodes, tails, heads, literals, *repository); std::unique_ptr route_relations_helper = @@ -312,7 +312,7 @@ TEST_P(DimensionBasedMinOutgoingFlowHelperTest, demands[use_outgoing_load ? head : tail], 1000); } } - repository->Build(model.GetOrCreate()); + repository->Build(); const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions( num_nodes, tails, heads, literals, *repository); std::unique_ptr 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()); + repository->Build(); std::unique_ptr 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()); + repository->Build(); std::unique_ptr 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()); + repository->Build(); std::unique_ptr 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()); + repository->Build(); std::unique_ptr 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()); + repository->Build(); std::unique_ptr 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()); + repository->Build(); std::unique_ptr 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()); + 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()); + repository->Build(); const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions( loads.size(), tails, heads, literals, *repository); std::unique_ptr route_relations_helper = @@ -799,7 +799,7 @@ TEST(MinOutgoingFlowHelperTest, DimensionBasedMinOutgoingFlow_IsolatedNodes) { LinearExpression2(variables[head], variables[0], 1, -1), 1, 100); } - repository->Build(model.GetOrCreate()); + repository->Build(); const RoutingCumulExpressions cumuls = DetectDimensionsAndCumulExpressions( num_nodes, tails, heads, literals, *repository); std::unique_ptr 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()); + 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()); + 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()); + repository->Build(); // To check our indices mapping, lets remove a random nodes from the subset std::vector subset; @@ -1186,7 +1186,7 @@ TEST(MinOutgoingFlowHelperTest, LinearExpression2::Difference(cumul_vars[head], cumul_vars[tail]), travel_times[arc], 10000); } - repository->Build(model.GetOrCreate()); + repository->Build(); // Serve everyone but the depot. std::vector 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()); + 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()); + 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()); + 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()); + 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()); + 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()); + 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()); + 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()); + 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()); + 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()); + repository->Build(); // Enable the cut generator. model.GetOrCreate() ->set_routing_cut_max_infeasible_path_length(10); diff --git a/ortools/sat/scheduling_helpers.cc b/ortools/sat/scheduling_helpers.cc index fa6fe706a5..6dd090fae4 100644 --- a/ortools/sat/scheduling_helpers.cc +++ b/ortools/sat/scheduling_helpers.cc @@ -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) {