[CP-SAT] use linearized expression in ttef; add probing_max_lp

ortools/sat/BUILD.bazel

@@ -907,6 +907,7 @@ cc_library(
     srcs = ["timetable_edgefinding.cc"],
     hdrs = ["timetable_edgefinding.h"],
     deps = [
+        ":implied_bounds",
         ":integer",
         ":intervals",
         ":sat_base",

ortools/sat/cp_model_lns.cc

@@ -625,7 +625,7 @@ void ProcessDemandListFromCumulativeConstraint(
       unique_starts.push_back(demand.start);
     }
   }
-  CHECK(std::is_sorted(unique_starts.begin(), unique_starts.end()));
+  DCHECK(std::is_sorted(unique_starts.begin(), unique_starts.end()));
   const int num_points = unique_starts.size();
 
   // Split the capacity in 2 and dispatch all demands on the 2 parts.

ortools/sat/cp_model_search.cc

@@ -504,6 +504,9 @@ std::vector<SatParameters> GetDiverseSetOfParameters(
       new_params.set_use_hard_precedences_in_cumulative_constraint(true);
     }
     strategies["probing"] = new_params;
+
+    new_params.set_linearization_level(2);
+    strategies["probing_max_lp"] = new_params;
   }
 
   // Search variation.
@@ -605,6 +608,7 @@ std::vector<SatParameters> GetDiverseSetOfParameters(
       names.push_back("quick_restart_no_lp");
       names.push_back("lb_tree_search");
       names.push_back("probing");
+      if (base_params.num_workers() > 16) names.push_back("probing_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)

ortools/sat/cumulative.cc

@@ -244,8 +244,8 @@ std::function<void(Model*)> Cumulative(
     // rule. It increases the minimum of the start variables and decreases the
     // maximum of the end variables,
     if (parameters.use_timetable_edge_finding_in_cumulative_constraint()) {
-      TimeTableEdgeFinding* time_table_edge_finding =
-          new TimeTableEdgeFinding(demands, capacity, helper, integer_trail);
+      TimeTableEdgeFinding* time_table_edge_finding = new TimeTableEdgeFinding(
+          demands, capacity, helper, integer_trail, model);
       time_table_edge_finding->RegisterWith(watcher);
       model->TakeOwnership(time_table_edge_finding);
     }
@@ -316,8 +316,8 @@ std::function<void(Model*)> CumulativeTimeDecomposition(
 
         model->Add(ReifiedBoolAnd(consume_condition, consume));
 
-        // TODO(user): this is needed because we currently can't create a
-        // boolean variable if the model is unsat.
+        // this is needed because we currently can't create a boolean variable
+        // if the model is unsat.
         if (sat_solver->IsModelUnsat()) return;
 
         literals_with_coeff.push_back(

ortools/sat/timetable_edgefinding.cc

@@ -19,6 +19,7 @@
 
 #include "ortools/base/iterator_adaptors.h"
 #include "ortools/base/logging.h"
+#include "ortools/sat/implied_bounds.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/intervals.h"
 #include "ortools/util/strong_integers.h"
@@ -28,7 +29,8 @@ namespace sat {
 
 TimeTableEdgeFinding::TimeTableEdgeFinding(
     const std::vector<AffineExpression>& demands, AffineExpression capacity,
-    SchedulingConstraintHelper* helper, IntegerTrail* integer_trail)
+    SchedulingConstraintHelper* helper, IntegerTrail* integer_trail,
+    Model* model)
     : num_tasks_(helper->NumTasks()),
       demands_(demands),
       capacity_(capacity),
@@ -41,6 +43,12 @@ TimeTableEdgeFinding::TimeTableEdgeFinding(
   // Energy of free parts.
   size_free_.resize(num_tasks_);
   energy_free_.resize(num_tasks_);
+
+  // Try to linearize the energy.
+  energies_.resize(num_tasks_);
+  for (int t = 0; t < num_tasks_; t++) {
+    energies_[t] = TryToLinearizeProduct(helper->Sizes()[t], demands[t], model);
+  }
 }
 
 void TimeTableEdgeFinding::RegisterWith(GenericLiteralWatcher* watcher) {
@@ -156,12 +164,27 @@ bool TimeTableEdgeFinding::TimeTableEdgeFindingPass() {
     // If the task has no mandatory part, then its free part is the task itself.
     const IntegerValue start_max = helper_->StartMax(t);
     const IntegerValue end_min = helper_->EndMin(t);
+    const IntegerValue demand_min = DemandMin(t);
+    IntegerValue mandatory_energy(0);
+
     if (start_max >= end_min) {
       size_free_[t] = helper_->SizeMin(t);
     } else {
       size_free_[t] = helper_->SizeMin(t) + start_max - end_min;
+      mandatory_energy = (end_min - start_max) * demand_min;
     }
-    energy_free_[t] = size_free_[t] * DemandMin(t);
+    const IntegerValue min_energy_of_product = helper_->SizeMin(t) * demand_min;
+    const IntegerValue min_linear_energy =
+        energies_[t].has_value() ? energies_[t].value().Min(*integer_trail_)
+                                 : IntegerValue(0);
+    CHECK_EQ(size_free_[t] * DemandMin(t) + mandatory_energy,
+             min_energy_of_product);
+    // if (min_linear_energy > min_energy_of_product) {
+    //   LOG(INFO) << "linear: " << min_linear_energy.value()
+    //             << " vs product: " << min_energy_of_product.value();
+    // }
+    energy_free_[t] =
+        std::max(min_linear_energy, min_energy_of_product) - mandatory_energy;
   }
 
   BuildTimeTable();
@@ -294,6 +317,23 @@ bool TimeTableEdgeFinding::TimeTableEdgeFindingPass() {
   return true;
 }
 
+void TimeTableEdgeFinding::AddEnergyReason(int task_index) {
+  if (energies_[task_index].has_value()) {
+    for (const IntegerVariable var : energies_[task_index].value().vars) {
+      helper_->MutableIntegerReason()->push_back(
+          integer_trail_->LowerBoundAsLiteral(var));
+    }
+  } else {
+    // Variables of the task to be pushed. We do not need the end max for this
+    // task and we only need for it to begin in the time window.
+    if (demands_[task_index].var != kNoIntegerVariable) {
+      helper_->MutableIntegerReason()->push_back(
+          integer_trail_->LowerBoundAsLiteral(demands_[task_index].var));
+    }
+    helper_->AddSizeMinReason(task_index);
+  }
+}
+
 bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin,
                                             IntegerValue end, int task_index,
                                             IntegerValue new_start) {
@@ -306,14 +346,8 @@ bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin,
         integer_trail_->UpperBoundAsLiteral(capacity_.var));
   }
 
-  // Variables of the task to be pushed. We do not need the end max for this
-  // task and we only need for it to begin in the time window.
-  if (demands_[task_index].var != kNoIntegerVariable) {
-    mutable_reason->push_back(
-        integer_trail_->LowerBoundAsLiteral(demands_[task_index].var));
-  }
   helper_->AddStartMinReason(task_index, begin);
-  helper_->AddSizeMinReason(task_index);
+  AddEnergyReason(task_index);
 
   // Task contributing to the energy in the interval.
   for (int t = 0; t < num_tasks_; ++t) {
@@ -322,11 +356,6 @@ bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin,
     if (helper_->EndMax(t) <= begin) continue;
     if (helper_->StartMin(t) >= end) continue;
 
-    if (demands_[t].var != kNoIntegerVariable) {
-      mutable_reason->push_back(
-          integer_trail_->LowerBoundAsLiteral(demands_[t].var));
-    }
-
     // We need the reason for the energy contribution of this interval into
     // [begin, end].
     //
@@ -338,8 +367,8 @@ bool TimeTableEdgeFinding::IncreaseStartMin(IntegerValue begin,
     // that just using size min and these bounds. Fix.
     helper_->AddStartMinReason(t, std::min(begin, helper_->StartMin(t)));
     helper_->AddEndMaxReason(t, std::max(end, helper_->EndMax(t)));
-    helper_->AddSizeMinReason(t);
     helper_->AddPresenceReason(t);
+    AddEnergyReason(t);
   }
 
   return helper_->IncreaseStartMin(task_index, new_start);

ortools/sat/timetable_edgefinding.h

@@ -63,7 +63,7 @@ class TimeTableEdgeFinding : public PropagatorInterface {
   TimeTableEdgeFinding(const std::vector<AffineExpression>& demands,
                        AffineExpression capacity,
                        SchedulingConstraintHelper* helper,
-                       IntegerTrail* integer_trail);
+                       IntegerTrail* integer_trail, Model* model);
 
   bool Propagate() final;
 
@@ -87,6 +87,9 @@ class TimeTableEdgeFinding : public PropagatorInterface {
   bool IncreaseStartMin(IntegerValue begin, IntegerValue end, int task_index,
                         IntegerValue new_start);
 
+  // Add the minimum energy reason of a task.
+  void AddEnergyReason(int task_index);
+
   IntegerValue DemandMin(int task_index) const {
     return integer_trail_->LowerBound(demands_[task_index]);
   }
@@ -106,6 +109,8 @@ class TimeTableEdgeFinding : public PropagatorInterface {
   SchedulingConstraintHelper* helper_;
   IntegerTrail* integer_trail_;
 
+  std::vector<std::optional<LinearExpression>> energies_;
+
   // Start (resp. end) of the compulsory parts used to build the profile.
   std::vector<TaskTime> scp_;
   std::vector<TaskTime> ecp_;