[CP-SAT] cleanups; tweaks shaving limits

This commit is contained in:
Laurent Perron
2025-04-15 17:19:41 +02:00
parent 714ba15a4e
commit 467091fe92
3 changed files with 13 additions and 12 deletions

View File

@@ -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;

View File

@@ -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;

View File

@@ -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(), "/",