[CP-SAT] more bugfixes

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;

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;
 

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<GreaterThanAtLeastOneOfDetector>();
+    auto* repository = m->GetOrCreate<BinaryRelationRepository>();
     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);
     }
   }
 

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<BinaryRelationRepository>()->Build();
   if (parameters.auto_detect_greater_than_at_least_one_of()) {
     model->GetOrCreate<GreaterThanAtLeastOneOfDetector>()
         ->AddGreaterThanAtLeastOneOfConstraints(model);

ortools/sat/cuts.cc

@@ -1666,8 +1666,7 @@ BoolRLTCutHelper::~BoolRLTCutHelper() {
   shared_stats_->AddStats(stats);
 }
 
-void BoolRLTCutHelper::Initialize(
-    const absl::flat_hash_map<IntegerVariable, glop::ColIndex>& lp_vars) {
+void BoolRLTCutHelper::Initialize(absl::Span<const IntegerVariable> lp_vars) {
   product_detector_->InitializeBooleanRLTCuts(lp_vars, *lp_values_);
   enabled_ = !product_detector_->BoolRLTCandidates().empty();
 }

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<IntegerVariable, glop::ColIndex>& lp_vars);
+  void Initialize(absl::Span<const IntegerVariable> lp_vars);
 
   // Tries RLT separation of the input constraint. Returns true on success.
   bool TrySimpleSeparation(const CutData& input_ct);

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<IntegerVariable, glop::ColIndex>& lp_vars,
+    absl::Span<const IntegerVariable> lp_vars,
     const util_intops::StrongVector<IntegerVariable, double>& 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

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<IntegerVariable, glop::ColIndex>& lp_vars,
+      absl::Span<const IntegerVariable> lp_vars,
       const util_intops::StrongVector<IntegerVariable, double>& 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<IntegerVariable> ternary_clauses_with_view_;
 
+  Bitset64<IntegerVariable> is_in_lp_vars_;
+
   // Stats.
   int64_t num_products_ = 0;
   int64_t num_int_products_ = 0;

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<IntegerVariable, glop::ColIndex> lp_vars = {
-      {x, glop::ColIndex(0)}, {y, glop::ColIndex(1)}, {z, glop::ColIndex(2)}};
+  std::vector<IntegerVariable> lp_vars = {x, y, z};
   detector->InitializeBooleanRLTCuts(lp_vars, lp_values);
 
   // (1 - X) * Y <= Z,   0.3 * 0.9 == 0.27 <= 0.2,   interesting!

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<IntegerVariable, glop::ColIndex> {
+  ModelLpVariableMapping() = default;
+};
+
 // Knowing the symmetry of the IP problem should allow us to
 // solve the LP faster via "folding" techniques.
 //

ortools/sat/linear_programming_constraint.cc

@@ -296,6 +296,7 @@ LinearProgrammingConstraint::LinearProgrammingConstraint(
       implied_bounds_processor_({}, integer_trail_,
                                 model->GetOrCreate<ImpliedBounds>()),
       dispatcher_(model->GetOrCreate<LinearProgrammingDispatcher>()),
+      mirror_lp_variable_(*model->GetOrCreate<ModelLpVariableMapping>()),
       expanded_lp_solution_(*model->GetOrCreate<ModelLpValues>()),
       expanded_reduced_costs_(*model->GetOrCreate<ModelReducedCosts>()) {
   // 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<SharedStatistics>();
@@ -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;

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<glop::ColIndex,
-  // IntegerVariable>.
   std::vector<IntegerVariable> integer_variables_;
   std::vector<IntegerVariable> extended_integer_variables_;
-  absl::flat_hash_map<IntegerVariable, glop::ColIndex> 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_;