[CP-SAT] fix #4458; fix overflow in cumulative propagator

Author: lperron

ortools/sat/cp_model_solver.cc

@@ -2489,11 +2489,17 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
   const CpSolverStatus presolve_status =
       PresolveCpModel(context.get(), &postsolve_mapping);
 
-  // Delete the context as soon a the presolve is done. Note that only
+  // Delete the context as soon as the presolve is done. Note that only
   // postsolve_mapping and mapping_proto are needed for postsolve.
   context.reset(nullptr);
 
   if (presolve_status != CpSolverStatus::UNKNOWN) {
+    if (presolve_status == CpSolverStatus::INFEASIBLE &&
+        hint_feasible_before_presolve &&
+        params.debug_crash_if_presolve_breaks_hint()) {
+      LOG(FATAL) << "Presolve bug: model with feasible hint found UNSAT "
+                    "after presolve.";
+    }
     SOLVER_LOG(logger, "Problem closed by presolve.");
     CpSolverResponse status_response;
     status_response.set_status(presolve_status);

ortools/sat/cumulative_energy.cc

@@ -529,14 +529,15 @@ bool CumulativeDualFeasibleEnergyConstraint::Propagate() {
   if (num_events == 0) return true;
   ++num_calls_;
 
-  const IntegerValue largest_window =
-      helper_->EndMax(helper_->TaskByDecreasingEndMax().front().task_index) -
-      helper_->TaskByIncreasingStartMin().front().time;
-  if (largest_window == 0) return true;
+  const IntegerValue start_end_magnitude =
+      std::max(IntTypeAbs(helper_->EndMax(
+                   helper_->TaskByDecreasingEndMax().front().task_index)),
+               IntTypeAbs(helper_->TaskByIncreasingStartMin().front().time));
+  if (start_end_magnitude == 0) return true;
 
   const IntegerValue max_for_fixpoint_inverse =
       std::numeric_limits<IntegerValue>::max() /
-      (num_events * capacity_max * largest_window);
+      (num_events * capacity_max * start_end_magnitude);
 
   theta_tree_.Reset(num_events);
 

ortools/sat/diffn_util.cc

@@ -2008,7 +2008,7 @@ std::vector<std::pair<int, int>> FindPartialRectangleIntersectionsAlsoEmpty(
   return result;
 }
 
-absl::optional<std::pair<int, int>> FindOneIntersectionIfPresent(
+std::optional<std::pair<int, int>> FindOneIntersectionIfPresent(
     absl::Span<const Rectangle> rectangles) {
   DCHECK(
       absl::c_is_sorted(rectangles, [](const Rectangle& a, const Rectangle& b) {

ortools/sat/diffn_util.h

@@ -713,7 +713,7 @@ std::vector<std::pair<int, int>> FindPartialRectangleIntersectionsAlsoEmpty(
 //
 // If a pair {i, j} is returned, we will have i < j, and no intersection in
 // the subset of rectanges in [0, j).
-absl::optional<std::pair<int, int>> FindOneIntersectionIfPresent(
+std::optional<std::pair<int, int>> FindOneIntersectionIfPresent(
     absl::Span<const Rectangle> rectangles);
 
 }  // namespace sat

ortools/sat/precedences.cc

@@ -216,10 +216,13 @@ void PrecedenceRelations::Build() {
 
   // We will construct a graph with the current relation from all_relations_.
   // And use this to compute the "closure".
-  // Note that the non-determinism of the arcs order shouldn't matter.
   CHECK(arc_offsets_.empty());
   graph_.ReserveArcs(2 * root_relations_.size());
-  for (const auto [var_pair, negated_offset] : root_relations_) {
+  std::vector<
+      std::pair<std::pair<IntegerVariable, IntegerVariable>, IntegerValue>>
+      root_relations_sorted(root_relations_.begin(), root_relations_.end());
+  std::sort(root_relations_sorted.begin(), root_relations_sorted.end());
+  for (const auto [var_pair, negated_offset] : root_relations_sorted) {
     // TODO(user): Support negative offset?
     //
     // Note that if we only have >= 0 ones, if we do have a cycle, we could

ortools/sat/work_assignment.cc

@@ -820,6 +820,8 @@ bool SharedTreeWorker::SyncWithSharedTree() {
                                    time_limit_->GetElapsedDeterministicTime()) {
     earliest_replacement_dtime_ =
         time_limit_->GetElapsedDeterministicTime() + 1;
+    // Treat this as reassigning the same tree.
+    assigned_tree_lbds_.Add(restart_policy_->LbdAverageSinceReset());
   }
   VLOG(2) << "Assigned level: " << assigned_tree_.MaxLevel() << " "
           << parameters_->name();