[CP-SAT] disambiguate shaving parameters

Author: lperron

ortools/sat/cp_model_search.cc

@@ -650,7 +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();
+    // Use a small deterministic time to avoid spending too much time on
+    // shaving by default. The probing workers will increase it as needed.
     new_params.set_shaving_search_deterministic_time(0.001);
     if (base_params.use_dual_scheduling_heuristics()) {
       AddExtraSchedulingPropagators(new_params);
@@ -660,8 +661,6 @@ absl::flat_hash_map<std::string, SatParameters> GetNamedParameters(
     new_params.set_linearization_level(0);
     strategies["probing_no_lp"] = new_params;
 
-    // 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);

ortools/sat/integer_search.cc

@@ -25,7 +25,6 @@
 #include "absl/log/check.h"
 #include "absl/log/log.h"
 #include "absl/log/vlog_is_on.h"
-#include "absl/meta/type_traits.h"
 #include "absl/random/distributions.h"
 #include "absl/strings/str_cat.h"
 #include "absl/types/span.h"
@@ -1950,9 +1949,9 @@ SatSolver::Status ContinuousProber::Probe() {
 
     // Update the use_shaving_ parameter.
     // TODO(user): Currently, the heuristics is that we alternate shaving and
-    // not shaving, unless use_shaving_in_probing_search is false.
+    // not shaving, unless shaving_deterministic_time_in_probing_search is <= 0.
     use_shaving_ =
-        parameters_.use_shaving_in_probing_search() ? !use_shaving_ : false;
+        parameters_.shaving_deterministic_time_in_probing_search() > 0.0;
     trail_index_at_start_of_iteration_ = new_trail_index;
     integer_trail_index_at_start_of_iteration_ = new_integer_trail_index;
 

ortools/sat/parameters_validation.cc

@@ -88,6 +88,7 @@ std::string ValidateParameters(const SatParameters& params) {
   TEST_IS_FINITE(restart_dl_average_ratio);
   TEST_IS_FINITE(restart_lbd_average_ratio);
   TEST_IS_FINITE(shared_tree_open_leaves_per_worker);
+  TEST_IS_FINITE(shaving_deterministic_time_in_probing_search);
   TEST_IS_FINITE(shaving_search_deterministic_time);
   TEST_IS_FINITE(strategy_change_increase_ratio);
   TEST_IS_FINITE(symmetry_detection_deterministic_time_limit);

ortools/sat/sat_parameters.proto

@@ -1054,8 +1054,10 @@ message SatParameters {
   optional int32 probing_num_combinations_limit = 272 [default = 20000];
 
   // Add a shaving phase (where the solver tries to prove that the lower or
-  // upper bound of a variable are infeasible) to the probing search.
-  optional bool use_shaving_in_probing_search = 204 [default = true];
+  // upper bound of a variable are infeasible) to the probing search. (<= 0
+  // disables it).
+  optional double shaving_deterministic_time_in_probing_search = 204
+      [default = 0.001];
 
   // Specifies the amount of deterministic time spent of each try at shaving a
   // bound in the shaving search.