[CP-SAT] cleanups; tweaks shaving limits

Author: lperron

ortools/sat/cp_model_lns_test.cc

@@ -817,10 +817,8 @@ TEST(NeighborhoodGeneratorHelperTest, GetSchedulingPrecedences) {
   SharedBoundsManager shared_bounds_manager(proto);
 
   SatParameters params;
-  Model main_model;
-  ModelSharedTimeLimit time_limit(&main_model);
-  auto* shared_response_manager =
-      main_model.GetOrCreate<SharedResponseManager>();
+  ModelSharedTimeLimit time_limit(&model);
+  auto* shared_response_manager = model.GetOrCreate<SharedResponseManager>();
   NeighborhoodGeneratorHelper helper(&proto, &params, shared_response_manager,
                                      &time_limit, &shared_bounds_manager);
   random_engine_t random;

ortools/sat/cp_model_search.cc

@@ -650,6 +650,8 @@ absl::flat_hash_map<std::string, SatParameters> GetNamedParameters(
     new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
     new_params.set_use_probing_search(true);
     new_params.set_at_most_one_max_expansion_size(2);
+    const double dtime = base_params.shaving_search_deterministic_time();
+    new_params.set_shaving_search_deterministic_time(0.001);
     if (base_params.use_dual_scheduling_heuristics()) {
       AddExtraSchedulingPropagators(new_params);
     }
@@ -658,8 +660,10 @@ absl::flat_hash_map<std::string, SatParameters> GetNamedParameters(
     new_params.set_linearization_level(0);
     strategies["probing_no_lp"] = new_params;
 
-    new_params.set_linearization_level(2);
+    // Use the default deterministic time.
+    new_params.set_shaving_search_deterministic_time(dtime);
     // We want to spend more time on the LP here.
+    new_params.set_linearization_level(2);
     new_params.set_add_lp_constraints_lazily(false);
     new_params.set_root_lp_iterations(100'000);
     strategies["probing_max_lp"] = new_params;

ortools/sat/integer_search.cc

@@ -1921,15 +1921,14 @@ SatSolver::Status ContinuousProber::Probe() {
 
     // Adjust the active_limit.
     if (use_shaving_) {
-      const double deterministic_time =
-          parameters_.shaving_search_deterministic_time();
+      const double dtime = parameters_.shaving_search_deterministic_time();
       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_ < 25 * deterministic_time) {  // Bump the limit.
-        active_limit_ += deterministic_time;
+        active_limit_ = dtime;
+      } else if (active_limit_ <= 128 * dtime) {  // Bump the limit.
+        active_limit_ *= 2;
       }
     }
 
@@ -2047,8 +2046,8 @@ void ContinuousProber::LogStatistics() {
     shared_response_manager_->LogMessageWithThrottling(
         "Probe",
         absl::StrCat(
-            " (iterations=", iteration_,
-            " linearization_level=", parameters_.linearization_level(),
+            " (iterations=", iteration_, " linearization_level=",
+            parameters_.linearization_level(), " active_limit=", active_limit_,
             " shaving=", use_shaving_, " active_bool_vars=", bool_vars_.size(),
             " active_int_vars=", integer_trail_->NumIntegerVariables(),
             " literals fixed/probed=", prober_->num_new_literals_fixed(), "/",