fix cumulative presolve in CP-SAT

ortools/sat/cp_model_presolve.cc

@@ -1709,8 +1709,8 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) {
     ct->mutable_cumulative()->mutable_demands()->Truncate(new_size);
   }
 
-  if (HasEnforcementLiteral(*ct)) return false;
-  if (!context->IsFixed(proto.capacity())) return false;
+  if (HasEnforcementLiteral(*ct)) return changed;
+  if (!context->IsFixed(proto.capacity())) return changed;
   const int64 capacity = context->MinOf(proto.capacity());
 
   const int size = proto.intervals_size();
@@ -1735,7 +1735,7 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) {
     if (context->MinOf(duration_ref) == 0) {
       // The behavior for zero-duration interval is currently not the same in
       // the no-overlap and the cumulative constraint.
-      return false;
+      return changed;
     }
     const int64 demand_min = context->MinOf(demand_ref);
     const int64 demand_max = context->MaxOf(demand_ref);
@@ -1746,12 +1746,12 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) {
       context->UpdateRuleStats("cumulative: demand_min exceeds capacity");
       if (ct.enforcement_literal().empty()) {
         context->is_unsat = true;
-        return false;
+        return changed;
       } else {
         CHECK_EQ(ct.enforcement_literal().size(), 1);
         context->SetLiteralToFalse(ct.enforcement_literal(0));
       }
-      return false;
+      return changed;
     } else if (demand_max > capacity) {
       if (ct.enforcement_literal().empty()) {
         context->UpdateRuleStats("cumulative: demand_max exceeds capacity.");
@@ -1761,7 +1761,7 @@ bool PresolveCumulative(ConstraintProto* ct, PresolveContext* context) {
         // for instance.
         context->UpdateRuleStats(
             "cumulative: demand_max of optional interval exceeds capacity.");
-        return false;
+        return changed;
       }
     }
   }

ortools/sat/cp_model_solver.cc

@@ -1181,9 +1181,7 @@ CpSolverResponse SolveCpModelInternal(
     SharedBoundsManager* shared_bounds_manager, Model* model) {
   // Timing.
   WallTimer wall_timer;
-  UserTimer user_timer;
   wall_timer.Start();
-  user_timer.Start();
 
   // Initialize a default invalid response.
   CpSolverResponse response;
@@ -1200,7 +1198,6 @@ CpSolverResponse SolveCpModelInternal(
             ? 0
             : model->Get<IntegerTrail>()->num_enqueues());
     response.set_wall_time(wall_timer.Get());
-    response.set_user_time(user_timer.Get());
     response.set_deterministic_time(
         model->Get<TimeLimit>()->GetElapsedDeterministicTime());
   };
@@ -1677,9 +1674,7 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto,
 
   // Timing.
   WallTimer wall_timer;
-  UserTimer user_timer;
   wall_timer.Start();
-  user_timer.Start();
 
   auto get_literal = [](int ref) {
     if (ref >= 0) return Literal(BooleanVariable(ref), true);
@@ -1791,13 +1786,11 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto,
   response.set_num_binary_propagations(solver->num_propagations());
   response.set_num_integer_propagations(0);
   response.set_wall_time(wall_timer.Get());
-  response.set_user_time(user_timer.Get());
   response.set_deterministic_time(
       model->Get<TimeLimit>()->GetElapsedDeterministicTime());
 
   if (status == SatSolver::INFEASIBLE && drat_proof_handler != nullptr) {
     wall_timer.Restart();
-    user_timer.Restart();
     DratChecker::Status drat_status =
         drat_proof_handler->Check(FLAGS_max_drat_time_in_seconds);
     switch (drat_status) {
@@ -1815,7 +1808,6 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto,
         break;
     }
     LOG(INFO) << "DRAT wall time: " << wall_timer.Get();
-    LOG(INFO) << "DRAT user time: " << user_timer.Get();
   } else if (drat_proof_handler != nullptr) {
     // Always log a DRAT status to make it easier to extract it from a multirun
     // result with awk.
@@ -2206,8 +2198,10 @@ CpSolverResponse SolveCpModelParallel(
 }  // namespace
 
 CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
-  WallTimer timer;
-  timer.Start();
+  WallTimer wall_timer;
+  UserTimer user_timer;
+  wall_timer.Start();
+  user_timer.Start();
 
   // Validate model_proto.
   // TODO(user): provide an option to skip this step for speed?
@@ -2316,11 +2310,11 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
   const auto& observers = model->GetOrCreate<SolutionObservers>()->observers;
   int num_solutions = 0;
   std::function<void(const CpSolverResponse&)> observer_function =
-      [&model_proto, &observers, &num_solutions, &timer,
+      [&model_proto, &observers, &num_solutions, &wall_timer, &user_timer,
        &postprocess_solution](const CpSolverResponse& response) {
         const bool maximize = model_proto.objective().scaling_factor() < 0.0;
         if (VLOG_IS_ON(1)) {
-          LogNewSolution(absl::StrCat(++num_solutions), timer.Get(),
+          LogNewSolution(absl::StrCat(++num_solutions), wall_timer.Get(),
                          maximize ? response.objective_value()
                                   : response.best_objective_bound(),
                          maximize ? response.best_objective_bound()
@@ -2338,6 +2332,9 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
                                                 copy.solution().end())));
           }
         }
+
+        copy.set_wall_time(wall_timer.Get());
+        copy.set_user_time(user_timer.Get());
         for (const auto& observer : observers) {
           observer(copy);
         }
@@ -2351,7 +2348,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
 #else   // __PORTABLE_PLATFORM__
   if (params.num_search_workers() > 1) {
     response =
-        SolveCpModelParallel(new_model, observer_function, &timer, model);
+        SolveCpModelParallel(new_model, observer_function, &wall_timer, model);
 #endif  // __PORTABLE_PLATFORM__
   } else if (params.use_lns() && new_model.has_objective() &&
              !params.enumerate_all_solutions()) {
@@ -2373,8 +2370,9 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
                                                 response.solution().end())));
   }
 
-  // Fix the walltime before returning the response.
-  response.set_wall_time(timer.Get());
+  // Fix the timing information before returning the response.
+  response.set_wall_time(wall_timer.Get());
+  response.set_user_time(user_timer.Get());
   return response;
 }
 

ortools/sat/integer_search.cc

@@ -488,7 +488,7 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model) {
 void LogNewSolution(const std::string& event_or_solution_count,
                     double time_in_seconds, double obj_lb, double obj_ub,
                     const std::string& solution_info) {
-  LOG(INFO) << absl::StrFormat("#%-5s %6.2fs  obj:[%0.0f,%0.0f]  %s",
+  LOG(INFO) << absl::StrFormat("#%-5s %6.2fs  obj:[%g,%g]  %s",
                                event_or_solution_count, time_in_seconds, obj_lb,
                                obj_ub, solution_info);
 }