[CP-SAT] fix bug with reservoir expansion; improve hint processing; improve work sharing

Author: lperron

ortools/sat/cp_model_checker.cc

@@ -1720,7 +1720,7 @@ class ConstraintChecker {
       current_level += delta.second;
       if (current_level < min_level || current_level > max_level) {
         VLOG(1) << "Reservoir level " << current_level
-                << " is out of bounds at time" << delta.first;
+                << " is out of bounds at time: " << delta.first;
         return false;
       }
     }

ortools/sat/cp_model_expand.cc

@@ -169,8 +169,8 @@ void ExpandReservoirUsingCircuit(int64_t sum_of_positive_demand,
   context->UpdateRuleStats("reservoir: expanded using circuit.");
 }
 
-void ExpandReservoirUsingPrecedences(int64_t sum_of_positive_demand,
-                                     int64_t sum_of_negative_demand,
+void ExpandReservoirUsingPrecedences(bool max_level_is_constraining,
+                                     bool min_level_is_constraining,
                                      ConstraintProto* reservoir_ct,
                                      PresolveContext* context) {
   const ReservoirConstraintProto& reservoir = reservoir_ct->reservoir();
@@ -192,23 +192,21 @@ void ExpandReservoirUsingPrecedences(int64_t sum_of_positive_demand,
 
     // No need for some constraints if the reservoir is just constrained in
     // one direction.
-    if (demand_i > 0 && sum_of_positive_demand <= reservoir.max_level()) {
-      continue;
-    }
-    if (demand_i < 0 && sum_of_negative_demand >= reservoir.min_level()) {
-      continue;
-    }
+    if (demand_i > 0 && !max_level_is_constraining) continue;
+    if (demand_i < 0 && !min_level_is_constraining) continue;
 
-    ConstraintProto* new_ct = context->working_model->add_constraints();
-    LinearConstraintProto* new_linear = new_ct->mutable_linear();
-
-    // Add contributions from previous events.
+    ConstraintProto* new_cumul = context->working_model->add_constraints();
+    LinearConstraintProto* new_linear = new_cumul->mutable_linear();
     int64_t offset = 0;
+
+    // Add contributions from events that happened at time_j <= time_i.
     const LinearExpressionProto& time_i = reservoir.time_exprs(i);
     for (int j = 0; j < num_events; ++j) {
       if (i == j) continue;
       const int active_j = is_active_literal(j);
       if (context->LiteralIsFalse(active_j)) continue;
+      const int64_t demand_j = context->FixedValue(reservoir.level_changes(j));
+      if (demand_j == 0) continue;
 
       // Get or create the literal equivalent to
       // active_i && active_j && time[j] <= time[i].
@@ -218,44 +216,30 @@ void ExpandReservoirUsingPrecedences(int64_t sum_of_positive_demand,
       const LinearExpressionProto& time_j = reservoir.time_exprs(j);
       const int j_lesseq_i = context->GetOrCreateReifiedPrecedenceLiteral(
           time_j, time_i, active_j, active_i);
-      context->working_model->mutable_variables(j_lesseq_i)
-          ->set_name(absl::StrCat(j, " before ", i));
-
-      const int64_t demand = context->FixedValue(reservoir.level_changes(j));
-      if (RefIsPositive(j_lesseq_i)) {
-        new_linear->add_vars(j_lesseq_i);
-        new_linear->add_coeffs(demand);
-      } else {
-        new_linear->add_vars(NegatedRef(j_lesseq_i));
-        new_linear->add_coeffs(-demand);
-        offset -= demand;
-      }
+      AddWeightedLiteralToLinearConstraint(j_lesseq_i, demand_j, new_linear,
+                                           &offset);
     }
 
     // Add contribution from event i.
     //
     // TODO(user): Alternatively we can mark the whole constraint as enforced
     // only if active_i is true. Experiments with both version, right now we
     // miss enough benchmarks to conclude.
-    if (RefIsPositive(active_i)) {
-      new_linear->add_vars(active_i);
-      new_linear->add_coeffs(demand_i);
-    } else {
-      new_linear->add_vars(NegatedRef(active_i));
-      new_linear->add_coeffs(-demand_i);
-      offset -= demand_i;
-    }
+    AddWeightedLiteralToLinearConstraint(active_i, demand_i, new_linear,
+                                         &offset);
 
     // Note that according to the sign of demand_i, we only need one side.
+    // We apply the offset here to make sure we use int64_t min and max.
     if (demand_i > 0) {
       new_linear->add_domain(std::numeric_limits<int64_t>::min());
-      new_linear->add_domain(reservoir.max_level());
+      new_linear->add_domain(reservoir.max_level() - offset);
     } else {
-      new_linear->add_domain(reservoir.min_level());
+      new_linear->add_domain(reservoir.min_level() - offset);
       new_linear->add_domain(std::numeric_limits<int64_t>::max());
     }
 
-    context->CanonicalizeLinearConstraint(new_ct);
+    // Canonicalize the newly created constraint.
+    context->CanonicalizeLinearConstraint(new_cumul);
   }
 
   reservoir_ct->Clear();
@@ -367,9 +351,10 @@ void ExpandReservoir(ConstraintProto* reservoir_ct, PresolveContext* context) {
   } else {
     // This one is the faster option usually.
     if (all_demands_are_fixed) {
-      ExpandReservoirUsingPrecedences(sum_of_positive_demand,
-                                      sum_of_negative_demand, reservoir_ct,
-                                      context);
+      ExpandReservoirUsingPrecedences(
+          sum_of_positive_demand > reservoir_ct->reservoir().max_level(),
+          sum_of_negative_demand < reservoir_ct->reservoir().min_level(),
+          reservoir_ct, context);
     } else {
       context->UpdateRuleStats(
           "reservoir: skipped expansion due to variable demands");

ortools/sat/cp_model_expand_test.cc

@@ -92,6 +92,29 @@ TEST(ReservoirExpandTest, NoOptionalAndInitiallyFeasible) {
   EXPECT_EQ(27, solutions.size());
 }
 
+TEST(ReservoirExpandTest, SimpleSemaphore) {
+  const CpModelProto initial_model = ParseTestProto(R"pb(
+    variables { domain: 0 domain: 10 }
+    variables { domain: 0 domain: 10 }
+    variables { domain: 0 domain: 1 }
+    constraints {
+      reservoir {
+        max_level: 2
+        time_exprs { vars: 0 coeffs: 1 }
+        time_exprs { vars: 1 coeffs: 1 }
+        active_literals: [ 2, 2 ]
+        level_changes { offset: -1 }
+        level_changes { offset: 1 }
+      }
+    }
+  )pb");
+  absl::btree_set<std::vector<int>> solutions;
+  const CpSolverResponse response =
+      SolveAndCheck(initial_model, "", &solutions);
+  EXPECT_EQ(OPTIMAL, response.status());
+  EXPECT_EQ(187, solutions.size());
+}
+
 TEST(ReservoirExpandTest, GizaReport) {
   const CpModelProto initial_model = ParseTestProto(R"pb(
     variables { domain: 0 domain: 10 }

ortools/sat/cp_model_presolve.cc

@@ -444,7 +444,11 @@ bool CpModelPresolver::PresolveBoolAnd(ConstraintProto* ct) {
       return MarkConstraintAsFalse(ct);
     }
     if (context_->VariableIsUniqueAndRemovable(literal)) {
+      // This is a "dual" reduction.
       changed = true;
+      context_->UpdateRuleStats(
+          "bool_and: setting unused literal in rhs to true");
+      context_->UpdateLiteralSolutionHint(literal, true);
       if (!context_->SetLiteralToTrue(literal)) return true;
       continue;
     }
@@ -6879,8 +6883,8 @@ bool CpModelPresolver::PresolveReservoir(ConstraintProto* ct) {
       (num_positives == 0 || num_negatives == 0)) {
     // If all level_changes have the same sign, and if the initial state is
     // always feasible, we do not care about the order, just the sum.
-    auto* const sum =
-        context_->working_model->add_constraints()->mutable_linear();
+    auto* const sum_ct = context_->working_model->add_constraints();
+    auto* const sum = sum_ct->mutable_linear();
     int64_t fixed_contrib = 0;
     for (int i = 0; i < proto.level_changes_size(); ++i) {
       const int64_t demand = context_->FixedValue(proto.level_changes(i));
@@ -6898,6 +6902,7 @@ bool CpModelPresolver::PresolveReservoir(ConstraintProto* ct) {
     }
     sum->add_domain(proto.min_level() - fixed_contrib);
     sum->add_domain(proto.max_level() - fixed_contrib);
+    CanonicalizeLinear(sum_ct);
     context_->UpdateRuleStats("reservoir: converted to linear");
     return RemoveConstraint(ct);
   }

ortools/sat/cp_model_utils.cc

@@ -643,6 +643,20 @@ void AddLinearExpressionToLinearConstraint(const LinearExpressionProto& expr,
   }
 }
 
+void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff,
+                                          LinearConstraintProto* linear,
+                                          int64_t* offset) {
+  if (coeff == 0) return;
+  if (RefIsPositive(lit)) {
+    linear->add_vars(lit);
+    linear->add_coeffs(coeff);
+  } else {
+    linear->add_vars(NegatedRef(lit));
+    linear->add_coeffs(-coeff);
+    *offset += coeff;
+  }
+}
+
 bool SafeAddLinearExpressionToLinearConstraint(
     const LinearExpressionProto& expr, int64_t coefficient,
     LinearConstraintProto* linear) {

ortools/sat/cp_model_utils.h

@@ -237,6 +237,13 @@ void AddLinearExpressionToLinearConstraint(const LinearExpressionProto& expr,
                                            int64_t coefficient,
                                            LinearConstraintProto* linear);
 
+// Same as above, but with a single term (lit, coeff). Note that lit can be
+// negative. The offset is relative to the linear expression (and should be
+// negated when added to the rhs of the linear constraint proto).
+void AddWeightedLiteralToLinearConstraint(int lit, int64_t coeff,
+                                          LinearConstraintProto* linear,
+                                          int64_t* offset);
+
 // Same method, but returns if the addition was possible without overflowing.
 bool SafeAddLinearExpressionToLinearConstraint(
     const LinearExpressionProto& expr, int64_t coefficient,

ortools/sat/parameters_validation.cc

@@ -106,6 +106,8 @@ std::string ValidateParameters(const SatParameters& params) {
   TEST_IN_RANGE(interleave_batch_size, 0, kMaxReasonableParallelism);
   TEST_IN_RANGE(shared_tree_open_leaves_per_worker, 1,
                 kMaxReasonableParallelism);
+  TEST_IN_RANGE(shared_tree_balance_tolerance, 0,
+                log2(kMaxReasonableParallelism));
 
   // TODO(user): Consider using annotations directly in the proto for these
   // validation. It is however not open sourced.

ortools/sat/presolve_context.cc

@@ -2319,7 +2319,7 @@ int PresolveContext::GetOrCreateReifiedPrecedenceLiteral(
   if (!LiteralIsTrue(active_i)) {
     AddImplication(result, active_i);
   }
-  if (!LiteralIsTrue(active_j)) {
+  if (!LiteralIsTrue(active_j) && active_i != active_j) {
     AddImplication(result, active_j);
   }
 
@@ -2341,7 +2341,7 @@ int PresolveContext::GetOrCreateReifiedPrecedenceLiteral(
     if (!LiteralIsTrue(active_i)) {
       greater->add_enforcement_literal(active_i);
     }
-    if (!LiteralIsTrue(active_j)) {
+    if (!LiteralIsTrue(active_j) && active_i != active_j) {
       greater->add_enforcement_literal(active_j);
     }
     CanonicalizeLinearConstraint(greater);

ortools/sat/presolve_context.h

@@ -603,14 +603,18 @@ class PresolveContext {
            hint_[var] == (RefIsPositive(lit) ? value : !value);
   }
 
+  // If the given literal is already hinted, updates its hint.
+  // Otherwise do nothing.
   void UpdateLiteralSolutionHint(int lit, bool value) {
-    UpdateSolutionHint(PositiveRef(lit), RefIsPositive(lit) ? value : !value);
+    UpdateSolutionHint(PositiveRef(lit), RefIsPositive(lit) == value ? 1 : 0);
   }
 
-  // Updates the hint of an existing variable with an existing hint.
+  // If the given variable is already hinted, updates its hint value.
+  // Otherwise, do nothing.
   void UpdateSolutionHint(int var, int64_t value) {
-    CHECK(hint_is_loaded_);
-    CHECK(hint_has_value_[var]);
+    DCHECK(RefIsPositive(var));
+    if (!hint_is_loaded_) return;
+    if (!hint_has_value_[var]) return;
     hint_[var] = value;
   }
 

ortools/sat/sat_parameters.proto

@@ -23,7 +23,7 @@ option java_multiple_files = true;
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //
-// NEXT TAG: 305
+// NEXT TAG: 306
 message SatParameters {
   // In some context, like in a portfolio of search, it makes sense to name a
   // given parameters set for logging purpose.
@@ -1141,6 +1141,15 @@ message SatParameters {
   optional SharedTreeSplitStrategy shared_tree_split_strategy = 239
       [default = SPLIT_STRATEGY_AUTO];
 
+  // How much deeper compared to the ideal max depth of the tree is considered
+  // "balanced" enough to still accept a split. Without such a tolerance,
+  // sometimes the tree can only be split by a single worker, and they may not
+  // generate a split for some time. In contrast, with a tolerance of 1, at
+  // least half of all workers should be able to split the tree as soon as a
+  // split becomes required. This only has an effect on
+  // SPLIT_STRATEGY_BALANCED_TREE and SPLIT_STRATEGY_DISCREPANCY.
+  optional int32 shared_tree_balance_tolerance = 305 [default = 1];
+
   // Whether we enumerate all solutions of a problem without objective. Note
   // that setting this to true automatically disable some presolve reduction
   // that can remove feasible solution. That is it has the same effect as