From 00adfb5dd291229a9df794a3035bf7c28026116b Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 31 Jan 2025 17:09:37 +0100 Subject: [PATCH] [CP-SAT] more bugfixes --- ortools/sat/all_different.cc | 5 +- ortools/sat/cp_constraints.cc | 12 ++-- ortools/sat/cp_model_loader.cc | 8 +-- ortools/sat/cp_model_solver_helpers.cc | 1 + ortools/sat/cuts.cc | 3 +- ortools/sat/cuts.h | 3 +- ortools/sat/implied_bounds.cc | 17 ++++-- ortools/sat/implied_bounds.h | 4 +- ortools/sat/implied_bounds_test.cc | 3 +- ortools/sat/linear_constraint_manager.h | 7 +++ ortools/sat/linear_programming_constraint.cc | 19 +++--- ortools/sat/linear_programming_constraint.h | 19 ++++-- ortools/sat/precedences.cc | 50 +++++++--------- ortools/sat/precedences.h | 61 +++++++++++++++----- ortools/sat/precedences_test.cc | 17 +++--- ortools/sat/presolve_context.cc | 5 +- ortools/sat/scheduling_cuts.cc | 4 +- 17 files changed, 149 insertions(+), 89 deletions(-) diff --git a/ortools/sat/all_different.cc b/ortools/sat/all_different.cc index f2bb1abc8a..b88d0e80a2 100644 --- a/ortools/sat/all_different.cc +++ b/ortools/sat/all_different.cc @@ -275,7 +275,7 @@ bool AllDifferentConstraint::Propagate() { successor_.AppendToLastVector(value); // Seed with previous matching. - if (prev_matching_[x] == value) { + if (prev_matching_[x] == value && value_to_variable_[value] == -1) { variable_to_value_[x] = prev_matching_[x]; value_to_variable_[prev_matching_[x]] = x; } @@ -373,6 +373,7 @@ bool AllDifferentConstraint::Propagate() { if (assignment.LiteralIsFalse(x_lit)) continue; const int value_node = value + num_variables_; + DCHECK_LT(value_node, component_number_.size()); if (variable_to_value_[x] != value && component_number_[x] != component_number_[value_node]) { // We can deduce that x != value. To explain, force x == value, @@ -383,6 +384,8 @@ bool AllDifferentConstraint::Propagate() { variable_visited_.assign(num_variables_, false); // Undo x -> old_value and old_variable -> value. const int old_variable = value_to_variable_[value]; + DCHECK_GE(old_variable, 0); + DCHECK_LT(old_variable, num_variables_); variable_to_value_[old_variable] = -1; const int old_value = variable_to_value_[x]; value_to_variable_[old_value] = -1; diff --git a/ortools/sat/cp_constraints.cc b/ortools/sat/cp_constraints.cc index bf431f4f59..80c29cf3f3 100644 --- a/ortools/sat/cp_constraints.cc +++ b/ortools/sat/cp_constraints.cc @@ -135,20 +135,22 @@ bool GreaterThanAtLeastOneOfPropagator::Propagate() { int first_non_false = 0; const int size = exprs_.size(); + Literal* const selectors = selectors_.data(); + AffineExpression* const exprs = exprs_.data(); for (int i = 0; i < size; ++i) { - if (assignment.LiteralIsTrue(selectors_[i])) return true; + if (assignment.LiteralIsTrue(selectors[i])) return true; // The permutation is needed to have proper lazy reason. - if (assignment.LiteralIsFalse(selectors_[i])) { + if (assignment.LiteralIsFalse(selectors[i])) { if (i != first_non_false) { - std::swap(selectors_[i], selectors_[first_non_false]); - std::swap(exprs_[i], exprs_[first_non_false]); + std::swap(selectors[i], selectors[first_non_false]); + std::swap(exprs[i], exprs[first_non_false]); } ++first_non_false; continue; } - const IntegerValue min = integer_trail_->LowerBound(exprs_[i]); + const IntegerValue min = integer_trail_->LowerBound(exprs[i]); if (min < target_min) { target_min = min; diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 9150902387..df2b6bc4fb 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -1286,14 +1286,14 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { rhs_min = std::max(rhs_min, min_sum.value()); rhs_max = std::min(rhs_max, max_sum.value()); - auto* detector = m->GetOrCreate(); + auto* repository = m->GetOrCreate(); const Literal lit = mapping->Literal(ct.enforcement_literal(0)); const Domain domain = ReadDomainFromProto(ct.linear()); if (vars.size() == 1) { - detector->Add(lit, {vars[0], coeffs[0]}, {}, rhs_min, rhs_max); + repository->Add(lit, {vars[0], coeffs[0]}, {}, rhs_min, rhs_max); } else if (vars.size() == 2) { - detector->Add(lit, {vars[0], coeffs[0]}, {vars[1], coeffs[1]}, rhs_min, - rhs_max); + repository->Add(lit, {vars[0], coeffs[0]}, {vars[1], coeffs[1]}, rhs_min, + rhs_max); } } diff --git a/ortools/sat/cp_model_solver_helpers.cc b/ortools/sat/cp_model_solver_helpers.cc index b41af14fc3..5fd97b89da 100644 --- a/ortools/sat/cp_model_solver_helpers.cc +++ b/ortools/sat/cp_model_solver_helpers.cc @@ -1253,6 +1253,7 @@ void LoadCpModel(const CpModelProto& model_proto, Model* model) { // Note that we do that before we finish loading the problem (objective and // LP relaxation), because propagation will be faster at this point and it // should be enough for the purpose of this auto-detection. + model->GetOrCreate()->Build(); if (parameters.auto_detect_greater_than_at_least_one_of()) { model->GetOrCreate() ->AddGreaterThanAtLeastOneOfConstraints(model); diff --git a/ortools/sat/cuts.cc b/ortools/sat/cuts.cc index fbc65d13c7..bb31ab8f0e 100644 --- a/ortools/sat/cuts.cc +++ b/ortools/sat/cuts.cc @@ -1666,8 +1666,7 @@ BoolRLTCutHelper::~BoolRLTCutHelper() { shared_stats_->AddStats(stats); } -void BoolRLTCutHelper::Initialize( - const absl::flat_hash_map& lp_vars) { +void BoolRLTCutHelper::Initialize(absl::Span lp_vars) { product_detector_->InitializeBooleanRLTCuts(lp_vars, *lp_values_); enabled_ = !product_detector_->BoolRLTCandidates().empty(); } diff --git a/ortools/sat/cuts.h b/ortools/sat/cuts.h index a51dcb835e..ab5563494b 100644 --- a/ortools/sat/cuts.h +++ b/ortools/sat/cuts.h @@ -582,8 +582,7 @@ class BoolRLTCutHelper { // Precompute data according to the current lp relaxation. // This also restrict any Boolean to be currently appearing in the LP. - void Initialize( - const absl::flat_hash_map& lp_vars); + void Initialize(absl::Span lp_vars); // Tries RLT separation of the input constraint. Returns true on success. bool TrySimpleSeparation(const CutData& input_ct); diff --git a/ortools/sat/implied_bounds.cc b/ortools/sat/implied_bounds.cc index fab1b7dfc1..8fed91fe17 100644 --- a/ortools/sat/implied_bounds.cc +++ b/ortools/sat/implied_bounds.cc @@ -797,7 +797,7 @@ void ProductDetector::UpdateRLTMaps( // TODO(user): limit work if too many ternary. void ProductDetector::InitializeBooleanRLTCuts( - const absl::flat_hash_map& lp_vars, + absl::Span lp_vars, const util_intops::StrongVector& lp_values) { // TODO(user): Maybe we shouldn't reconstruct this every time, but it is hard // in case of multiple lps to make sure we don't use variables not in the lp @@ -808,14 +808,19 @@ void ProductDetector::InitializeBooleanRLTCuts( // We will list all interesting multiplicative candidate for each variable. bool_rlt_candidates_.clear(); const int size = ternary_clauses_with_view_.size(); + if (size == 0) return; + + is_in_lp_vars_.resize(integer_trail_->NumIntegerVariables().value()); + for (const IntegerVariable var : lp_vars) is_in_lp_vars_.Set(var); + for (int i = 0; i < size; i += 3) { const IntegerVariable var1 = ternary_clauses_with_view_[i]; const IntegerVariable var2 = ternary_clauses_with_view_[i + 1]; const IntegerVariable var3 = ternary_clauses_with_view_[i + 2]; - if (!lp_vars.contains(PositiveVariable(var1))) continue; - if (!lp_vars.contains(PositiveVariable(var2))) continue; - if (!lp_vars.contains(PositiveVariable(var3))) continue; + if (!is_in_lp_vars_[PositiveVariable(var1)]) continue; + if (!is_in_lp_vars_[PositiveVariable(var2)]) continue; + if (!is_in_lp_vars_[PositiveVariable(var3)]) continue; // If we have l1 + l2 + l3 >= 1, then for all (i, j) pair we have // !li * !lj <= lk. We are looking for violation like this. @@ -830,6 +835,10 @@ void ProductDetector::InitializeBooleanRLTCuts( UpdateRLTMaps(lp_values, NegationOf(var2), 1.0 - lp2, NegationOf(var3), 1.0 - lp3, var1, lp1); } + + // Clear. + // TODO(user): Just switch to memclear() when dense. + for (const IntegerVariable var : lp_vars) is_in_lp_vars_.ClearBucket(var); } } // namespace sat diff --git a/ortools/sat/implied_bounds.h b/ortools/sat/implied_bounds.h index 0cdf3f0ffe..f3301f0ef6 100644 --- a/ortools/sat/implied_bounds.h +++ b/ortools/sat/implied_bounds.h @@ -298,7 +298,7 @@ class ProductDetector { // Experimental. Find violated inequality of the form l1 * l2 <= l3. // And set-up data structure to query this efficiently. void InitializeBooleanRLTCuts( - const absl::flat_hash_map& lp_vars, + absl::Span lp_vars, const util_intops::StrongVector& lp_values); // BoolRLTCandidates()[var] contains the list of factor for which we have @@ -385,6 +385,8 @@ class ProductDetector { // as NegatedVariable(). This is a flat vector of size multiple of 3. std::vector ternary_clauses_with_view_; + Bitset64 is_in_lp_vars_; + // Stats. int64_t num_products_ = 0; int64_t num_int_products_ = 0; diff --git a/ortools/sat/implied_bounds_test.cc b/ortools/sat/implied_bounds_test.cc index 8bcb8fe36e..9421020b68 100644 --- a/ortools/sat/implied_bounds_test.cc +++ b/ortools/sat/implied_bounds_test.cc @@ -665,8 +665,7 @@ TEST(ProductDetectorTest, RLT) { lp_values[x] = 0.7; lp_values[y] = 0.9; lp_values[z] = 0.2; - const absl::flat_hash_map lp_vars = { - {x, glop::ColIndex(0)}, {y, glop::ColIndex(1)}, {z, glop::ColIndex(2)}}; + std::vector lp_vars = {x, y, z}; detector->InitializeBooleanRLTCuts(lp_vars, lp_values); // (1 - X) * Y <= Z, 0.3 * 0.9 == 0.27 <= 0.2, interesting! diff --git a/ortools/sat/linear_constraint_manager.h b/ortools/sat/linear_constraint_manager.h index 4b0f3ce8bd..f83746acae 100644 --- a/ortools/sat/linear_constraint_manager.h +++ b/ortools/sat/linear_constraint_manager.h @@ -56,6 +56,13 @@ struct ModelReducedCosts ModelReducedCosts() = default; }; +// Stores the mapping integer_variable -> glop::ColIndex. +// This is shared across all LP, which is fine since there are disjoint. +struct ModelLpVariableMapping + : public util_intops::StrongVector { + ModelLpVariableMapping() = default; +}; + // Knowing the symmetry of the IP problem should allow us to // solve the LP faster via "folding" techniques. // diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 3cb3cec4c1..af082d5100 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -296,6 +296,7 @@ LinearProgrammingConstraint::LinearProgrammingConstraint( implied_bounds_processor_({}, integer_trail_, model->GetOrCreate()), dispatcher_(model->GetOrCreate()), + mirror_lp_variable_(*model->GetOrCreate()), expanded_lp_solution_(*model->GetOrCreate()), expanded_reduced_costs_(*model->GetOrCreate()) { // Tweak the default parameters to make the solve incremental. @@ -314,6 +315,8 @@ LinearProgrammingConstraint::LinearProgrammingConstraint( // Register our local rev int repository. integer_trail_->RegisterReversibleClass(&rc_rev_int_repository_); + mirror_lp_variable_.resize(integer_trail_->NumIntegerVariables(), + glop::kInvalidCol); // Register SharedStatistics with the cut helpers. auto* stats = model->GetOrCreate(); @@ -336,6 +339,7 @@ LinearProgrammingConstraint::LinearProgrammingConstraint( integer_variables_.push_back(positive_variable); extended_integer_variables_.push_back(positive_variable); + DCHECK_EQ(mirror_lp_variable_[positive_variable], glop::kInvalidCol); mirror_lp_variable_[positive_variable] = col; ++col; } @@ -347,6 +351,7 @@ LinearProgrammingConstraint::LinearProgrammingConstraint( const int orbit_index = symmetrizer_->OrbitIndex(var); for (const IntegerVariable var : symmetrizer_->Orbit(orbit_index)) { extended_integer_variables_.push_back(var); + DCHECK_EQ(mirror_lp_variable_[var], glop::kInvalidCol); mirror_lp_variable_[var] = col; ++col; } @@ -458,7 +463,7 @@ void LinearProgrammingConstraint::RegisterWith(Model* model) { glop::ColIndex LinearProgrammingConstraint::GetMirrorVariable( IntegerVariable positive_variable) { DCHECK(VariableIsPositive(positive_variable)); - return mirror_lp_variable_.at(positive_variable); + return mirror_lp_variable_[positive_variable]; } void LinearProgrammingConstraint::SetObjectiveCoefficient(IntegerVariable ivar, @@ -898,7 +903,7 @@ glop::Fractional LinearProgrammingConstraint::GetVariableValueAtCpScale( double LinearProgrammingConstraint::GetSolutionValue( IntegerVariable variable) const { - return lp_solution_[mirror_lp_variable_.at(variable).value()]; + return lp_solution_[mirror_lp_variable_[variable].value()]; } void LinearProgrammingConstraint::UpdateBoundsOfLpVariables() { @@ -1539,8 +1544,7 @@ bool LinearProgrammingConstraint::PostprocessAndAddCut( // Simple copy for non-slack variables. if (var < first_slack) { - const glop::ColIndex col = - mirror_lp_variable_.at(PositiveVariable(var)); + const glop::ColIndex col = mirror_lp_variable_[PositiveVariable(var)]; if (VariableIsPositive(var)) { tmp_scattered_vector_.Add(col, coeff); } else { @@ -2166,7 +2170,7 @@ bool LinearProgrammingConstraint::Propagate() { implied_bounds_processor_.RecomputeCacheAndSeparateSomeImpliedBoundCuts( expanded_lp_solution_); if (parameters_.add_rlt_cuts()) { - rlt_cut_helper_.Initialize(mirror_lp_variable_); + rlt_cut_helper_.Initialize(extended_integer_variables_); } // The "generic" cuts are currently part of this class as they are using @@ -2610,12 +2614,11 @@ bool LinearProgrammingConstraint::PropagateExactLpReason() { // For the corner case of an objective of size 1, we do not want or need // to take it into account. bool take_objective_into_account = true; - if (mirror_lp_variable_.contains(objective_cp_)) { + if (objective_cp_is_part_of_lp_) { // The objective is part of the lp. // This should only happen for objective with a single term. CHECK_EQ(integer_objective_.size(), 1); - CHECK_EQ(integer_objective_[0].first, - mirror_lp_variable_.at(objective_cp_)); + CHECK_EQ(integer_objective_[0].first, mirror_lp_variable_[objective_cp_]); CHECK_EQ(integer_objective_[0].second, IntegerValue(1)); take_objective_into_account = false; diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h index f517d711a4..9fb24c3528 100644 --- a/ortools/sat/linear_programming_constraint.h +++ b/ortools/sat/linear_programming_constraint.h @@ -154,7 +154,16 @@ class LinearProgrammingConstraint : public PropagatorInterface, // The main objective variable should be equal to the linear sum of // the arguments passed to SetObjectiveCoefficient(). - void SetMainObjectiveVariable(IntegerVariable ivar) { objective_cp_ = ivar; } + void SetMainObjectiveVariable(IntegerVariable ivar) { + objective_cp_ = ivar; + objective_cp_is_part_of_lp_ = false; + for (const IntegerVariable var : integer_variables_) { + if (var == objective_cp_) { + objective_cp_is_part_of_lp_ = true; + break; + } + } + } IntegerVariable ObjectiveVariable() const { return objective_cp_; } // Register a new cut generator with this constraint. @@ -500,14 +509,10 @@ class LinearProgrammingConstraint : public PropagatorInterface, // Structures used for mirroring IntegerVariables inside the underlying LP // solver: an integer variable var is mirrored by mirror_lp_variable_[var]. - // Note that these indices are dense in [0, mirror_lp_variable_.size()] so + // Note that these indices are dense in [0, integer_variables.size()] so // they can be used as vector indices. - // - // TODO(user): This should be util_intops::StrongVector. std::vector integer_variables_; std::vector extended_integer_variables_; - absl::flat_hash_map mirror_lp_variable_; // This is only used if we use symmetry folding. // Refer to relevant orbit in the LinearConstraintSymmetrizer. @@ -516,6 +521,7 @@ class LinearProgrammingConstraint : public PropagatorInterface, // We need to remember what to optimize if an objective is given, because // then we will switch the objective between feasibility and optimization. bool objective_is_defined_ = false; + bool objective_cp_is_part_of_lp_ = false; IntegerVariable objective_cp_; // Singletons from Model. @@ -587,6 +593,7 @@ class LinearProgrammingConstraint : public PropagatorInterface, bool lp_at_level_zero_is_final_ = false; // Same as lp_solution_ but this vector is indexed by IntegerVariable. + ModelLpVariableMapping& mirror_lp_variable_; ModelLpValues& expanded_lp_solution_; ModelReducedCosts& expanded_reduced_costs_; diff --git a/ortools/sat/precedences.cc b/ortools/sat/precedences.cc index f6821c94a1..5151fba7d0 100644 --- a/ortools/sat/precedences.cc +++ b/ortools/sat/precedences.cc @@ -1104,9 +1104,8 @@ bool PrecedencesPropagator::BellmanFordTarjan(Trail* trail) { return true; } -void GreaterThanAtLeastOneOfDetector::Add(Literal lit, LinearTerm a, - LinearTerm b, IntegerValue lhs, - IntegerValue rhs) { +void BinaryRelationRepository::Add(Literal lit, LinearTerm a, LinearTerm b, + IntegerValue lhs, IntegerValue rhs) { Relation r; r.enforcement = lit; r.a = a; @@ -1127,6 +1126,18 @@ void GreaterThanAtLeastOneOfDetector::Add(Literal lit, LinearTerm a, relations_.push_back(std::move(r)); } +void BinaryRelationRepository::Build() { + DCHECK(!is_built_); + is_built_ = true; + std::vector keys; + const int num_relations = relations_.size(); + keys.reserve(num_relations); + for (int i = 0; i < num_relations; ++i) { + keys.push_back(relations_[i].enforcement.Index()); + } + lit_to_relations_.ResetFromFlatMapping(keys, IdentityMap()); +} + bool GreaterThanAtLeastOneOfDetector::AddRelationFromIndices( IntegerVariable var, absl::Span clause, absl::Span indices, Model* model) { @@ -1137,7 +1148,7 @@ bool GreaterThanAtLeastOneOfDetector::AddRelationFromIndices( const IntegerValue var_lb = integer_trail->LevelZeroLowerBound(var); for (const int index : indices) { - Relation r = relations_[index]; + Relation r = repository_.relation(index); if (r.a.var != PositiveVariable(var)) std::swap(r.a, r.b); CHECK_EQ(r.a.var, PositiveVariable(var)); @@ -1193,9 +1204,8 @@ int GreaterThanAtLeastOneOfDetector:: // Collect all relations impacted by this clause. std::vector> infos; for (const Literal l : clause) { - if (l.Index() >= lit_to_relations_->size()) continue; - for (const int index : (*lit_to_relations_)[l.Index()]) { - const Relation& r = relations_[index]; + for (const int index : repository_.relation_indices(l.Index())) { + const Relation& r = repository_.relation(index); if (r.a.var != kNoIntegerVariable && IntTypeAbs(r.a.coeff) == 1) { infos.push_back({r.a.var, index}); } @@ -1247,8 +1257,8 @@ int GreaterThanAtLeastOneOfDetector:: // Fill the set of interesting relations for each variables. util_intops::StrongVector> var_to_relations; - for (int index = 0; index < relations_.size(); ++index) { - const Relation& r = relations_[index]; + for (int index = 0; index < repository_.size(); ++index) { + const Relation& r = repository_.relation(index); if (r.a.var != kNoIntegerVariable && IntTypeAbs(r.a.coeff) == 1) { if (r.a.var >= var_to_relations.size()) { var_to_relations.resize(r.a.var + 1); @@ -1275,7 +1285,7 @@ int GreaterThanAtLeastOneOfDetector:: if (solver->ModelIsUnsat()) return num_added_constraints; std::vector clause; for (const int index : var_to_relations[target]) { - const Literal literal = relations_[index].enforcement; + const Literal literal = repository_.relation(index).enforcement; if (solver->Assignment().LiteralIsFalse(literal)) continue; const SatSolver::Status status = solver->EnqueueDecisionAndBacktrackOnConflict(literal.Negated()); @@ -1295,7 +1305,7 @@ int GreaterThanAtLeastOneOfDetector:: std::vector indices; for (const int index : var_to_relations[target]) { - const Literal literal = relations_[index].enforcement; + const Literal literal = repository_.relation(index).enforcement; if (clause_set.contains(literal)) { indices.push_back(index); } @@ -1322,22 +1332,9 @@ int GreaterThanAtLeastOneOfDetector::AddGreaterThanAtLeastOneOfConstraints( auto* logger = model->GetOrCreate(); int num_added_constraints = 0; - SOLVER_LOG(logger, "[Precedences] num_relations=", relations_.size(), + SOLVER_LOG(logger, "[Precedences] num_relations=", repository_.size(), " num_clauses=", clauses->AllClausesInCreationOrder().size()); - // Initialize lit_to_relations_. - { - std::vector keys; - const int num_relations = relations_.size(); - keys.reserve(num_relations); - for (int i = 0; i < num_relations; ++i) { - keys.push_back(relations_[i].enforcement.Index()); - } - lit_to_relations_ = - std::make_unique>(); - lit_to_relations_->ResetFromFlatMapping(keys, IdentityMap()); - } - // We have two possible approaches. For now, we prefer the first one except if // there is too many clauses in the problem. // @@ -1387,9 +1384,6 @@ int GreaterThanAtLeastOneOfDetector::AddGreaterThanAtLeastOneOfConstraints( " GreaterThanAtLeastOneOf() constraints."); } - // Release the memory, it is not longer needed. - lit_to_relations_.reset(nullptr); - gtl::STLClearObject(&relations_); return num_added_constraints; } diff --git a/ortools/sat/precedences.h b/ortools/sat/precedences.h index 8f304c078b..65a8723a58 100644 --- a/ortools/sat/precedences.h +++ b/ortools/sat/precedences.h @@ -469,18 +469,56 @@ struct LinearTerm { IntegerValue coeff = IntegerValue(0); }; -// This collect all enforced linear of size 2 or 1 and detect if at least one of -// a subset touching the same variable must be true. When this is the case -// we add a new propagator to propagate that fact. +// A relation of the form enforcement => a + b \in [lhs, rhs]. +// Note that the [lhs, rhs] interval should always be within [min_activity, +// max_activity] where the activity is the value of a + b. +struct Relation { + Literal enforcement; + LinearTerm a; + LinearTerm b; + IntegerValue lhs; + IntegerValue rhs; +}; + +// A repository of all the enforced linear constraints of size 1 or 2. // -// TODO(user): Shall we do that on the main thread before the workers are -// spawned? note that the probing version need the model to be loaded though. -class GreaterThanAtLeastOneOfDetector { +// TODO(user): This is not always needed, find a way to clean this once we +// don't need it. +class BinaryRelationRepository { public: + int size() const { return relations_.size(); } + const Relation& relation(int index) const { return relations_[index]; } + + absl::Span relation_indices(LiteralIndex lit) const { + if (lit >= lit_to_relations_.size()) return {}; + return lit_to_relations_[lit]; + } + // Adds a relation lit => a + b \in [lhs, rhs]. void Add(Literal lit, LinearTerm a, LinearTerm b, IntegerValue lhs, IntegerValue rhs); + // Builds the literal to relations mapping. This should be called once all the + // relations have been added. + void Build(); + + private: + bool is_built_ = false; + std::vector relations_; + CompactVectorVector lit_to_relations_; +}; + +// Detects if at least one of a subset of linear of size 2 or 1, touching the +// same variable, must be true. When this is the case we add a new propagator to +// propagate that fact. +// +// TODO(user): Shall we do that on the main thread before the workers are +// spawned? note that the probing version need the model to be loaded though. +class GreaterThanAtLeastOneOfDetector { + public: + explicit GreaterThanAtLeastOneOfDetector(Model* model) + : repository_(*model->GetOrCreate()) {} + // Advanced usage. To be called once all the constraints have been added to // the model. This will detect GreaterThanAtLeastOneOfConstraint(). // Returns the number of added constraint. @@ -510,16 +548,7 @@ class GreaterThanAtLeastOneOfDetector { absl::Span clause, absl::Span indices, Model* model); - struct Relation { - Literal enforcement; - LinearTerm a; - LinearTerm b; - IntegerValue lhs; - IntegerValue rhs; - }; - std::vector relations_; - - std::unique_ptr> lit_to_relations_; + BinaryRelationRepository& repository_; }; // ============================================================================= diff --git a/ortools/sat/precedences_test.cc b/ortools/sat/precedences_test.cc index cda31a9ef2..f72587706d 100644 --- a/ortools/sat/precedences_test.cc +++ b/ortools/sat/precedences_test.cc @@ -32,7 +32,6 @@ namespace sat { namespace { using ::testing::ElementsAre; -using ::testing::Pair; using ::testing::UnorderedElementsAre; // A simple macro to make the code more readable. @@ -455,10 +454,12 @@ TEST(GreaterThanAtLeastOneOfDetectorTest, AddGreaterThanAtLeastOneOf) { const Literal lit_c = Literal(model.Add(NewBooleanVariable()), true); model.Add(ClauseConstraint({lit_a, lit_b, lit_c})); + auto* repository = model.GetOrCreate(); + repository->Add(lit_a, {a, -1}, {d, 1}, 2, 1000); // d >= a + 2 + repository->Add(lit_b, {b, -1}, {d, 1}, -1, 1000); // d >= b -1 + repository->Add(lit_c, {c, -1}, {d, 1}, 0, 1000); // d >= c + repository->Build(); auto* detector = model.GetOrCreate(); - detector->Add(lit_a, {a, -1}, {d, 1}, 2, 1000); // d >= a + 2 - detector->Add(lit_b, {b, -1}, {d, 1}, -1, 1000); // d >= b -1 - detector->Add(lit_c, {c, -1}, {d, 1}, 0, 1000); // d >= c auto* solver = model.GetOrCreate(); EXPECT_TRUE(solver->Propagate()); @@ -481,10 +482,12 @@ TEST(GreaterThanAtLeastOneOfDetectorTest, const Literal lit_c = Literal(model.Add(NewBooleanVariable()), true); model.Add(ClauseConstraint({lit_a, lit_b, lit_c})); + auto* repository = model.GetOrCreate(); + repository->Add(lit_a, {a, -1}, {d, 1}, 2, 1000); // d >= a + 2 + repository->Add(lit_b, {b, -1}, {d, 1}, -1, 1000); // d >= b -1 + repository->Add(lit_c, {c, -1}, {d, 1}, 0, 1000); // d >= c + repository->Build(); auto* detector = model.GetOrCreate(); - detector->Add(lit_a, {a, -1}, {d, 1}, 2, 1000); // d >= a + 2 - detector->Add(lit_b, {b, -1}, {d, 1}, -1, 1000); // d >= b -1 - detector->Add(lit_c, {c, -1}, {d, 1}, 0, 1000); // d >= c auto* solver = model.GetOrCreate(); EXPECT_TRUE(solver->Propagate()); diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 129cfe85a5..0ca203e988 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -1259,7 +1259,10 @@ bool PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) { CHECK(CanBeUsedAsLiteral(ref_b)); if (ref_a == ref_b) return true; - if (ref_a == NegatedRef(ref_b)) return false; + if (ref_a == NegatedRef(ref_b)) { + is_unsat_ = true; + return false; + } const int var_a = PositiveRef(ref_a); const int var_b = PositiveRef(ref_b); diff --git a/ortools/sat/scheduling_cuts.cc b/ortools/sat/scheduling_cuts.cc index 44ffe75341..3dcb659c29 100644 --- a/ortools/sat/scheduling_cuts.cc +++ b/ortools/sat/scheduling_cuts.cc @@ -480,7 +480,7 @@ void GenerateCumulativeEnergeticCutsWithMakespanAndFixedCapacity( } void GenerateCumulativeEnergeticCuts( - const std::string& cut_name, + absl::string_view cut_name, const util_intops::StrongVector& lp_values, std::vector events, const AffineExpression& capacity, TimeLimit* time_limit, Model* model, LinearConstraintManager* manager) { @@ -568,7 +568,7 @@ void GenerateCumulativeEnergeticCuts( } if (cut_generated) { - std::string full_name = cut_name; + std::string full_name(cut_name); if (add_opt_to_name) full_name.append("_optional"); if (add_quadratic_to_name) full_name.append("_quadratic"); if (add_lifted_to_name) full_name.append("_lifted");