From e0c05ab965cee183f5fc3403a55718c4633a2b64 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Tue, 15 Apr 2025 21:04:21 +0200 Subject: [PATCH] [CP-SAT] disambiguate shaving parameters --- ortools/sat/cp_model_search.cc | 5 ++--- ortools/sat/integer_search.cc | 5 ++--- ortools/sat/parameters_validation.cc | 1 + ortools/sat/sat_parameters.proto | 6 ++++-- 4 files changed, 9 insertions(+), 8 deletions(-) diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 6a6375aae2..ff253b4041 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -650,7 +650,8 @@ absl::flat_hash_map 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 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); diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 749f705f78..0d5de45924 100644 --- a/ortools/sat/integer_search.cc +++ b/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; diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc index 4d3125585a..fc889abcf3 100644 --- a/ortools/sat/parameters_validation.cc +++ b/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); diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 96f345d909..0f28a03181 100644 --- a/ortools/sat/sat_parameters.proto +++ b/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.