[CP-SAT] rewrite probing search; fix bug with missing propagation on the first binary clause learned

2022-02-05 10:39:14 +01:00
parent 03f6e01de7
commit ac28232456
11 changed files with 355 additions and 239 deletions
--- a/ortools/sat/clause.h
+++ b/ortools/sat/clause.h
@@ -479,7 +479,9 @@ class BinaryImplicationGraph : public SatPropagator {
  void Resize(int num_variables);

  // Returns true if there is no constraints in this class.
-  bool IsEmpty() { return num_implications_ == 0 && at_most_ones_.empty(); }
+  bool IsEmpty() const final {
+    return num_implications_ == 0 && at_most_ones_.empty();
+  }

  // Adds the binary clause (a OR b), which is the same as (not a => b).
  // Note that it is also equivalent to (not b => a).
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -79,9 +79,9 @@ void CpModelPresolver::RemoveEmptyConstraints() {
      context_->working_model->constraints_size();
  for (int c = 0; c < old_num_non_empty_constraints; ++c) {
    const auto type = context_->working_model->constraints(c).constraint_case();
-    if (type == ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) continue;
-    if (type == ConstraintProto::ConstraintCase::kDummyConstraint) continue;
-    if (type == ConstraintProto::ConstraintCase::kInterval) {
+    if (type == ConstraintProto::CONSTRAINT_NOT_SET) continue;
+    if (type == ConstraintProto::kDummyConstraint) continue;
+    if (type == ConstraintProto::kInterval) {
      interval_mapping[c] = new_num_constraints;
    }
    context_->working_model->mutable_constraints(new_num_constraints++)
@@ -1279,13 +1279,15 @@ bool CpModelPresolver::PresolveIntMod(ConstraintProto* ct) {
  return false;
 }

+// TODO(user): Now that everything has affine relations, we should maybe
+// canonicalize all linear subexpression in an generic way.
 bool CpModelPresolver::ExploitEquivalenceRelations(int c, ConstraintProto* ct) {
  bool changed = false;

  // Optim: Special case for the linear constraint. We just remap the
  // enforcement literals, the normal variables will be replaced by their
  // representative in CanonicalizeLinear().
-  if (ct->constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
+  if (ct->constraint_case() == ConstraintProto::kLinear) {
    for (int& ref : *ct->mutable_enforcement_literal()) {
      const int rep = this->context_->GetLiteralRepresentative(ref);
      if (rep != ref) {
@@ -1308,17 +1310,6 @@ bool CpModelPresolver::ExploitEquivalenceRelations(int c, ConstraintProto* ct) {
  }
  if (!work_to_do) return false;

-  // Remap equal and negated variables to their representative.
-  ApplyToAllVariableIndices(
-      [&changed, this](int* ref) {
-        const int rep = context_->GetVariableRepresentative(*ref);
-        if (rep != *ref) {
-          changed = true;
-          *ref = rep;
-        }
-      },
-      ct);
-
  // Remap literal and negated literal to their representative.
  ApplyToAllLiteralIndices(
      [&changed, this](int* ref) {
@@ -1461,10 +1452,8 @@ bool CpModelPresolver::CanonicalizeLinearExpression(
 }

 bool CpModelPresolver::CanonicalizeLinear(ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
-      context_->ModelIsUnsat()) {
-    return false;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return false;
+  if (context_->ModelIsUnsat()) return false;

  if (ct->linear().domain().empty()) {
    context_->UpdateRuleStats("linear: no domain");
@@ -1484,7 +1473,7 @@ bool CpModelPresolver::CanonicalizeLinear(ConstraintProto* ct) {
 }

 bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
+  if (ct->constraint_case() != ConstraintProto::kLinear ||
      context_->ModelIsUnsat()) {
    return false;
  }
@@ -2169,9 +2158,7 @@ void TakeIntersectionWith(const absl::flat_hash_set<int>& current,

 bool CpModelPresolver::DetectAndProcessOneSidedLinearConstraint(
    int c, ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
-    return false;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return false;
  if (context_->ModelIsUnsat()) return false;
  if (context_->keep_all_feasible_solutions) return false;

@@ -2290,10 +2277,8 @@ bool CpModelPresolver::DetectAndProcessOneSidedLinearConstraint(

 bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
                                                ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
-      context_->ModelIsUnsat()) {
-    return false;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return false;
+  if (context_->ModelIsUnsat()) return false;

  // Compute the implied rhs bounds from the variable ones.
  auto& term_domains = context_->tmp_term_domains;
@@ -2469,7 +2454,7 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
      }
      if (c == ct_index) continue;
      if (context_->working_model->constraints(c).constraint_case() !=
-          ConstraintProto::ConstraintCase::kLinear) {
+          ConstraintProto::kLinear) {
        abort = true;
        break;
      }
@@ -2548,10 +2533,8 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
 // This operation is similar to coefficient strengthening in the MIP world.
 void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint(
    int ct_index, ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
-      context_->ModelIsUnsat()) {
-    return;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return;
+  if (context_->ModelIsUnsat()) return;

  const LinearConstraintProto& arg = ct->linear();
  const int num_vars = arg.vars_size();
@@ -2624,7 +2607,9 @@ void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint(
                      new_ct2->mutable_linear());

    context_->UpdateNewConstraintsVariableUsage();
-    return (void)RemoveConstraint(ct);
+    ct->Clear();
+    context_->UpdateConstraintVariableUsage(ct_index);
+    return;
  }

  // Any coefficient greater than this will cause the constraint to be trivially
@@ -2751,10 +2736,8 @@ void CpModelPresolver::ExtractAtMostOneFromLinear(ConstraintProto* ct) {
 // Convert some linear constraint involving only Booleans to their Boolean
 // form.
 bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
-      context_->ModelIsUnsat()) {
-    return false;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return false;
+  if (context_->ModelIsUnsat()) return false;

  const LinearConstraintProto& arg = ct->linear();
  const int num_vars = arg.vars_size();
@@ -4969,7 +4952,7 @@ void CpModelPresolver::ExtractBoolAnd() {
    const ConstraintProto& ct = context_->working_model->constraints(c);
    if (HasEnforcementLiteral(ct)) continue;

-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr &&
+    if (ct.constraint_case() == ConstraintProto::kBoolOr &&
        ct.bool_or().literals().size() == 2) {
      AddImplication(NegatedRef(ct.bool_or().literals(0)),
                     ct.bool_or().literals(1), context_->working_model,
@@ -4978,7 +4961,7 @@ void CpModelPresolver::ExtractBoolAnd() {
      continue;
    }

-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne &&
+    if (ct.constraint_case() == ConstraintProto::kAtMostOne &&
        ct.at_most_one().literals().size() == 2) {
      AddImplication(ct.at_most_one().literals(0),
                     NegatedRef(ct.at_most_one().literals(1)),
@@ -5100,8 +5083,8 @@ void CpModelPresolver::PresolvePureSatPart() {
  // reach this point?
  for (int c = 0; c < context_->working_model->constraints_size(); ++c) {
    const ConstraintProto& ct = context_->working_model->constraints(c);
-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr ||
-        ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolAnd) {
+    if (ct.constraint_case() == ConstraintProto::kBoolOr ||
+        ct.constraint_case() == ConstraintProto::kBoolAnd) {
      if (PresolveOneConstraint(c)) {
        context_->UpdateConstraintVariableUsage(c);
      }
@@ -5125,7 +5108,7 @@ void CpModelPresolver::PresolvePureSatPart() {
  for (int i = 0; i < context_->working_model->constraints_size(); ++i) {
    const ConstraintProto& ct = context_->working_model->constraints(i);

-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
+    if (ct.constraint_case() == ConstraintProto::kBoolOr) {
      ++num_removed_constraints;
      clause.clear();
      for (const int ref : ct.bool_or().literals()) {
@@ -5141,7 +5124,7 @@ void CpModelPresolver::PresolvePureSatPart() {
      continue;
    }

-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolAnd) {
+    if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
      ++num_removed_constraints;
      std::vector<Literal> clause;
      for (const int ref : ct.enforcement_literal()) {
@@ -5265,7 +5248,7 @@ void CpModelPresolver::ExpandObjective() {
    const ConstraintProto& ct = context_->working_model->constraints(ct_index);
    // Skip everything that is not a linear equality constraint.
    if (!ct.enforcement_literal().empty() ||
-        ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
+        ct.constraint_case() != ConstraintProto::kLinear ||
        ct.linear().domain().size() != 2 ||
        ct.linear().domain(0) != ct.linear().domain(1)) {
      continue;
@@ -5472,9 +5455,7 @@ void CpModelPresolver::MergeNoOverlapConstraints() {
  std::vector<std::vector<Literal>> cliques;
  for (int c = 0; c < num_constraints; ++c) {
    const ConstraintProto& ct = context_->working_model->constraints(c);
-    if (ct.constraint_case() != ConstraintProto::ConstraintCase::kNoOverlap) {
-      continue;
-    }
+    if (ct.constraint_case() != ConstraintProto::kNoOverlap) continue;
    std::vector<Literal> clique;
    for (const int i : ct.no_overlap().intervals()) {
      clique.push_back(Literal(BooleanVariable(i), true));
@@ -5545,7 +5526,7 @@ void CpModelPresolver::TransformIntoMaxCliques() {

  for (int c = 0; c < num_constraints; ++c) {
    ConstraintProto* ct = context_->working_model->mutable_constraints(c);
-    if (ct->constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne) {
+    if (ct->constraint_case() == ConstraintProto::kAtMostOne) {
      std::vector<Literal> clique;
      for (const int ref : ct->at_most_one().literals()) {
        clique.push_back(convert(ref));
@@ -5554,8 +5535,7 @@ void CpModelPresolver::TransformIntoMaxCliques() {
      if (RemoveConstraint(ct)) {
        context_->UpdateConstraintVariableUsage(c);
      }
-    } else if (ct->constraint_case() ==
-               ConstraintProto::ConstraintCase::kBoolAnd) {
+    } else if (ct->constraint_case() == ConstraintProto::kBoolAnd) {
      if (ct->enforcement_literal().size() != 1) continue;
      const Literal enforcement = convert(ct->enforcement_literal(0));
      for (const int ref : ct->bool_and().literals()) {
@@ -5679,17 +5659,17 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {

  // Call the presolve function for this constraint if any.
  switch (ct->constraint_case()) {
-    case ConstraintProto::ConstraintCase::kBoolOr:
+    case ConstraintProto::kBoolOr:
      return PresolveBoolOr(ct);
-    case ConstraintProto::ConstraintCase::kBoolAnd:
+    case ConstraintProto::kBoolAnd:
      return PresolveBoolAnd(ct);
-    case ConstraintProto::ConstraintCase::kAtMostOne:
+    case ConstraintProto::kAtMostOne:
      return PresolveAtMostOne(ct);
-    case ConstraintProto::ConstraintCase::kExactlyOne:
+    case ConstraintProto::kExactlyOne:
      return PresolveExactlyOne(ct);
-    case ConstraintProto::ConstraintCase::kBoolXor:
+    case ConstraintProto::kBoolXor:
      return PresolveBoolXor(ct);
-    case ConstraintProto::ConstraintCase::kLinMax:
+    case ConstraintProto::kLinMax:
      if (CanonicalizeLinearArgument(*ct, ct->mutable_lin_max())) {
        context_->UpdateConstraintVariableUsage(c);
      }
@@ -5698,22 +5678,22 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
      } else {
        return PresolveLinMax(ct);
      }
-    case ConstraintProto::ConstraintCase::kIntProd:
+    case ConstraintProto::kIntProd:
      if (CanonicalizeLinearArgument(*ct, ct->mutable_int_prod())) {
        context_->UpdateConstraintVariableUsage(c);
      }
      return PresolveIntProd(ct);
-    case ConstraintProto::ConstraintCase::kIntDiv:
+    case ConstraintProto::kIntDiv:
      if (CanonicalizeLinearArgument(*ct, ct->mutable_int_div())) {
        context_->UpdateConstraintVariableUsage(c);
      }
      return PresolveIntDiv(ct);
-    case ConstraintProto::ConstraintCase::kIntMod:
+    case ConstraintProto::kIntMod:
      if (CanonicalizeLinearArgument(*ct, ct->mutable_int_mod())) {
        context_->UpdateConstraintVariableUsage(c);
      }
      return PresolveIntMod(ct);
-    case ConstraintProto::ConstraintCase::kLinear: {
+    case ConstraintProto::kLinear: {
      // In the presence of affine relation, it is possible that the sign of a
      // variable change during canonicalization, and a variable that could
      // freely move in one direction can no longer do so. So we make sure we
@@ -5756,16 +5736,15 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
      if (PresolveLinearOnBooleans(ct)) {
        context_->UpdateConstraintVariableUsage(c);
      }
-      if (ct->constraint_case() == ConstraintProto::kLinear) {
-        const int old_num_enforcement_literals = ct->enforcement_literal_size();
-        ExtractEnforcementLiteralFromLinearConstraint(c, ct);
-        if (ct->constraint_case() ==
-            ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
+
+      // If we extracted some enforcement, we redo some preoslve.
+      const int old_num_enforcement_literals = ct->enforcement_literal_size();
+      ExtractEnforcementLiteralFromLinearConstraint(c, ct);
+      if (ct->enforcement_literal_size() > old_num_enforcement_literals) {
+        if (DivideLinearByGcd(ct)) {
          context_->UpdateConstraintVariableUsage(c);
-          return true;
        }
-        if (ct->enforcement_literal_size() > old_num_enforcement_literals &&
-            PresolveSmallLinear(ct)) {
+        if (PresolveSmallLinear(ct)) {
          context_->UpdateConstraintVariableUsage(c);
        }
      }
@@ -5773,35 +5752,34 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
      // Note that it is important for this to be last, so that if a constraint
      // is marked as being in one direction, no other presolve is applied until
      // it is processed again and unmarked at the beginning of this case.
-      if (ct->constraint_case() == ConstraintProto::kLinear &&
-          DetectAndProcessOneSidedLinearConstraint(c, ct)) {
+      if (DetectAndProcessOneSidedLinearConstraint(c, ct)) {
        context_->UpdateConstraintVariableUsage(c);
      }
      return false;
    }
-    case ConstraintProto::ConstraintCase::kInterval:
+    case ConstraintProto::kInterval:
      return PresolveInterval(c, ct);
-    case ConstraintProto::ConstraintCase::kInverse:
+    case ConstraintProto::kInverse:
      return PresolveInverse(ct);
-    case ConstraintProto::ConstraintCase::kElement:
+    case ConstraintProto::kElement:
      return PresolveElement(ct);
-    case ConstraintProto::ConstraintCase::kTable:
+    case ConstraintProto::kTable:
      return PresolveTable(ct);
-    case ConstraintProto::ConstraintCase::kAllDiff:
+    case ConstraintProto::kAllDiff:
      return PresolveAllDiff(ct);
-    case ConstraintProto::ConstraintCase::kNoOverlap:
+    case ConstraintProto::kNoOverlap:
      return PresolveNoOverlap(ct);
-    case ConstraintProto::ConstraintCase::kNoOverlap2D:
+    case ConstraintProto::kNoOverlap2D:
      return PresolveNoOverlap2D(c, ct);
-    case ConstraintProto::ConstraintCase::kCumulative:
+    case ConstraintProto::kCumulative:
      return PresolveCumulative(ct);
-    case ConstraintProto::ConstraintCase::kCircuit:
+    case ConstraintProto::kCircuit:
      return PresolveCircuit(ct);
-    case ConstraintProto::ConstraintCase::kRoutes:
+    case ConstraintProto::kRoutes:
      return PresolveRoutes(ct);
-    case ConstraintProto::ConstraintCase::kAutomaton:
+    case ConstraintProto::kAutomaton:
      return PresolveAutomaton(ct);
-    case ConstraintProto::ConstraintCase::kReservoir:
+    case ConstraintProto::kReservoir:
      return PresolveReservoir(ct);
    default:
      return false;
@@ -7059,7 +7037,7 @@ void CpModelPresolver::PresolveToFixPoint() {
  std::deque<int> queue;
  for (int c = 0; c < in_queue.size(); ++c) {
    if (context_->working_model->constraints(c).constraint_case() !=
-        ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
+        ConstraintProto::CONSTRAINT_NOT_SET) {
      in_queue[c] = true;
      queue.push_back(c);
    }
@@ -7227,25 +7205,25 @@ void CpModelPresolver::PresolveToFixPoint() {
  for (int c = 0; c < num_constraints; ++c) {
    ConstraintProto* ct = context_->working_model->mutable_constraints(c);
    switch (ct->constraint_case()) {
-      case ConstraintProto::ConstraintCase::kNoOverlap:
+      case ConstraintProto::kNoOverlap:
        // Filter out absent intervals.
        if (PresolveNoOverlap(ct)) {
          context_->UpdateConstraintVariableUsage(c);
        }
        break;
-      case ConstraintProto::ConstraintCase::kNoOverlap2D:
+      case ConstraintProto::kNoOverlap2D:
        // Filter out absent intervals.
        if (PresolveNoOverlap2D(c, ct)) {
          context_->UpdateConstraintVariableUsage(c);
        }
        break;
-      case ConstraintProto::ConstraintCase::kCumulative:
+      case ConstraintProto::kCumulative:
        // Filter out absent intervals.
        if (PresolveCumulative(ct)) {
          context_->UpdateConstraintVariableUsage(c);
        }
        break;
-      case ConstraintProto::ConstraintCase::kBoolOr: {
+      case ConstraintProto::kBoolOr: {
        // Try to infer domain reductions from clauses and the saved "implies in
        // domain" relations.
        for (const auto& pair :
@@ -7750,19 +7728,19 @@ CpSolverStatus CpModelPresolver::Presolve() {
      ConstraintProto* ct = context_->working_model->mutable_constraints(c);
      PresolveEnforcementLiteral(ct);
      switch (ct->constraint_case()) {
-        case ConstraintProto::ConstraintCase::kBoolOr:
+        case ConstraintProto::kBoolOr:
          PresolveBoolOr(ct);
          break;
-        case ConstraintProto::ConstraintCase::kBoolAnd:
+        case ConstraintProto::kBoolAnd:
          PresolveBoolAnd(ct);
          break;
-        case ConstraintProto::ConstraintCase::kAtMostOne:
+        case ConstraintProto::kAtMostOne:
          PresolveAtMostOne(ct);
          break;
-        case ConstraintProto::ConstraintCase::kExactlyOne:
+        case ConstraintProto::kExactlyOne:
          PresolveExactlyOne(ct);
          break;
-        case ConstraintProto::ConstraintCase::kLinear:
+        case ConstraintProto::kLinear:
          CanonicalizeLinear(ct);
          break;
        default:
@@ -7822,7 +7800,7 @@ CpSolverStatus CpModelPresolver::Presolve() {
    for (int c = 0; c < context_->working_model->constraints_size(); ++c) {
      const auto type =
          context_->working_model->constraints(c).constraint_case();
-      if (type == ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) continue;
+      if (type == ConstraintProto::CONSTRAINT_NOT_SET) continue;
      old_num_non_empty_constraints++;
    }

@@ -7868,9 +7846,7 @@ CpSolverStatus CpModelPresolver::Presolve() {
      const int old_size = context_->working_model->constraints_size();
      for (int c = 0; c < old_size; ++c) {
        ConstraintProto* ct = context_->working_model->mutable_constraints(c);
-        if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
-          continue;
-        }
+        if (ct->constraint_case() != ConstraintProto::kLinear) continue;
        ExtractAtMostOneFromLinear(ct);
      }
      context_->UpdateNewConstraintsVariableUsage();
@@ -8239,7 +8215,7 @@ std::vector<std::pair<int, int>> FindDuplicateConstraints(

    // TODO(user): we could delete duplicate identical interval, but we need
    // to make sure reference to them are updated.
-    if (type == ConstraintProto::ConstraintCase::kInterval) continue;
+    if (type == ConstraintProto::kInterval) continue;

    // We ignore names when comparing constraints.
    //
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -1444,25 +1444,23 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, Model* model) {
  const auto& mapping = *model->GetOrCreate<CpModelMapping>();
  SatSolver::Status status;
  const SatParameters& parameters = *model->GetOrCreate<SatParameters>();
+
  if (parameters.use_probing_search()) {
-    std::vector<BooleanVariable> bool_vars;
-    std::vector<IntegerVariable> int_vars;
-    IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
-    absl::flat_hash_set<BooleanVariable> visited;
-    for (int v = 0; v < model_proto.variables_size(); ++v) {
-      if (mapping.IsBoolean(v)) {
-        const BooleanVariable bool_var = mapping.Literal(v).Variable();
-        if (!visited.contains(bool_var)) {
-          visited.insert(bool_var);
-          bool_vars.push_back(bool_var);
-        }
-      } else {
-        IntegerVariable var = mapping.Integer(v);
-        if (integer_trail->IsFixed(var)) continue;
-        int_vars.push_back(var);
+    ContinuousProber prober(model_proto, model);
+    while (true) {
+      status = prober.Probe();
+      if (status == SatSolver::INFEASIBLE) {
+        shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
+            solution_info);
+        break;
+      }
+      if (status == SatSolver::FEASIBLE) {
+        solution_observer();
+      }
+      if (status == SatSolver::LIMIT_REACHED) {
+        break;
      }
    }
-    status = ContinuousProbing(bool_vars, int_vars, solution_observer, model);
  } else if (!model_proto.has_objective()) {
    while (true) {
      status = ResetAndSolveIntegerProblem(
--- a/ortools/sat/integer_search.cc
+++ b/ortools/sat/integer_search.cc
@@ -16,6 +16,7 @@
 #include <cmath>
 #include <cstdint>
 #include <functional>
+#include <limits>
 #include <vector>

 #include "absl/container/flat_hash_set.h"
@@ -1080,130 +1081,227 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model) {
  return ResetAndSolveIntegerProblem(/*assumptions=*/{}, model);
 }

-SatSolver::Status ContinuousProbing(
-    const std::vector<BooleanVariable>& bool_vars,
-    const std::vector<IntegerVariable>& int_vars,
-    const std::function<void()>& feasible_solution_observer, Model* model) {
-  VLOG(2) << "Start continuous probing with " << bool_vars.size()
-          << " Boolean variables, and " << int_vars.size()
-          << " integer variables";
-
-  SatSolver* solver = model->GetOrCreate<SatSolver>();
-  TimeLimit* time_limit = model->GetOrCreate<TimeLimit>();
-  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
-  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
-  const SatParameters& sat_parameters = *(model->GetOrCreate<SatParameters>());
-  auto* level_zero_callbacks = model->GetOrCreate<LevelZeroCallbackHelper>();
-  Prober* prober = model->GetOrCreate<Prober>();
-  auto* shared_response_manager = model->Mutable<SharedResponseManager>();
-  auto* shared_bounds_manager = model->Mutable<SharedBoundsManager>();
-
-  std::vector<BooleanVariable> active_vars;
-  std::vector<BooleanVariable> integer_bounds;
-  absl::flat_hash_set<BooleanVariable> integer_bounds_set;
-
-  int iteration = 1;
-  absl::Time last_check = absl::Now();
-
-  while (!time_limit->LimitReached()) {
-    if (shared_response_manager != nullptr &&
-        shared_bounds_manager != nullptr &&
-        absl::Now() - last_check >= absl::Seconds(10)) {
-      shared_response_manager->LogMessage(
-          "Probe",
-          absl::StrCat("#iterations:", iteration,
-                       " #literals_fixed:", prober->num_new_literals_fixed(),
-                       " #new_integer_bounds:",
-                       shared_bounds_manager->NumBoundsExported("probing")));
-      last_check = absl::Now();
-    }
-    iteration++;
-
-    // Sync the bounds first.
-    auto SyncBounds = [solver, &level_zero_callbacks]() {
-      if (!solver->ResetToLevelZero()) return false;
-      for (const auto& cb : level_zero_callbacks->callbacks) {
-        if (!cb()) {
-          solver->NotifyThatModelIsUnsat();
-          return false;
-        }
+ContinuousProber::ContinuousProber(const CpModelProto& model_proto,
+                                   Model* model)
+    : model_(model),
+      sat_solver_(model->GetOrCreate<SatSolver>()),
+      time_limit_(model->GetOrCreate<TimeLimit>()),
+      trail_(model->GetOrCreate<Trail>()),
+      integer_trail_(model->GetOrCreate<IntegerTrail>()),
+      encoder_(model->GetOrCreate<IntegerEncoder>()),
+      sat_parameters_(*(model->GetOrCreate<SatParameters>())),
+      deterministic_time_(sat_parameters_.shaving_search_deterministic_time()),
+      use_shaving_(sat_parameters_.use_shaving_in_probing_search()),
+      level_zero_callbacks_(model->GetOrCreate<LevelZeroCallbackHelper>()),
+      prober_(model->GetOrCreate<Prober>()),
+      shared_response_manager_(model->Mutable<SharedResponseManager>()),
+      shared_bounds_manager_(model->Mutable<SharedBoundsManager>()),
+      active_limit_(deterministic_time_) {
+  auto* mapping = model_->GetOrCreate<CpModelMapping>();
+  absl::flat_hash_set<BooleanVariable> visited;
+  for (int v = 0; v < model_proto.variables_size(); ++v) {
+    if (mapping->IsBoolean(v)) {
+      const BooleanVariable bool_var = mapping->Literal(v).Variable();
+      const auto [_, inserted] = visited.insert(bool_var);
+      if (inserted) {
+        bool_vars_.push_back(bool_var);
      }
-      return true;
-    };
-    if (!SyncBounds()) {
-      return SatSolver::INFEASIBLE;
+    } else {
+      IntegerVariable var = mapping->Integer(v);
+      if (integer_trail_->IsFixed(var)) continue;
+      int_vars_.push_back(var);
    }
+  }
+  VLOG(2) << "Start continuous probing with " << bool_vars_.size()
+          << " Boolean variables, and " << int_vars_.size()
+          << " integer variables"
+          << ", deterministic time limit = "
+          << time_limit_->GetDeterministicLimit() << " on " << model_->Name();
+  last_check_ = absl::Now();
+}

+// Continuous probing procedure.
+// TODO(user):
+//   - sort variables before the iteration (statically or dynamically)
+//   - compress clause databases regularly (especially the implication graph)
+//   - better interleaving of the probing and shaving phases
+//   - move the shaving code directly in the probing class
+SatSolver::Status ContinuousProber::Probe() {
+  while (!time_limit_->LimitReached()) {
    // Run sat in-processing to reduce the size of the clause database.
-    if (sat_parameters.use_sat_inprocessing() &&
-        !model->GetOrCreate<Inprocessing>()->InprocessingRound()) {
+    if (sat_parameters_.use_sat_inprocessing() &&
+        !model_->GetOrCreate<Inprocessing>()->InprocessingRound()) {
      return SatSolver::INFEASIBLE;
    }

-    // TODO(user): Explore fast probing methods.
-
    // Probe each Boolean variable at most once per loop.
-    absl::flat_hash_set<BooleanVariable> probed;
+    probed_bool_vars_.clear();
+    probed_literals_.clear();
+
+    // Store current statistics to detect an iteration without any improvement.
+    const int64_t initial_num_literals_fixed =
+        prober_->num_new_literals_fixed();
+    const int64_t initial_num_bounds_shaved = num_bounds_shaved_;

    // Probe variable bounds.
    // TODO(user): Probe optional variables.
-    for (const IntegerVariable int_var : int_vars) {
-      if (integer_trail->IsFixed(int_var) ||
-          integer_trail->IsOptional(int_var)) {
+    for (const IntegerVariable int_var : int_vars_) {
+      if (integer_trail_->IsFixed(int_var) ||
+          integer_trail_->IsOptional(int_var)) {
        continue;
      }

+      if (!ImportFromSharedClasses()) {
+        return SatSolver::INFEASIBLE;
+      }
+
+      if (time_limit_->LimitReached()) {
+        return SatSolver::LIMIT_REACHED;
+      }
+
      const BooleanVariable shave_lb =
-          encoder
+          encoder_
              ->GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual(
-                  int_var, integer_trail->LowerBound(int_var)))
+                  int_var, integer_trail_->LowerBound(int_var)))
              .Variable();
-      if (!probed.contains(shave_lb)) {
-        probed.insert(shave_lb);
-        if (!prober->ProbeOneVariable(shave_lb)) {
+      const auto [_lb, lb_inserted] = probed_bool_vars_.insert(shave_lb);
+      if (lb_inserted) {
+        if (!prober_->ProbeOneVariable(shave_lb)) {
          return SatSolver::INFEASIBLE;
        }
+        num_literals_probed_++;
      }

      const BooleanVariable shave_ub =
-          encoder
+          encoder_
              ->GetOrCreateAssociatedLiteral(IntegerLiteral::GreaterOrEqual(
-                  int_var, integer_trail->UpperBound(int_var)))
+                  int_var, integer_trail_->UpperBound(int_var)))
              .Variable();
-      if (!probed.contains(shave_ub)) {
-        probed.insert(shave_ub);
-        if (!prober->ProbeOneVariable(shave_ub)) {
+      const auto [_ub, ub_inserted] = probed_bool_vars_.insert(shave_ub);
+      if (ub_inserted) {
+        if (!prober_->ProbeOneVariable(shave_ub)) {
          return SatSolver::INFEASIBLE;
        }
+        num_literals_probed_++;
      }

-      if (!SyncBounds()) {
-        return SatSolver::INFEASIBLE;
-      }
-      if (time_limit->LimitReached()) {
-        return SatSolver::LIMIT_REACHED;
+      if (use_shaving_) {
+        const SatSolver::Status lb_status =
+            ShaveLiteral(Literal(shave_lb, true));
+        if (ReportStatus(lb_status)) return lb_status;
+
+        const SatSolver::Status ub_status =
+            ShaveLiteral(Literal(shave_ub, true));
+        if (ReportStatus(ub_status)) return ub_status;
      }
+
+      LogStatistics();
    }

    // Probe Boolean variables from the model.
-    for (const BooleanVariable& bool_var : bool_vars) {
-      if (solver->Assignment().VariableIsAssigned(bool_var)) continue;
-      if (time_limit->LimitReached()) {
-        return SatSolver::LIMIT_REACHED;
-      }
-      if (!SyncBounds()) {
+    for (const BooleanVariable& bool_var : bool_vars_) {
+      if (sat_solver_->Assignment().VariableIsAssigned(bool_var)) continue;
+
+      if (!ImportFromSharedClasses()) {
        return SatSolver::INFEASIBLE;
      }
-      if (!probed.contains(bool_var)) {
-        probed.insert(bool_var);
-        if (!prober->ProbeOneVariable(bool_var)) {
+
+      if (time_limit_->LimitReached()) {
+        return SatSolver::LIMIT_REACHED;
+      }
+
+      const auto [_, inserted] = probed_bool_vars_.insert(bool_var);
+      if (inserted) {
+        if (!prober_->ProbeOneVariable(bool_var)) {
          return SatSolver::INFEASIBLE;
        }
+        num_literals_probed_++;
      }
+
+      const Literal literal(bool_var, true);
+      if (use_shaving_ &&
+          !sat_solver_->Assignment().LiteralIsAssigned(literal)) {
+        const SatSolver::Status true_status = ShaveLiteral(literal);
+        if (ReportStatus(true_status)) return true_status;
+        if (true_status == SatSolver::ASSUMPTIONS_UNSAT) continue;
+
+        const SatSolver::Status false_status = ShaveLiteral(literal.Negated());
+        if (ReportStatus(false_status)) return false_status;
+      }
+
+      LogStatistics();
    }
+
+    // Adjust the active_limit.
+    const bool something_has_been_detected =
+        num_bounds_shaved_ != initial_num_bounds_shaved ||
+        prober_->num_new_literals_fixed() != initial_num_literals_fixed;
+    if (something_has_been_detected) {  // Reset the limit.
+      active_limit_ = deterministic_time_;
+    } else if (active_limit_ < 10 * deterministic_time_) {  // Bump the limit.
+      active_limit_ += deterministic_time_;
+    }
+
+    ++iteration_;
  }
  return SatSolver::LIMIT_REACHED;
 }

+bool ContinuousProber::ImportFromSharedClasses() {
+  if (!sat_solver_->ResetToLevelZero()) return false;
+  for (const auto& cb : level_zero_callbacks_->callbacks) {
+    if (!cb()) {
+      sat_solver_->NotifyThatModelIsUnsat();
+      return false;
+    }
+  }
+  return true;
+}
+
+SatSolver::Status ContinuousProber::ShaveLiteral(Literal literal) {
+  const auto [_, inserted] = probed_literals_.insert(literal.Index());
+  if (trail_->Assignment().LiteralIsAssigned(literal) || !inserted) {
+    return SatSolver::LIMIT_REACHED;
+  }
+  num_bounds_tried_++;
+
+  const double original_dtime_limit = time_limit_->GetDeterministicLimit();
+  time_limit_->ChangeDeterministicLimit(
+      std::min(original_dtime_limit,
+               time_limit_->GetElapsedDeterministicTime() + active_limit_));
+  const SatSolver::Status status =
+      ResetAndSolveIntegerProblem({literal}, model_);
+  time_limit_->ChangeDeterministicLimit(original_dtime_limit);
+
+  if (status == SatSolver::ASSUMPTIONS_UNSAT) {
+    num_bounds_shaved_++;
+  }
+
+  return status;
+}
+
+bool ContinuousProber::ReportStatus(const SatSolver::Status status) {
+  return status == SatSolver::INFEASIBLE || status == SatSolver::FEASIBLE;
+}
+
+void ContinuousProber::LogStatistics() {
+  if (shared_response_manager_ == nullptr ||
+      shared_bounds_manager_ == nullptr) {
+    return;
+  }
+  const absl::Time now = absl::Now();
+  if (now <= last_check_ + absl::Seconds(10)) return;
+  shared_response_manager_->LogMessage(
+      "Probe",
+      absl::StrCat(
+          "#iterations:", iteration_,
+          " #literals fixed/probed:", prober_->num_new_literals_fixed(), "/",
+          num_literals_probed_, " #bounds shaved/tried:", num_bounds_shaved_,
+          "/", num_bounds_tried_, " #new_integer_bounds:",
+          shared_bounds_manager_->NumBoundsExported("probing"),
+          ", #new_binary_clauses:", prober_->num_new_binary_clauses()));
+  last_check_ = now;
+}
+
 }  // namespace sat
 }  // namespace operations_research
--- a/ortools/sat/integer_search.h
+++ b/ortools/sat/integer_search.h
@@ -25,8 +25,10 @@

 #include <vector>

+#include "ortools/sat/cp_model_mapping.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/linear_programming_constraint.h"
+#include "ortools/sat/probing.h"
 #include "ortools/sat/pseudo_costs.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_solver.h"
@@ -231,8 +233,7 @@ std::vector<std::function<BooleanOrIntegerLiteral()>> CompleteHeuristics(
 // of integer variables.
 SatSolver::Status ContinuousProbing(
    const std::vector<BooleanVariable>& bool_vars,
-    const std::vector<IntegerVariable>& int_vars,
-    const std::function<void()>& feasible_solution_observer, Model* model);
+    const std::vector<IntegerVariable>& int_vars, Model* model);

 // An helper class to share the code used by the different kind of search.
 class IntegerSearchHelper {
@@ -262,6 +263,46 @@ class IntegerSearchHelper {
  IntegerVariable objective_var_ = kNoIntegerVariable;
 };

+// This class will loop continuously on model variables and try to probe/shave
+// its bounds.
+class ContinuousProber {
+ public:
+  ContinuousProber(const CpModelProto& model_proto, Model* model);
+  SatSolver::Status Probe();
+
+ private:
+  bool ImportFromSharedClasses();
+  SatSolver::Status ShaveLiteral(Literal literal);
+  bool ReportStatus(const SatSolver::Status status);
+  void LogStatistics();
+
+  std::vector<BooleanVariable> bool_vars_;
+  std::vector<IntegerVariable> int_vars_;
+  Model* model_;
+  SatSolver* sat_solver_;
+  TimeLimit* time_limit_;
+  Trail* trail_;
+  IntegerTrail* integer_trail_;
+  IntegerEncoder* encoder_;
+  const SatParameters sat_parameters_;
+  const double deterministic_time_;
+  const bool use_shaving_;
+  LevelZeroCallbackHelper* level_zero_callbacks_;
+  Prober* prober_;
+  SharedResponseManager* shared_response_manager_;
+  SharedBoundsManager* shared_bounds_manager_;
+  double active_limit_;
+  int64_t num_bounds_shaved_ = 0;
+  int64_t num_bounds_tried_ = 0;
+  // Probe each Boolean variable or literal at most once per loop.
+  // TODO(user): use 2 vector<bool>.
+  absl::flat_hash_set<BooleanVariable> probed_bool_vars_;
+  absl::flat_hash_set<LiteralIndex> probed_literals_;
+  int iteration_ = 1;
+  int64_t num_literals_probed_ = 0;
+  absl::Time last_check_;
+};
+
 }  // namespace sat
 }  // namespace operations_research

--- a/ortools/sat/pb_constraint.h
+++ b/ortools/sat/pb_constraint.h
@@ -571,6 +571,7 @@ class PbConstraints : public SatPropagator {

  // Returns the number of constraints managed by this class.
  int NumberOfConstraints() const { return constraints_.size(); }
+  bool IsEmpty() const final { return constraints_.empty(); }

  // ConflictingConstraint() returns the last PB constraint that caused a
  // conflict. Calling ClearConflictingConstraint() reset this to nullptr.
--- a/ortools/sat/probing.h
+++ b/ortools/sat/probing.h
@@ -76,6 +76,7 @@ class Prober {
  // They are reset each time ProbleBooleanVariables() is called.
  // Note however that we do not reset them on a call to ProbeOneVariable().
  int num_new_literals_fixed() const { return num_new_literals_fixed_; }
+  int num_new_binary_clauses() const { return num_new_binary_; }

 private:
  bool ProbeOneVariableInternal(BooleanVariable b);
--- a/ortools/sat/sat_base.h
+++ b/ortools/sat/sat_base.h
@@ -503,6 +503,12 @@ class SatPropagator {
    return propagation_trail_index_ == trail.Index();
  }

+  // Small optimization: If a propagator does not contain any "constraints"
+  // there is no point calling propagate on it. Before each propagation, the
+  // solver will checks for emptiness, and construct an optimized list of
+  // propagator before looping many time over the list.
+  virtual bool IsEmpty() const { return false; }
+
 protected:
  const std::string name_;
  int propagator_id_;
--- a/ortools/sat/sat_parameters.proto
+++ b/ortools/sat/sat_parameters.proto
@@ -24,7 +24,7 @@ option csharp_namespace = "Google.OrTools.Sat";
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //
-// NEXT TAG: 204
+// NEXT TAG: 206
 message SatParameters {
  // In some context, like in a portfolio of search, it makes sense to name a
  // given parameters set for logging purpose.
@@ -826,9 +826,18 @@ message SatParameters {
  optional int64 probing_period_at_root = 142 [default = 0];

  // If true, search will continuously probe Boolean variables, and integer
-  // variable bounds.
+  // variable bounds. This parameter is set to true in parallel on the probing
+  // worker.
  optional bool use_probing_search = 176 [default = false];

+  // Add a shaving phase (where the solver tries to prove that the lower or
+  // upper bound of a variable are infeasible) to the probing search.
+  optional bool use_shaving_in_probing_search = 204 [default = true];
+
+  // Specifies the amount of deterministic time spent of each try at shaving a
+  // bound in the shaving search.
+  optional double shaving_search_deterministic_time = 205 [default = 0.001];
+
  // The solver ignores the pseudo costs of variables with number of recordings
  // less than this threshold.
  optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -1617,17 +1617,29 @@ void SatSolver::ProcessNewlyFixedVariables() {
  deterministic_time_of_last_fixed_variables_cleanup_ = deterministic_time();
 }

+bool SatSolver::PropagationIsDone() const {
+  for (SatPropagator* propagator : propagators_) {
+    if (propagator->IsEmpty()) continue;
+    if (!propagator->PropagationIsDone(*trail_)) return false;
+  }
+  return true;
+}
+
 // TODO(user): Support propagating only the "first" propagators. That can
 // be useful for probing/in-processing, so we can control if we do only the SAT
 // part or the full integer part...
 bool SatSolver::Propagate() {
  SCOPED_TIME_STAT(&stats_);

-  // If new binary or pb constraint were added for the first time, we need
-  // to "re-initialize" the list of propagators.
-  if ((!propagate_binary_ && !binary_implication_graph_->IsEmpty()) ||
-      (!propagate_pb_ && pb_constraints_->NumberOfConstraints() > 0)) {
-    InitializePropagators();
+  // Because we might potentially iterate often on this list below, we remove
+  // empty propagators.
+  //
+  // TODO(user): This might not really be needed.
+  non_empty_propagators_.clear();
+  for (SatPropagator* propagator : propagators_) {
+    if (!propagator->IsEmpty()) {
+      non_empty_propagators_.push_back(propagator);
+    }
  }

  while (true) {
@@ -1639,7 +1651,7 @@ bool SatSolver::Propagate() {
    // and that its Propagate() functions will not abort on the first
    // propagation to be slightly more efficient.
    const int old_index = trail_->Index();
-    for (SatPropagator* propagator : propagators_) {
+    for (SatPropagator* propagator : non_empty_propagators_) {
      DCHECK(propagator->PropagatePreconditionsAreSatisfied(*trail_));
      if (!propagator->Propagate(trail_)) return false;
      if (trail_->Index() > old_index) break;
@@ -1651,24 +1663,9 @@ bool SatSolver::Propagate() {

 void SatSolver::InitializePropagators() {
  propagators_.clear();
-
-  // To make Propagate() as fast as possible, we only add the
-  // binary_implication_graph_/pb_constraints_ propagators if there is anything
-  // to propagate.
-  //
-  // TODO(user): uses the Model classes here to only call
-  // model.GetOrCreate<BinaryImplicationGraph>() when the first binary
-  // constraint is needed, and have a mecanism to always make this propagator
-  // first. Same for the linear constraints.
-  if (!binary_implication_graph_->IsEmpty()) {
-    propagate_binary_ = true;
-    propagators_.push_back(binary_implication_graph_);
-  }
+  propagators_.push_back(binary_implication_graph_);
  propagators_.push_back(clauses_propagator_);
-  if (pb_constraints_->NumberOfConstraints() > 0) {
-    propagate_pb_ = true;
-    propagators_.push_back(pb_constraints_);
-  }
+  propagators_.push_back(pb_constraints_);
  for (int i = 0; i < external_propagators_.size(); ++i) {
    propagators_.push_back(external_propagators_[i]);
  }
@@ -1677,13 +1674,6 @@ void SatSolver::InitializePropagators() {
  }
 }

-bool SatSolver::PropagationIsDone() const {
-  for (SatPropagator* propagator : propagators_) {
-    if (!propagator->PropagationIsDone(*trail_)) return false;
-  }
-  return true;
-}
-
 bool SatSolver::ResolvePBConflict(BooleanVariable var,
                                  MutableUpperBoundedLinearConstraint* conflict,
                                  Coefficient* slack) {
@@ -1768,13 +1758,8 @@ void SatSolver::EnqueueNewDecision(Literal literal) {
 void SatSolver::Untrail(int target_trail_index) {
  SCOPED_TIME_STAT(&stats_);
  DCHECK_LT(target_trail_index, trail_->Index());
-
-  if ((!propagate_binary_ && !binary_implication_graph_->IsEmpty()) ||
-      (!propagate_pb_ && pb_constraints_->NumberOfConstraints() > 0)) {
-    InitializePropagators();
-  }
-
  for (SatPropagator* propagator : propagators_) {
+    if (propagator->IsEmpty()) continue;
    propagator->Untrail(*trail_, target_trail_index);
  }
  decision_policy_->Untrail(target_trail_index);
--- a/ortools/sat/sat_solver.h
+++ b/ortools/sat/sat_solver.h
@@ -699,14 +699,13 @@ class SatSolver {

  // Internal propagators. We keep them here because we need more than the
  // SatPropagator interface for them.
-  bool propagate_binary_ = false;
-  bool propagate_pb_ = false;
  BinaryImplicationGraph* binary_implication_graph_;
  LiteralWatchers* clauses_propagator_;
  PbConstraints* pb_constraints_;

  // Ordered list of propagators used by Propagate()/Untrail().
  std::vector<SatPropagator*> propagators_;
+  std::vector<SatPropagator*> non_empty_propagators_;

  // Ordered list of propagators added with AddPropagator().
  std::vector<SatPropagator*> external_propagators_;