From e4c6bbb327f5b7c40258a3b229f6d30fab193dd0 Mon Sep 17 00:00:00 2001
From: Laurent Perron <lperron@google.com>
Date: Thu, 15 Dec 2022 10:37:30 +0100
Subject: [PATCH] [CP-SAT] better expand_objective during presolve; improved
 implementation of obj_lb_search; refactor search code

---
 ortools/sat/cp_model.h           |  11 +
 ortools/sat/cp_model_presolve.cc | 412 +++++++++++++++----------------
 ortools/sat/cp_model_presolve.h  |   3 +
 ortools/sat/cp_model_search.cc   |   6 +
 ortools/sat/cp_model_solver.cc   |   7 +-
 ortools/sat/cp_model_utils.h     |   5 +-
 ortools/sat/integer_search.cc    | 123 +++++----
 ortools/sat/integer_search.h     |  25 +-
 ortools/sat/optimization.cc      |  92 +------
 ortools/sat/optimization.h       |  35 ---
 ortools/sat/presolve_context.cc  |   7 +-
 ortools/sat/presolve_context.h   |   7 +-
 ortools/sat/pseudo_costs.cc      |  30 ++-
 ortools/sat/pseudo_costs.h       |  13 +-
 ortools/sat/sat_parameters.proto |   3 +
 15 files changed, 343 insertions(+), 436 deletions(-)

diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h
index a56b2ce0bd..116df8f1fd 100644
--- a/ortools/sat/cp_model.h
+++ b/ortools/sat/cp_model.h
@@ -505,6 +505,17 @@ class IntervalVar {
 
 std::ostream& operator<<(std::ostream& os, const IntervalVar& var);
 
+// -- ABSL HASHING SUPPORT -----------------------------------------------------
+template <typename H>
+H AbslHashValue(H h, const IntVar& i) {
+  return H::combine(std::move(h), i.index());
+}
+
+template <typename H>
+H AbslHashValue(H h, const IntervalVar& i) {
+  return H::combine(std::move(h), i.index());
+}
+
 /**
  * A constraint.
  *
diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
index 6889cdd081..b6f1043019 100644
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -40,6 +40,7 @@
 #include "ortools/base/mathutil.h"
 #include "ortools/base/stl_util.h"
 #include "ortools/base/timer.h"
+#include "ortools/graph/topologicalsorter.h"
 #include "ortools/sat/circuit.h"
 #include "ortools/sat/clause.h"
 #include "ortools/sat/cp_model.pb.h"
@@ -1899,8 +1900,7 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) {
       // TODO(user): We have an issue if objective coeff is not one, because
       // the RecomputeSingletonObjectiveDomain() do not properly put holes
       // in the objective domain, which might cause an issue. Note that this
-      // presolve rule is actually almost never applied on the miplib. It is
-      // also a bit redundant with ExpandObjective().
+      // presolve rule is actually almost never applied on the miplib.
       if (std::abs(objective_coeff) != 1) continue;
 
       // We do not do that if the domain of rhs becomes too complex.
@@ -1913,7 +1913,7 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) {
 
       // Special case: If the objective was a single variable, we can transfer
       // the domain of var to the objective, and just completely remove this
-      // equality constraint like it is done in ExpandObjective().
+      // equality constraint.
       //
       // TODO(user): Maybe if var has a complex domain, we might not want to
       // substitute it?
@@ -6643,41 +6643,50 @@ void CpModelPresolver::PresolvePureSatPart() {
                  context_->mapping_model);
 }
 
-// TODO(user): The idea behind this was that it is better to have an objective
-// as spreaded as possible. However on some problems this have the opposite
-// effect. Like on a triangular matrix where each expansion reduced the size
-// of the objective by one. Investigate and fix?
+// Expand the objective expression in some easy cases.
+//
+// The ideas is to look at all the "tight" equality constraints. These should
+// give a topological order on the variable in which we can perform
+// substitution.
+//
+// Basically, we will only use constraints of the form X' = sum ci * Xi' with ci
+// > 0 and the variable X' being shifted version >= 0. Note that if there is a
+// cycle with these constraints, all variables involved must be equal to each
+// other and likely zero. Otherwise, we can express everything in terms of the
+// leaves.
+//
+// This assumes we are more or less at the propagation fix point, even if we
+// try to address cases where we are not.
 void CpModelPresolver::ExpandObjective() {
   if (context_->ModelIsUnsat()) return;
+  WallTimer wall_timer;
+  wall_timer.Start();
 
-  // The objective is already loaded in the context, but we re-canonicalize
-  // it with the latest information.
-  if (!context_->CanonicalizeObjective()) {
-    (void)context_->NotifyThatModelIsUnsat();
-    return;
-  }
-
-  if (context_->time_limit()->LimitReached()) {
-    context_->WriteObjectiveToProto();
-    return;
-  }
-
-  // If the objective is a single variable, then we can usually remove this
-  // variable if it is only used in one linear equality constraint and we do
-  // just one expansion. This is because the domain of the variable will be
-  // transferred to our objective_domain.
-  int unique_expanded_constraint = -1;
-  const bool objective_was_a_single_variable =
-      context_->ObjectiveMap().size() == 1;
-
-  // To avoid a bad complexity, we need to compute the number of relevant
-  // constraints for each variables.
   const int num_variables = context_->working_model->variables_size();
   const int num_constraints = context_->working_model->constraints_size();
-  absl::flat_hash_set<int> relevant_constraints;
-  std::vector<int> var_to_num_relevant_constraints(num_variables, 0);
-  for (int ct_index = 0; ct_index < num_constraints; ++ct_index) {
-    const ConstraintProto& ct = context_->working_model->constraints(ct_index);
+
+  // We consider two types of shifted variables (X - LB(X)) and (UB(X) - X).
+  const auto get_index = [](int var, bool to_lb) {
+    return 2 * var + (to_lb ? 0 : 1);
+  };
+  const int num_nodes = 2 * num_variables;
+  std::vector<std::vector<int>> index_graph(num_nodes);
+
+  // TODO(user): instead compute how much each constraint can be further
+  // expanded?
+  std::vector<int> index_to_best_c(num_nodes, -1);
+
+  // Lets see first if there are "tight" constraint and for which variables.
+  // We stop processing constraint if we have too many entries.
+  int num_entries = 0;
+  int num_propagations = 0;
+  int num_tight_variables = 0;
+  int num_tight_constraints = 0;
+  const int kNumEntriesThreshold = 1e8;
+  for (int c = 0; c < num_constraints; ++c) {
+    if (num_entries > kNumEntriesThreshold) break;
+
+    const ConstraintProto& ct = context_->working_model->constraints(c);
     // Skip everything that is not a linear equality constraint.
     if (!ct.enforcement_literal().empty() ||
         ct.constraint_case() != ConstraintProto::kLinear ||
@@ -6686,202 +6695,185 @@ void CpModelPresolver::ExpandObjective() {
       continue;
     }
 
-    relevant_constraints.insert(ct_index);
+    // Let see for which variable is it "tight". We need a coeff of 1, and that
+    // the implied bounds match exactly.
+    const auto [min_activity, max_activity] =
+        context_->ComputeMinMaxActivity(ct.linear());
+
+    bool is_tight = false;
+    const int64_t rhs = ct.linear().domain(0);
     const int num_terms = ct.linear().vars_size();
     for (int i = 0; i < num_terms; ++i) {
-      var_to_num_relevant_constraints[PositiveRef(ct.linear().vars(i))]++;
-    }
-  }
+      const int var = ct.linear().vars(i);
+      const int64_t coeff = ct.linear().coeffs(i);
+      if (std::abs(coeff) != 1) continue;
+      if (num_entries > kNumEntriesThreshold) break;
 
-  absl::btree_set<int> var_to_process;
-  for (const auto entry : context_->ObjectiveMap()) {
-    const int var = entry.first;
-    CHECK(RefIsPositive(var));
-    if (var_to_num_relevant_constraints[var] != 0) {
-      var_to_process.insert(var);
-    }
-  }
+      const int index = get_index(var, coeff > 0);
 
-  // We currently never expand a variable more than once.
-  int num_expansions = 0;
-  int last_expanded_objective_var;
-  absl::flat_hash_set<int> processed_vars;
-  std::vector<int> new_vars_in_objective;
-  while (!relevant_constraints.empty()) {
-    // Find a not yet expanded var.
-    int objective_var = -1;
-    while (!var_to_process.empty()) {
-      const int var = *var_to_process.begin();
-      CHECK(!processed_vars.contains(var));
-      if (var_to_num_relevant_constraints[var] == 0) {
-        processed_vars.insert(var);
-        var_to_process.erase(var);
-        continue;
-      }
-      if (!context_->ObjectiveMap().contains(var)) {
-        // We do not mark it as processed in case it re-appear later.
-        var_to_process.erase(var);
-        continue;
-      }
-      objective_var = var;
-      break;
-    }
+      const int64_t var_range = context_->MaxOf(var) - context_->MinOf(var);
+      const int64_t implied_shifted_ub = rhs - min_activity;
+      if (implied_shifted_ub <= var_range) {
+        if (implied_shifted_ub < var_range) ++num_propagations;
+        is_tight = true;
+        ++num_tight_variables;
 
-    if (objective_var == -1) break;
-    CHECK(RefIsPositive(objective_var));
-    processed_vars.insert(objective_var);
-    var_to_process.erase(objective_var);
+        const int neg_index = index ^ 1;
+        const int old_c = index_to_best_c[neg_index];
+        if (old_c == -1 ||
+            num_terms > context_->working_model->constraints(old_c)
+                            .linear()
+                            .vars()
+                            .size()) {
+          index_to_best_c[neg_index] = c;
+        }
 
-    int expanded_linear_index = -1;
-    int64_t objective_coeff_in_expanded_constraint;
-    int64_t size_of_expanded_constraint = 0;
-    const auto& non_deterministic_list =
-        context_->VarToConstraints(objective_var);
-    std::vector<int> constraints_with_objective(non_deterministic_list.begin(),
-                                                non_deterministic_list.end());
-    std::sort(constraints_with_objective.begin(),
-              constraints_with_objective.end());
-    for (const int ct_index : constraints_with_objective) {
-      if (relevant_constraints.count(ct_index) == 0) continue;
-      const ConstraintProto& ct =
-          context_->working_model->constraints(ct_index);
-
-      // This constraint is relevant now, but it will never be later because
-      // it will contain the objective_var which is already processed!
-      relevant_constraints.erase(ct_index);
-      const int num_terms = ct.linear().vars_size();
-      for (int i = 0; i < num_terms; ++i) {
-        var_to_num_relevant_constraints[PositiveRef(ct.linear().vars(i))]--;
-      }
-
-      // Find the coefficient of objective_var in this constraint, and perform
-      // various checks.
-      //
-      // TODO(user): This can crash the program if for some reason the linear
-      // constraint was not canonicalized and contains the objective variable
-      // twice. Currently this can only happen if the time limit was reached
-      // before all constraints where processed, but because we abort at the
-      // beginning of the function when this is the case we should be safe.
-      // However, it might be more robust to just handle this case properly.
-      bool is_present = false;
-      int64_t objective_coeff;
-      Domain implied = ReadDomainFromProto(ct.linear());
-      for (int i = 0; i < num_terms; ++i) {
-        const int ref = ct.linear().vars(i);
-        const int64_t coeff = ct.linear().coeffs(i);
-        if (PositiveRef(ref) == objective_var) {
-          CHECK(!is_present) << "Duplicate variables not supported.";
-          is_present = true;
-          objective_coeff = (ref == objective_var) ? coeff : -coeff;
-        } else {
-          // This is not possible since we only consider relevant constraints.
-          CHECK(!processed_vars.contains(PositiveRef(ref)));
-          implied = implied
-                        .AdditionWith(
-                            context_->DomainOf(ref).ContinuousMultiplicationBy(
-                                -coeff))
-                        .RelaxIfTooComplex();
+        for (int j = 0; j < num_terms; ++j) {
+          if (j == i) continue;
+          const int other_index =
+              get_index(ct.linear().vars(j), ct.linear().coeffs(j) > 0);
+          ++num_entries;
+          index_graph[neg_index].push_back(other_index);
         }
       }
-      CHECK(is_present);
+      const int64_t implied_shifted_lb = max_activity - rhs;
+      if (implied_shifted_lb <= var_range) {
+        if (implied_shifted_lb < var_range) ++num_propagations;
+        is_tight = true;
+        ++num_tight_variables;
 
-      // Important: We will only use equation where the implied lb on the
-      // objective var is tight. This is important for core based search, see
-      // for instance vpphard where without this the core do not solve it.
-      implied = implied.InverseMultiplicationBy(objective_coeff);
-      if (context_->ObjectiveCoeff(objective_var) > 0) {
-        if (implied.Min() < context_->MinOf(objective_var)) continue;
-      } else {
-        if (implied.Max() > context_->MaxOf(objective_var)) continue;
-      }
+        const int old_c = index_to_best_c[index];
+        if (old_c == -1 ||
+            num_terms > context_->working_model->constraints(old_c)
+                            .linear()
+                            .vars()
+                            .size()) {
+          index_to_best_c[index] = c;
+        }
 
-      // We use the longest equality we can find.
-      //
-      // TODO(user): Deal with objective_coeff with a magnitude greater than
-      // 1? This will only be possible if we change the objective coeff type
-      // to double.
-      if (std::abs(objective_coeff) == 1 &&
-          num_terms > size_of_expanded_constraint) {
-        expanded_linear_index = ct_index;
-        size_of_expanded_constraint = num_terms;
-        objective_coeff_in_expanded_constraint = objective_coeff;
+        for (int j = 0; j < num_terms; ++j) {
+          if (j == i) continue;
+          const int other_index =
+              get_index(ct.linear().vars(j), ct.linear().coeffs(j) < 0);
+          ++num_entries;
+          index_graph[index].push_back(other_index);
+        }
       }
     }
+    if (is_tight) ++num_tight_constraints;
+  }
 
-    if (expanded_linear_index != -1) {
-      // Update the objective map. Note that the division is possible because
-      // currently we only expand with coeff with a magnitude of 1.
-      CHECK_EQ(std::abs(objective_coeff_in_expanded_constraint), 1);
+  // Note(user): We assume the fixed point was already reached by the linear
+  // presolve, so we don't add extra code here for that. But we still abort if
+  // some are left to cover corner cases were linear a still not propagated.
+  if (num_propagations > 0) {
+    context_->UpdateRuleStats("TODO objective: propagation possible!");
+    return;
+  }
+
+  // In most cases, we should have no cycle and thus a topo order.
+  //
+  // In case there is a cycle, then all member of a strongly connected component
+  // must be equivalent, this is because from X to Y, if we follow the chain we
+  // will have X = non_negative_sum + Y and Y = non_negative_sum + X.
+  //
+  // Moreover, many shifted variables will need to be zero once we start to have
+  // equivalence.
+  //
+  // TODO(user): Make the fixing to zero? or at least when this happen redo
+  // a presolve pass?
+  //
+  // TODO(user): Densify index to only look at variable that can be substituted
+  // further.
+  const auto result = util::graph::FastTopologicalSort(index_graph);
+  if (!result.ok()) {
+    std::vector<std::vector<int>> components;
+    FindStronglyConnectedComponents(static_cast<int>(index_graph.size()),
+                                    index_graph, &components);
+    for (const std::vector<int>& compo : components) {
+      if (compo.size() == 1) continue;
+
+      const int rep_var = compo[0] / 2;
+      const bool rep_to_lp = (compo[0] % 2) == 0;
+      for (int i = 1; i < compo.size(); ++i) {
+        const int var = compo[i] / 2;
+        const bool to_lb = (compo[i] % 2) == 0;
+
+        // (rep - rep_lb)/(rep_ub - rep) == (var - var_lb)/(ub - var_ub)
+        // +/- rep = +/- var + offset.
+        const int64_t rep_coeff = rep_to_lp ? 1 : -1;
+        const int64_t var_coeff = to_lb ? 1 : -1;
+        const int64_t offset =
+            (to_lb ? -context_->MinOf(var) : context_->MaxOf(var)) -
+            (rep_to_lp ? -context_->MinOf(rep_var) : context_->MaxOf(rep_var));
+        if (!context_->StoreAffineRelation(rep_var, var, rep_coeff * var_coeff,
+                                           rep_coeff * offset)) {
+          return;
+        }
+      }
+      context_->UpdateRuleStats("objective: detected equivalence",
+                                compo.size() - 1);
+    }
+    return;
+  }
+
+  // The objective is already loaded in the context, but we re-canonicalize
+  // it with the latest information.
+  if (!context_->CanonicalizeObjective()) {
+    (void)context_->NotifyThatModelIsUnsat();
+    return;
+  }
+
+  // If the removed variable is now unique, we could remove it if it is implied
+  // free. But this should already be done by RemoveSingletonInLinear(), so we
+  // don't redo it here.
+  int num_expands = 0;
+  int num_issues = 0;
+  for (const int index : *result) {
+    if (index_graph[index].empty()) continue;
+
+    const int var = index / 2;
+    const int64_t obj_coeff = context_->ObjectiveCoeff(var);
+    if (obj_coeff == 0) continue;
+
+    const bool to_lb = (index % 2) == 0;
+    if (obj_coeff > 0 == to_lb) {
       const ConstraintProto& ct =
-          context_->working_model->constraints(expanded_linear_index);
+          context_->working_model->constraints(index_to_best_c[index]);
+
+      int64_t objective_coeff_in_expanded_constraint = 0;
+      const int num_terms = ct.linear().vars().size();
+      for (int i = 0; i < num_terms; ++i) {
+        if (ct.linear().vars(i) == var) {
+          objective_coeff_in_expanded_constraint = ct.linear().coeffs(i);
+          break;
+        }
+      }
+      if (objective_coeff_in_expanded_constraint == 0) {
+        ++num_issues;
+        continue;
+      }
+
       if (!context_->SubstituteVariableInObjective(
-              objective_var, objective_coeff_in_expanded_constraint, ct,
-              &new_vars_in_objective)) {
+              var, objective_coeff_in_expanded_constraint, ct)) {
         if (context_->ModelIsUnsat()) return;
+        ++num_issues;
         continue;
       }
 
-      context_->UpdateRuleStats("objective: expanded objective constraint.");
-
-      // Add not yet processed new variables.
-      for (const int var : new_vars_in_objective) {
-        if (!processed_vars.contains(var)) var_to_process.insert(var);
-      }
-
-      // If the objective variable wasn't used in other constraints and it can
-      // be reconstructed whatever the value of the other variables, we can
-      // remove the constraint.
-      //
-      // TODO(user): It should be possible to refactor the code so this is
-      // automatically done by the linear constraint singleton presolve rule.
-      if (context_->VarToConstraints(objective_var).size() == 1 &&
-          !context_->keep_all_feasible_solutions) {
-        // Compute implied domain on objective_var.
-        Domain implied_domain = ReadDomainFromProto(ct.linear());
-        for (int i = 0; i < size_of_expanded_constraint; ++i) {
-          const int ref = ct.linear().vars(i);
-          if (PositiveRef(ref) == objective_var) continue;
-          implied_domain =
-              implied_domain
-                  .AdditionWith(context_->DomainOf(ref).MultiplicationBy(
-                      -ct.linear().coeffs(i)))
-                  .RelaxIfTooComplex();
-        }
-        implied_domain = implied_domain.InverseMultiplicationBy(
-            objective_coeff_in_expanded_constraint);
-
-        // Remove the constraint if the implied domain is included in the
-        // domain of the objective_var term.
-        if (implied_domain.IsIncludedIn(context_->DomainOf(objective_var))) {
-          context_->MarkVariableAsRemoved(objective_var);
-          context_->UpdateRuleStats("objective: removed objective constraint.");
-          *(context_->mapping_model->add_constraints()) = ct;
-          context_->working_model->mutable_constraints(expanded_linear_index)
-              ->Clear();
-          context_->UpdateConstraintVariableUsage(expanded_linear_index);
-        } else {
-          unique_expanded_constraint = expanded_linear_index;
-        }
-      }
-
-      ++num_expansions;
-      last_expanded_objective_var = objective_var;
+      ++num_expands;
     }
   }
 
-  // Special case: If we just did one expansion of a single variable, then we
-  // can remove the expanded constraints if the objective wasn't used elsewhere.
-  if (num_expansions == 1 && objective_was_a_single_variable &&
-      unique_expanded_constraint != -1) {
-    context_->UpdateRuleStats(
-        "objective: removed unique objective constraint.");
-    ConstraintProto* mutable_ct = context_->working_model->mutable_constraints(
-        unique_expanded_constraint);
-    *(context_->mapping_model->add_constraints()) = *mutable_ct;
-    mutable_ct->Clear();
-    context_->MarkVariableAsRemoved(last_expanded_objective_var);
-    context_->UpdateConstraintVariableUsage(unique_expanded_constraint);
+  if (num_expands > 0) {
+    context_->UpdateRuleStats("objective: expanded via tight equality",
+                              num_expands);
   }
+  SOLVER_LOG(
+      logger_, "[ExpandObjective]", " #propagations=", num_propagations,
+      " #entries=", num_entries, " #tight_variables=", num_tight_variables,
+      " #tight_constraints=", num_tight_constraints, " #expands=", num_expands,
+      " #issues=", num_issues, " time=", wall_timer.Get(), "s");
 }
 
 void CpModelPresolver::MergeNoOverlapConstraints() {
@@ -9170,8 +9162,12 @@ void CpModelPresolver::ProcessVariableOnlyUsedInEncoding(int var) {
     const Domain rhs = ReadDomainFromProto(ct.linear())
                            .InverseMultiplicationBy(coeff)
                            .IntersectionWith(var_domain);
-
-    if (rhs.IsFixed()) {
+    if (rhs.IsEmpty()) {
+      if (!context_->SetLiteralToFalse(ct.enforcement_literal(0))) {
+        return;
+      }
+      return;
+    } else if (rhs.IsFixed()) {
       if (!var_domain.Contains(rhs.FixedValue())) {
         if (!context_->SetLiteralToFalse(ct.enforcement_literal(0))) {
           return;
diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h
index 5c3244ea86..fb470c80a2 100644
--- a/ortools/sat/cp_model_presolve.h
+++ b/ortools/sat/cp_model_presolve.h
@@ -246,6 +246,9 @@ class CpModelPresolver {
   // Converts bool_or and at_most_one of size 2 to bool_and.
   void ExtractBoolAnd();
 
+  // Try to reformulate the objective in term of "base" variables. This is
+  // mainly useful for core based approach where having more terms in the
+  // objective (but with a same trivial lower bound) should help.
   void ExpandObjective();
 
   void ProcessVariableOnlyUsedInEncoding(int var);
diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc
index 844a57adc2..01bbe4015f 100644
--- a/ortools/sat/cp_model_search.cc
+++ b/ortools/sat/cp_model_search.cc
@@ -641,6 +641,12 @@ std::vector<SatParameters> GetDiverseSetOfParameters(
     names.push_back("lb_tree_search");
     names.push_back("objective_lb_search");
     names.push_back("probing");
+    if (base_params.num_workers() >= 20) {
+      names.push_back("probing_max_lp");
+    }
+    if (base_params.num_workers() >= 24) {
+      names.push_back("objective_lb_search_max_lp");
+    }
 #if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP)
     if (absl::GetFlag(FLAGS_cp_model_use_max_hs)) names.push_back("max_hs");
 #endif  // !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP)
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index d0ecd155cd..097cf79a34 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -578,8 +578,7 @@ std::string CpSolverResponseStats(const CpSolverResponse& response,
   if (!response.solution().empty()) {
     absl::StrAppendFormat(
         &result, "\nsolution_fingerprint: %#x",
-        FingerprintRepeatedField(response.solution(),
-                                 uint64_t{0xa5b85c5e198ed849}));
+        FingerprintRepeatedField(response.solution(), kDefaultFingerprintSeed));
   }
   absl::StrAppend(&result, "\n");
   return result;
@@ -1693,10 +1692,6 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, Model* model) {
       } else {
         status = model->Mutable<CoreBasedOptimizer>()->Optimize();
       }
-    } else if (parameters.use_objective_lb_search()) {
-      ObjectiveLowerBoundScanner obj_lb_scanner(objective_var,
-                                                solution_observer, model);
-      status = obj_lb_scanner.ShaveObjectiveLowerBound();
     } else {
       // TODO(user): This parameter breaks the splitting in chunk of a Solve().
       // It should probably be moved into another SubSolver altogether.
diff --git a/ortools/sat/cp_model_utils.h b/ortools/sat/cp_model_utils.h
index dddf9aa8b2..9b30d31d8a 100644
--- a/ortools/sat/cp_model_utils.h
+++ b/ortools/sat/cp_model_utils.h
@@ -192,6 +192,9 @@ bool LinearExpressionProtosAreEqual(const LinearExpressionProto& a,
                                     const LinearExpressionProto& b,
                                     int64_t b_scaling = 1);
 
+// Default seed for fingerprints.
+constexpr uint64_t kDefaultFingerprintSeed = 0xa5b85c5e198ed849;
+
 // T must be castable to uint64_t.
 template <class T>
 inline uint64_t FingerprintRepeatedField(
@@ -211,7 +214,7 @@ uint64_t FingerprintExpression(const LinearExpressionProto& lin, uint64_t seed);
 
 // Returns a stable fingerprint of a model.
 uint64_t FingerprintModel(const CpModelProto& model,
-                          uint64_t seed = uint64_t{0xa5b85c5e198ed849});
+                          uint64_t seed = kDefaultFingerprintSeed);
 
 }  // namespace sat
 }  // namespace operations_research
diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc
index 56419ee0ec..b0b5fedda5 100644
--- a/ortools/sat/integer_search.cc
+++ b/ortools/sat/integer_search.cc
@@ -24,6 +24,7 @@
 #include "absl/strings/str_cat.h"
 #include "absl/time/clock.h"
 #include "absl/time/time.h"
+#include "ortools/base/check.h"
 #include "ortools/base/logging.h"
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_mapping.h"
@@ -340,6 +341,31 @@ std::function<BooleanOrIntegerLiteral()> SatSolverHeuristic(Model* model) {
   };
 }
 
+// TODO(user): Do we need a mechanism to reduce the range of possible gaps
+// when nothing gets proven? This could be a parameter or some adaptative code.
+std::function<BooleanOrIntegerLiteral()> ShaveObjectiveLb(Model* model) {
+  auto* objective_definition = model->GetOrCreate<ObjectiveDefinition>();
+  const IntegerVariable obj_var = objective_definition->objective_var;
+  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
+  auto* sat_solver = model->GetOrCreate<SatSolver>();
+  auto* random = model->GetOrCreate<ModelRandomGenerator>();
+
+  return [obj_var, integer_trail, sat_solver, random]() {
+    BooleanOrIntegerLiteral result;
+    const int level = sat_solver->CurrentDecisionLevel();
+    if (level > 0 || obj_var == kNoIntegerVariable) return result;
+
+    const IntegerValue obj_lb = integer_trail->LowerBound(obj_var);
+    const IntegerValue obj_ub = integer_trail->UpperBound(obj_var);
+    const IntegerValue mid = (obj_ub - obj_lb) / 2;
+    const IntegerValue new_ub =
+        obj_lb + absl::LogUniform<int64_t>(*random, 0, mid.value());
+
+    result.integer_literal = IntegerLiteral::LowerOrEqual(obj_var, new_ub);
+    return result;
+  };
+}
+
 std::function<BooleanOrIntegerLiteral()> PseudoCost(Model* model) {
   auto* objective = model->Get<ObjectiveDefinition>();
   const bool has_objective =
@@ -354,7 +380,7 @@ std::function<BooleanOrIntegerLiteral()> PseudoCost(Model* model) {
     const IntegerVariable chosen_var = pseudo_costs->GetBestDecisionVar();
     if (chosen_var == kNoIntegerVariable) return BooleanOrIntegerLiteral();
 
-    // TODO(user): This will be overidden by the value decision heuristic in
+    // TODO(user): This will be overridden by the value decision heuristic in
     // almost all cases.
     return BooleanOrIntegerLiteral(
         GreaterOrEqualToMiddleValue(chosen_var, integer_trail));
@@ -604,7 +630,7 @@ std::function<BooleanOrIntegerLiteral()> FollowHint(
   // even if we use this FollowHint() function just for a while. But it is
   // an easy solution to not have reference to deleted memory in the
   // RevIntRepository(). Note that once we backtrack, these reference will
-  // disapear.
+  // disappear.
   int* rev_start_index = model->TakeOwnership(new int);
   *rev_start_index = 0;
 
@@ -688,7 +714,12 @@ void ConfigureSearchHeuristics(Model* model) {
       decision_policy =
           SequentialSearch({decision_policy, heuristics.fixed_search});
       decision_policy = IntegerValueSelectionHeuristic(decision_policy, model);
-      heuristics.decision_policies = {decision_policy};
+      if (parameters.use_objective_lb_search()) {
+        heuristics.decision_policies = {
+            SequentialSearch({ShaveObjectiveLb(model), decision_policy})};
+      } else {
+        heuristics.decision_policies = {decision_policy};
+      }
       heuristics.restart_policies = {SatSolverRestartPolicy(model)};
       return;
     }
@@ -803,11 +834,13 @@ std::vector<std::function<BooleanOrIntegerLiteral()>> CompleteHeuristics(
 }
 
 IntegerSearchHelper::IntegerSearchHelper(Model* model)
-    : model_(model),
+    : parameters_(*model->GetOrCreate<SatParameters>()),
+      model_(model),
       sat_solver_(model->GetOrCreate<SatSolver>()),
       integer_trail_(model->GetOrCreate<IntegerTrail>()),
       encoder_(model->GetOrCreate<IntegerEncoder>()),
       implied_bounds_(model->GetOrCreate<ImpliedBounds>()),
+      prober_(model->GetOrCreate<Prober>()),
       product_detector_(model->GetOrCreate<ProductDetector>()),
       time_limit_(model->GetOrCreate<TimeLimit>()),
       pseudo_costs_(model->GetOrCreate<PseudoCosts>()) {
@@ -842,7 +875,7 @@ bool IntegerSearchHelper::BeforeTakingDecision() {
       }
     }
 
-    if (model_->GetOrCreate<SatParameters>()->use_sat_inprocessing() &&
+    if (parameters_.use_sat_inprocessing() &&
         !model_->GetOrCreate<Inprocessing>()->InprocessingRound()) {
       sat_solver_->NotifyThatModelIsUnsat();
       return false;
@@ -905,7 +938,7 @@ LiteralIndex IntegerSearchHelper::GetDecision(
 bool IntegerSearchHelper::TakeDecision(Literal decision) {
   // Record the changelist and objective bounds for updating pseudo costs.
   const std::vector<PseudoCosts::VariableBoundChange> bound_changes =
-      GetBoundChanges(decision.Index(), model_);
+      pseudo_costs_->GetBoundChanges(decision);
   IntegerValue old_obj_lb = kMinIntegerValue;
   IntegerValue old_obj_ub = kMaxIntegerValue;
   if (objective_var_ != kNoIntegerVariable) {
@@ -942,71 +975,56 @@ bool IntegerSearchHelper::TakeDecision(Literal decision) {
   return sat_solver_->ReapplyAssumptionsIfNeeded();
 }
 
-SatSolver::Status SolveIntegerProblem(Model* model) {
-  TimeLimit* time_limit = model->GetOrCreate<TimeLimit>();
-  if (time_limit->LimitReached()) return SatSolver::LIMIT_REACHED;
+SatSolver::Status IntegerSearchHelper::SolveIntegerProblem() {
+  if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;
 
-  SearchHeuristics& heuristics = *model->GetOrCreate<SearchHeuristics>();
+  SearchHeuristics& heuristics = *model_->GetOrCreate<SearchHeuristics>();
   const int num_policies = heuristics.decision_policies.size();
   CHECK_NE(num_policies, 0);
   CHECK_EQ(num_policies, heuristics.restart_policies.size());
 
-  auto* helper = model->GetOrCreate<IntegerSearchHelper>();
-
-  // This is needed for recording the pseudo-costs.
-  IntegerVariable objective_var = kNoIntegerVariable;
-  {
-    const ObjectiveDefinition* objective = model->Get<ObjectiveDefinition>();
-    if (objective != nullptr) objective_var = objective->objective_var;
-  }
-
   // Note that it is important to do the level-zero propagation if it wasn't
   // already done because EnqueueDecisionAndBackjumpOnConflict() assumes that
   // the solver is in a "propagated" state.
-  SatSolver* const sat_solver = model->GetOrCreate<SatSolver>();
-
+  //
   // TODO(user): We have the issue that at level zero. calling the propagation
   // loop more than once can propagate more! This is because we call the LP
   // again and again on each level zero propagation. This is causing some
   // CHECKs() to fail in multithread (rarely) because when we associate new
   // literals to integer ones, Propagate() is indirectly called. Not sure yet
   // how to fix.
-  if (!sat_solver->FinishPropagation()) return sat_solver->UnsatStatus();
-
-  auto* prober = model->GetOrCreate<Prober>();
-
-  const SatParameters& sat_parameters = *(model->GetOrCreate<SatParameters>());
+  if (!sat_solver_->FinishPropagation()) return sat_solver_->UnsatStatus();
 
   // Main search loop.
-  const int64_t old_num_conflicts = sat_solver->num_failures();
-  const int64_t conflict_limit = sat_parameters.max_number_of_conflicts();
+  const int64_t old_num_conflicts = sat_solver_->num_failures();
+  const int64_t conflict_limit = parameters_.max_number_of_conflicts();
   int64_t num_decisions_since_last_lp_record_ = 0;
   int64_t num_decisions_without_probing = 0;
-  while (!time_limit->LimitReached() &&
-         (sat_solver->num_failures() - old_num_conflicts < conflict_limit)) {
+  while (!time_limit_->LimitReached() &&
+         (sat_solver_->num_failures() - old_num_conflicts < conflict_limit)) {
     // If needed, restart and switch decision_policy.
     if (heuristics.restart_policies[heuristics.policy_index]()) {
-      if (!sat_solver->RestoreSolverToAssumptionLevel()) {
-        return sat_solver->UnsatStatus();
+      if (!sat_solver_->RestoreSolverToAssumptionLevel()) {
+        return sat_solver_->UnsatStatus();
       }
       heuristics.policy_index = (heuristics.policy_index + 1) % num_policies;
     }
 
-    if (!helper->BeforeTakingDecision()) return sat_solver->UnsatStatus();
+    if (!BeforeTakingDecision()) return sat_solver_->UnsatStatus();
 
     LiteralIndex decision = kNoLiteralIndex;
     while (true) {
       if (heuristics.next_decision_override != nullptr) {
         // Note that to properly count the num_times, we do not want to move
         // this function, but actually call that copy.
-        decision = helper->GetDecision(heuristics.next_decision_override);
+        decision = GetDecision(heuristics.next_decision_override);
         if (decision == kNoLiteralIndex) {
           heuristics.next_decision_override = nullptr;
         }
       }
       if (decision == kNoLiteralIndex) {
-        decision = helper->GetDecision(
-            heuristics.decision_policies[heuristics.policy_index]);
+        decision =
+            GetDecision(heuristics.decision_policies[heuristics.policy_index]);
       }
 
       // Probing?
@@ -1014,19 +1032,19 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
       // TODO(user): Be smarter about what variables we probe, we can
       // also do more than one.
       if (decision != kNoLiteralIndex &&
-          sat_solver->CurrentDecisionLevel() == 0 &&
-          sat_parameters.probing_period_at_root() > 0 &&
+          sat_solver_->CurrentDecisionLevel() == 0 &&
+          parameters_.probing_period_at_root() > 0 &&
           ++num_decisions_without_probing >=
-              sat_parameters.probing_period_at_root()) {
+              parameters_.probing_period_at_root()) {
         num_decisions_without_probing = 0;
-        if (!prober->ProbeOneVariable(Literal(decision).Variable())) {
+        if (!prober_->ProbeOneVariable(Literal(decision).Variable())) {
           return SatSolver::INFEASIBLE;
         }
-        DCHECK_EQ(sat_solver->CurrentDecisionLevel(), 0);
+        DCHECK_EQ(sat_solver_->CurrentDecisionLevel(), 0);
 
         // We need to check after the probing that the literal is not fixed,
         // otherwise we just go to the next decision.
-        if (sat_solver->Assignment().LiteralIsAssigned(Literal(decision))) {
+        if (sat_solver_->Assignment().LiteralIsAssigned(Literal(decision))) {
           continue;
         }
       }
@@ -1040,7 +1058,7 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
     // all variables are fixed, there is no guarantee that the propagation
     // responsible for testing the validity of the solution was run to
     // completion. So we cannot report a feasible solution.
-    if (time_limit->LimitReached()) return SatSolver::LIMIT_REACHED;
+    if (time_limit_->LimitReached()) return SatSolver::LIMIT_REACHED;
     if (decision == kNoLiteralIndex) {
       // Save the current polarity of all Booleans in the solution. It will be
       // followed for the next SAT decisions. This is known to be a good policy
@@ -1050,9 +1068,9 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
       // This idea is kind of "well known", see for instance the "LinSBPS"
       // submission to the maxSAT 2018 competition by Emir Demirovic and Peter
       // Stuckey where they show it is a good idea and provide more references.
-      if (model->GetOrCreate<SatParameters>()->use_optimization_hints()) {
-        auto* sat_decision = model->GetOrCreate<SatDecisionPolicy>();
-        const auto& trail = *model->GetOrCreate<Trail>();
+      if (parameters_.use_optimization_hints()) {
+        auto* sat_decision = model_->GetOrCreate<SatDecisionPolicy>();
+        const auto& trail = *model_->GetOrCreate<Trail>();
         for (int i = 0; i < trail.Index(); ++i) {
           sat_decision->SetAssignmentPreference(trail[i], 0.0);
         }
@@ -1060,8 +1078,8 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
       return SatSolver::FEASIBLE;
     }
 
-    if (!helper->TakeDecision(Literal(decision))) {
-      return sat_solver->UnsatStatus();
+    if (!TakeDecision(Literal(decision))) {
+      return sat_solver_->UnsatStatus();
     }
 
     // In multi-thread, we really only want to save the LP relaxation for thread
@@ -1076,14 +1094,14 @@ SatSolver::Status SolveIntegerProblem(Model* model) {
     // change. Avoid adding solution that are too deep in the tree (most
     // variable fixed). Also use a callback rather than having this here, we
     // don't want this file to depend on cp_model.proto.
-    if (model->Get<SharedLPSolutionRepository>() != nullptr &&
-        sat_parameters.linearization_level() >= 2) {
+    if (model_->Get<SharedLPSolutionRepository>() != nullptr &&
+        parameters_.linearization_level() >= 2) {
       num_decisions_since_last_lp_record_++;
       if (num_decisions_since_last_lp_record_ >= 100) {
         // NOTE: We can actually record LP solutions more frequently. However
         // this process is time consuming and workers waste a lot of time doing
         // this. To avoid this we don't record solutions after each decision.
-        RecordLPRelaxationValues(model);
+        RecordLPRelaxationValues(model_);
         num_decisions_since_last_lp_record_ = 0;
       }
     }
@@ -1109,7 +1127,7 @@ SatSolver::Status ResetAndSolveIntegerProblem(
   if (!solver->ResetWithGivenAssumptions(assumptions)) {
     return solver->UnsatStatus();
   }
-  return SolveIntegerProblem(model);
+  return model->GetOrCreate<IntegerSearchHelper>()->SolveIntegerProblem();
 }
 
 SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model) {
@@ -1331,6 +1349,7 @@ SatSolver::Status ContinuousProber::ShaveLiteral(Literal literal) {
   const SatSolver::Status status =
       ResetAndSolveIntegerProblem({literal}, model_);
   time_limit_->ChangeDeterministicLimit(original_dtime_limit);
+  if (ReportStatus(status)) return status;
 
   if (status == SatSolver::ASSUMPTIONS_UNSAT) {
     num_bounds_shaved_++;
diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h
index 73611dfc19..e89dcce681 100644
--- a/ortools/sat/integer_search.h
+++ b/ortools/sat/integer_search.h
@@ -110,17 +110,6 @@ struct LevelZeroCallbackHelper {
   std::vector<std::function<bool()>> callbacks;
 };
 
-// Tries to find a feasible solution to the current model.
-//
-// This function continues from the current state of the solver and loop until
-// all variables are instantiated (i.e. the next decision is kNoLiteralIndex) or
-// a search limit is reached. It uses the heuristic from the SearchHeuristics
-// class in the model to decide when to restart and what next decision to take.
-//
-// Each time a restart happen, this increment the policy index modulo the number
-// of heuristics to act as a portfolio search.
-SatSolver::Status SolveIntegerProblem(Model* model);
-
 // Resets the solver to the given assumptions before calling
 // SolveIntegerProblem().
 SatSolver::Status ResetAndSolveIntegerProblem(
@@ -267,12 +256,26 @@ class IntegerSearchHelper {
   // Returns false if the model is UNSAT.
   bool TakeDecision(Literal decision);
 
+  // Tries to find a feasible solution to the current model.
+  //
+  // This function continues from the current state of the solver and loop until
+  // all variables are instantiated (i.e. the next decision is kNoLiteralIndex)
+  // or a search limit is reached. It uses the heuristic from the
+  // SearchHeuristics class in the model to decide when to restart and what next
+  // decision to take.
+  //
+  // Each time a restart happen, this increment the policy index modulo the
+  // number of heuristics to act as a portfolio search.
+  SatSolver::Status SolveIntegerProblem();
+
  private:
+  const SatParameters& parameters_;
   Model* model_;
   SatSolver* sat_solver_;
   IntegerTrail* integer_trail_;
   IntegerEncoder* encoder_;
   ImpliedBounds* implied_bounds_;
+  Prober* prober_;
   ProductDetector* product_detector_;
   TimeLimit* time_limit_;
   PseudoCosts* pseudo_costs_;
diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc
index 57cc728865..53edd0486c 100644
--- a/ortools/sat/optimization.cc
+++ b/ortools/sat/optimization.cc
@@ -1074,14 +1074,15 @@ SatSolver::Status SolveWithCardinalityEncodingAndCore(
 SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding(
     IntegerVariable objective_var,
     const std::function<void()>& feasible_solution_observer, Model* model) {
-  SatSolver* sat_solver = model->GetOrCreate<SatSolver>();
-  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
+  auto* sat_solver = model->GetOrCreate<SatSolver>();
+  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
+  auto* search = model->GetOrCreate<IntegerSearchHelper>();
   const SatParameters& parameters = *(model->GetOrCreate<SatParameters>());
 
   // Simple linear scan algorithm to find the optimal.
   if (!sat_solver->ResetToLevelZero()) return SatSolver::INFEASIBLE;
   while (true) {
-    const SatSolver::Status result = SolveIntegerProblem(model);
+    const SatSolver::Status result = search->SolveIntegerProblem();
     if (result != SatSolver::FEASIBLE) return result;
 
     // The objective is the current lower bound of the objective_var.
@@ -2117,90 +2118,5 @@ SatSolver::Status CoreBasedOptimizer::Optimize() {
   }
 }
 
-ObjectiveLowerBoundScanner::ObjectiveLowerBoundScanner(
-    IntegerVariable objective_var,
-    const std::function<void()>& feasible_solution_observer, Model* model)
-    : model_(model),
-      sat_solver_(model->GetOrCreate<SatSolver>()),
-      time_limit_(model->GetOrCreate<TimeLimit>()),
-      integer_trail_(model->GetOrCreate<IntegerTrail>()),
-      encoder_(model->GetOrCreate<IntegerEncoder>()),
-      parameters_(*(model->GetOrCreate<SatParameters>())),
-      level_zero_callbacks_(model->GetOrCreate<LevelZeroCallbackHelper>()),
-      shared_response_manager_(model->Mutable<SharedResponseManager>()),
-      objective_var_(objective_var),
-      feasible_solution_observer_(feasible_solution_observer) {}
-
-SatSolver::Status ObjectiveLowerBoundScanner::ShaveObjectiveLowerBound() {
-  while (!time_limit_->LimitReached()) {
-    if (time_limit_->LimitReached()) {
-      return SatSolver::LIMIT_REACHED;
-    }
-
-    if (!sat_solver_->ResetToLevelZero()) return SatSolver::INFEASIBLE;
-    for (const auto& cb : level_zero_callbacks_->callbacks) {
-      if (!cb()) {
-        sat_solver_->NotifyThatModelIsUnsat();
-        return SatSolver::INFEASIBLE;
-      }
-    }
-
-    const IntegerValue lb = integer_trail_->LowerBound(objective_var_);
-    const IntegerValue ub = integer_trail_->UpperBound(objective_var_);
-    VLOG(2) << "   lb = " << lb << ", ub = " << ub;
-
-    const Literal assumption = encoder_->GetOrCreateAssociatedLiteral(
-        IntegerLiteral::LowerOrEqual(objective_var_, lb));
-    const SatSolver::Status status =
-        ResetAndSolveIntegerProblem({assumption}, model_);
-
-    switch (status) {
-      case SatSolver::INFEASIBLE: {
-        return SatSolver::INFEASIBLE;
-      }
-      case SatSolver::ASSUMPTIONS_UNSAT: {
-        shared_response_manager_->UpdateInnerObjectiveBounds(
-            absl::StrCat(model_->Name(), " #iteration=", iteration_), lb + 1,
-            ub);
-        // Update the objective lower bound.
-        const IntegerValue new_lb = integer_trail_->LowerBound(objective_var_);
-        sat_solver_->Backtrack(0);
-        if (!integer_trail_->Enqueue(
-                IntegerLiteral::GreaterOrEqual(objective_var_,
-                                               std::max(new_lb, lb + 1)),
-                {}, {})) {
-          return SatSolver::INFEASIBLE;
-        }
-        break;
-      }
-      case SatSolver::FEASIBLE: {
-        if (feasible_solution_observer_ != nullptr) {
-          feasible_solution_observer_();
-        }
-
-        // The objective is the current lower bound of the objective_var.
-        const IntegerValue objective_value =
-            integer_trail_->LowerBound(objective_var_);
-
-        // We have a solution, restrict the objective upper bound to only look
-        // for better ones now.
-        sat_solver_->Backtrack(0);
-        if (!integer_trail_->Enqueue(IntegerLiteral::LowerOrEqual(
-                                         objective_var_, objective_value - 1),
-                                     {}, {})) {
-          return SatSolver::INFEASIBLE;
-        }
-        break;
-      }
-      case SatSolver::LIMIT_REACHED: {
-        return SatSolver::LIMIT_REACHED;
-      }
-    }
-    iteration_++;
-  }
-
-  return SatSolver::LIMIT_REACHED;
-}
-
 }  // namespace sat
 }  // namespace operations_research
diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h
index ffbc2da036..5dfdbf2ca1 100644
--- a/ortools/sat/optimization.h
+++ b/ortools/sat/optimization.h
@@ -257,41 +257,6 @@ class CoreBasedOptimizer {
   bool stop_ = false;
 };
 
-// This class will scan the objective up from its minimal value to increase the
-// objective lower bound.
-//
-// TODO(user): Implement an acceleration schema in the LB improvements.
-class ObjectiveLowerBoundScanner {
- public:
-  ObjectiveLowerBoundScanner(
-      IntegerVariable objective_var,
-      const std::function<void()>& feasible_solution_observer, Model* model);
-
-  // Tries to shave the lower bound of the objective.
-  // It returns:
-  //   - SatSolver::INFEASIBLE if the search is done. If the solution observer
-  //     was called this actually means optimal, otherwise it means there is no
-  //     solution and it is a true infeasibility.
-  //   - SatSolver::LIMIT_REACHED if the limit stored in the model is reached.
-  SatSolver::Status ShaveObjectiveLowerBound();
-
- private:
-  // Model object.
-  Model* model_;
-  SatSolver* sat_solver_;
-  TimeLimit* time_limit_;
-  IntegerTrail* integer_trail_;
-  IntegerEncoder* encoder_;
-  const SatParameters parameters_;
-  LevelZeroCallbackHelper* level_zero_callbacks_;
-  SharedResponseManager* shared_response_manager_;
-  const IntegerVariable objective_var_;
-  const std::function<void()> feasible_solution_observer_;
-
-  // Current state of the scan.
-  int iteration_ = 0;
-};
-
 }  // namespace sat
 }  // namespace operations_research
 
diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc
index c0e01cfc76..c4e15db690 100644
--- a/ortools/sat/presolve_context.cc
+++ b/ortools/sat/presolve_context.cc
@@ -1742,12 +1742,10 @@ bool PresolveContext::AddToObjectiveOffset(int64_t delta) {
 
 bool PresolveContext::SubstituteVariableInObjective(
     int var_in_equality, int64_t coeff_in_equality,
-    const ConstraintProto& equality, std::vector<int>* new_vars_in_objective) {
+    const ConstraintProto& equality) {
   CHECK(equality.enforcement_literal().empty());
   CHECK(RefIsPositive(var_in_equality));
 
-  if (new_vars_in_objective != nullptr) new_vars_in_objective->clear();
-
   // We can only "easily" substitute if the objective coefficient is a multiple
   // of the one in the constraint.
   const int64_t coeff_in_objective = objective_map_.at(var_in_equality);
@@ -1796,9 +1794,6 @@ bool PresolveContext::SubstituteVariableInObjective(
     if (var == var_in_equality) continue;
 
     int64_t& map_ref = objective_map_[var];
-    if (map_ref == 0 && new_vars_in_objective != nullptr) {
-      new_vars_in_objective->push_back(var);
-    }
     map_ref -= coeff * multiplier;
 
     if (map_ref == 0) {
diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h
index 477804cd3f..b6904fa237 100644
--- a/ortools/sat/presolve_context.h
+++ b/ortools/sat/presolve_context.h
@@ -439,10 +439,6 @@ class PresolveContext {
   // objective, remove it from the objective by transferring its cost to other
   // variables in the equality.
   //
-  // If new_vars_in_objective is not nullptr, it will be filled with "new"
-  // variables that where not in the objective before and are after
-  // substitution.
-  //
   // Returns false, if the substitution cannot be done. This is the case if the
   // model become UNSAT or if doing it will result in an objective that do not
   // satisfy our overflow preconditions. Note that this can only happen if the
@@ -450,8 +446,7 @@ class PresolveContext {
   // the implied domain from the equality).
   ABSL_MUST_USE_RESULT bool SubstituteVariableInObjective(
       int var_in_equality, int64_t coeff_in_equality,
-      const ConstraintProto& equality,
-      std::vector<int>* new_vars_in_objective = nullptr);
+      const ConstraintProto& equality);
 
   // Objective getters.
   const Domain& ObjectiveDomain() const { return objective_domain_; }
diff --git a/ortools/sat/pseudo_costs.cc b/ortools/sat/pseudo_costs.cc
index 0a0d85d00c..5987cf642f 100644
--- a/ortools/sat/pseudo_costs.cc
+++ b/ortools/sat/pseudo_costs.cc
@@ -30,9 +30,10 @@ namespace operations_research {
 namespace sat {
 
 PseudoCosts::PseudoCosts(Model* model)
-    : integer_trail_(*model->GetOrCreate<IntegerTrail>()),
-      parameters_(*model->GetOrCreate<SatParameters>()) {
-  const int num_vars = integer_trail_.NumIntegerVariables().value();
+    : parameters_(*model->GetOrCreate<SatParameters>()),
+      integer_trail_(model->GetOrCreate<IntegerTrail>()),
+      encoder_(model->GetOrCreate<IntegerEncoder>()) {
+  const int num_vars = integer_trail_->NumIntegerVariables().value();
   pseudo_costs_.resize(num_vars);
 }
 
@@ -53,7 +54,7 @@ void PseudoCosts::UpdateCost(
   if (obj_bound_improvement == IntegerValue(0)) return;
 
   for (const VariableBoundChange& decision : bound_changes) {
-    if (integer_trail_.IsCurrentlyIgnored(decision.var)) continue;
+    if (integer_trail_->IsCurrentlyIgnored(decision.var)) continue;
     if (decision.lower_bound_change == IntegerValue(0)) continue;
 
     const double current_pseudo_cost =
@@ -73,9 +74,9 @@ IntegerVariable PseudoCosts::GetBestDecisionVar() {
   for (IntegerVariable positive_var(0); positive_var < pseudo_costs_.size();
        positive_var += 2) {
     const IntegerVariable negative_var = NegationOf(positive_var);
-    if (integer_trail_.IsCurrentlyIgnored(positive_var)) continue;
-    const IntegerValue lb = integer_trail_.LowerBound(positive_var);
-    const IntegerValue ub = integer_trail_.UpperBound(positive_var);
+    if (integer_trail_->IsCurrentlyIgnored(positive_var)) continue;
+    const IntegerValue lb = integer_trail_->LowerBound(positive_var);
+    const IntegerValue ub = integer_trail_->UpperBound(positive_var);
     if (lb >= ub) continue;
     if (GetRecordings(positive_var) + GetRecordings(negative_var) <
         parameters_.pseudo_cost_reliability_threshold()) {
@@ -101,21 +102,18 @@ IntegerVariable PseudoCosts::GetBestDecisionVar() {
   return chosen_var;
 }
 
-std::vector<PseudoCosts::VariableBoundChange> GetBoundChanges(
-    LiteralIndex decision, Model* model) {
+std::vector<PseudoCosts::VariableBoundChange> PseudoCosts::GetBoundChanges(
+    Literal decision) {
   std::vector<PseudoCosts::VariableBoundChange> bound_changes;
-  if (decision == kNoLiteralIndex) return bound_changes;
-  auto* encoder = model->GetOrCreate<IntegerEncoder>();
-  auto* integer_trail = model->GetOrCreate<IntegerTrail>();
+
   // NOTE: We ignore negation of equality decisions.
-  for (const IntegerLiteral l :
-       encoder->GetAllIntegerLiterals(Literal(decision))) {
+  for (const IntegerLiteral l : encoder_->GetAllIntegerLiterals(decision)) {
     if (l.var == kNoIntegerVariable) continue;
-    if (integer_trail->IsCurrentlyIgnored(l.var)) continue;
+    if (integer_trail_->IsCurrentlyIgnored(l.var)) continue;
     PseudoCosts::VariableBoundChange var_bound_change;
     var_bound_change.var = l.var;
     var_bound_change.lower_bound_change =
-        l.bound - integer_trail->LowerBound(l.var);
+        l.bound - integer_trail_->LowerBound(l.var);
     bound_changes.push_back(var_bound_change);
   }
 
diff --git a/ortools/sat/pseudo_costs.h b/ortools/sat/pseudo_costs.h
index 9fa9f87651..ae951cffad 100644
--- a/ortools/sat/pseudo_costs.h
+++ b/ortools/sat/pseudo_costs.h
@@ -60,23 +60,22 @@ class PseudoCosts {
     return pseudo_costs_[var].NumRecords();
   }
 
+  // Returns extracted information to update pseudo costs from the given
+  // branching decision.
+  std::vector<VariableBoundChange> GetBoundChanges(Literal decision);
+
  private:
   // Updates the cost of a given variable.
   void UpdateCostForVar(IntegerVariable var, double new_cost);
 
   // Reference of integer trail to access the current bounds of variables.
-  const IntegerTrail& integer_trail_;
-
   const SatParameters& parameters_;
+  IntegerTrail* integer_trail_;
+  IntegerEncoder* encoder_;
 
   absl::StrongVector<IntegerVariable, IncrementalAverage> pseudo_costs_;
 };
 
-// Returns extracted information to update pseudo costs from the given
-// branching decision.
-std::vector<PseudoCosts::VariableBoundChange> GetBoundChanges(
-    LiteralIndex decision, Model* model);
-
 }  // namespace sat
 }  // namespace operations_research
 
diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto
index 998af756a4..cc55fa1ec9 100644
--- a/ortools/sat/sat_parameters.proto
+++ b/ortools/sat/sat_parameters.proto
@@ -727,6 +727,9 @@ message SatParameters {
   // Create one literal for each disjunction of two pairs of tasks. This slows
   // down the solve time, but improves the lower bound of the objective in the
   // makespan case.
+  //
+  // Do not use if you have many tasks in one of your disjunctive since this
+  // creates O(#tasks^2) extra Booleans.
   optional bool create_precedence_literals_in_disjunctive_constraint = 229
       [default = false];