From ff8e0d249b54cc200849f424a1e61283fbb004ff Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Wed, 9 Aug 2023 14:25:48 -0700 Subject: [PATCH] tweak subsolvers list; add focus on terms parameters to lb_objective_search; fix bug in shared_tree --- ortools/sat/BUILD.bazel | 1 + ortools/sat/cp_model_search.cc | 25 +++++++--- ortools/sat/integer_search.cc | 72 +++++++++++++++++++++++----- ortools/sat/parameters_validation.cc | 1 + ortools/sat/sat_parameters.proto | 6 +++ ortools/sat/sat_runner.cc | 51 ++++++++++---------- ortools/sat/subsolver.h | 2 +- ortools/sat/table.h | 2 +- ortools/sat/work_assignment.cc | 19 ++++---- 9 files changed, 123 insertions(+), 56 deletions(-) diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index d76066e9653..23a64a08804 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -1721,6 +1721,7 @@ cc_binary( "//ortools/algorithms:sparse_permutation", "//ortools/base", "//ortools/base:file", + "//ortools/base:path", "//ortools/base:threadpool", "//ortools/lp_data:mps_reader", "//ortools/lp_data:proto_utils", diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 79d523f8a6c..532a44ea5df 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -508,16 +508,17 @@ absl::flat_hash_map GetNamedParameters( { SatParameters new_params = base_params; - new_params.set_linearization_level(1); new_params.set_use_objective_lb_search(true); - if (base_params.use_dual_scheduling_heuristics()) { - AddDualSchedulingHeuristics(new_params); - } - strategies["objective_lb_search"] = new_params; new_params.set_linearization_level(0); strategies["objective_lb_search_no_lp"] = new_params; + new_params.set_linearization_level(1); + strategies["objective_lb_search"] = new_params; + + if (base_params.use_dual_scheduling_heuristics()) { + AddDualSchedulingHeuristics(new_params); + } new_params.set_linearization_level(2); strategies["objective_lb_search_max_lp"] = new_params; } @@ -548,6 +549,9 @@ absl::flat_hash_map GetNamedParameters( strategies["probing_no_lp"] = new_params; new_params.set_linearization_level(2); + // We want to spend more time on the LP here. + new_params.set_add_lp_constraints_lazily(false); + new_params.set_root_lp_iterations(100'000); strategies["probing_max_lp"] = new_params; } @@ -673,6 +677,15 @@ std::vector GetDiverseSetOfParameters( if (num_workers_to_generate >= 24) { names.push_back("objective_shaving_search"); } + if (num_workers_to_generate >= 26) { + names.push_back("objective_lb_search_no_lp"); + } + if (num_workers_to_generate >= 28) { + names.push_back("objective_lb_search_max_lp"); + } + if (num_workers_to_generate >= 30) { + names.push_back("core_max_lp"); + } #if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP) if (absl::GetFlag(FLAGS_cp_model_use_max_hs)) names.push_back("max_hs"); #endif // !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP) @@ -725,7 +738,7 @@ std::vector GetDiverseSetOfParameters( if (params.use_probing_search() && cp_model.variables().empty()) continue; if (cp_model.has_objective() && !cp_model.objective().vars().empty()) { - // Disable core search if only 1 term in the objective. + // Disable core search if there is only 1 term in the objective. if (cp_model.objective().vars().size() == 1 && params.optimize_with_core()) { continue; diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index c61c558dfd0..8ae5b34728d 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -17,6 +17,7 @@ #include #include #include +#include #include #include @@ -336,26 +337,69 @@ std::function SatSolverHeuristic(Model* model) { // TODO(user): Do we need a mechanism to reduce the range of possible gaps // when nothing gets proven? This could be a parameter or some adaptative code. -std::function ShaveObjectiveLb(Model* model) { +std::function ShaveObjectiveLb( + Model* model, double focus_on_terms_probability) { auto* objective_definition = model->GetOrCreate(); const IntegerVariable obj_var = objective_definition->objective_var; auto* integer_trail = model->GetOrCreate(); auto* sat_solver = model->GetOrCreate(); auto* random = model->GetOrCreate(); - return [obj_var, integer_trail, sat_solver, random]() { + std::vector random_order; + if (objective_definition->vars.size() > 1) { + random_order.resize(objective_definition->vars.size()); + std::iota(random_order.begin(), random_order.end(), 0); + } + + const auto random_slack = [random](IntegerValue lb, IntegerValue ub) { + const IntegerValue mid = (ub - lb) / 2; + return absl::LogUniform(*random, 0, mid.value()); + }; + + return [obj_var, integer_trail, sat_solver, random, random_order, + objective_definition, random_slack, + focus_on_terms_probability]() mutable { BooleanOrIntegerLiteral result; const int level = sat_solver->CurrentDecisionLevel(); - if (level > 0 || obj_var == kNoIntegerVariable) return result; + if (random_order.empty() || + absl::Bernoulli(*random, 1.0 - focus_on_terms_probability)) { + if (level > 0 || obj_var == kNoIntegerVariable || + integer_trail->IsFixed(obj_var)) { + return result; + } + + const IntegerValue obj_lb = integer_trail->LowerBound(obj_var); + const IntegerValue obj_ub = integer_trail->UpperBound(obj_var); + const IntegerValue new_ub = obj_lb + random_slack(obj_lb, obj_ub); + result.integer_literal = IntegerLiteral::LowerOrEqual(obj_var, new_ub); + return result; + } - const IntegerValue obj_lb = integer_trail->LowerBound(obj_var); - const IntegerValue obj_ub = integer_trail->UpperBound(obj_var); - if (obj_lb == obj_ub) return result; - const IntegerValue mid = (obj_ub - obj_lb) / 2; - const IntegerValue new_ub = - obj_lb + absl::LogUniform(*random, 0, mid.value()); + if (level == 0) { + VLOG(2) << "ShaveObjectiveLb: randomize " << random_order.size() + << " terms"; + DCHECK_EQ(random_order.size(), objective_definition->vars.size()); + std::shuffle(random_order.begin(), random_order.end(), *random); + } - result.integer_literal = IntegerLiteral::LowerOrEqual(obj_var, new_ub); + for (const int index : random_order) { + const IntegerVariable var = objective_definition->vars[index]; + const IntegerValue coeff = objective_definition->coeffs[index]; + if (integer_trail->IsFixed(var) || coeff == 0) continue; + + const IntegerValue lb = integer_trail->LowerBound(var); + const IntegerValue ub = integer_trail->UpperBound(var); + const IntegerValue slack = random_slack(lb, ub); + if (coeff > 0) { + result.integer_literal = IntegerLiteral::LowerOrEqual(var, lb + slack); + } else { + result.integer_literal = + IntegerLiteral::GreaterOrEqual(var, ub - slack); + } + return result; + } + + // Returns no-decision. return result; }; } @@ -698,8 +742,12 @@ void ConfigureSearchHeuristics(Model* model) { SequentialSearch({decision_policy, heuristics.fixed_search}); decision_policy = IntegerValueSelectionHeuristic(decision_policy, model); if (parameters.use_objective_lb_search()) { - heuristics.decision_policies = { - SequentialSearch({ShaveObjectiveLb(model), decision_policy})}; + heuristics.decision_policies = {SequentialSearch( + {ShaveObjectiveLb( + model, + parameters + .focus_on_terms_in_objective_lb_search_probability()), + decision_policy})}; } else { heuristics.decision_policies = {decision_policy}; } diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc index 57823cc0f3a..765ca7ac693 100644 --- a/ortools/sat/parameters_validation.cc +++ b/ortools/sat/parameters_validation.cc @@ -101,6 +101,7 @@ std::string ValidateParameters(const SatParameters& params) { TEST_IN_RANGE(min_num_lns_workers, 0, kMaxReasonableParallelism); TEST_IN_RANGE(shared_tree_num_workers, 0, kMaxReasonableParallelism); TEST_IN_RANGE(interleave_batch_size, 0, kMaxReasonableParallelism); + TEST_IN_RANGE(focus_on_terms_in_objective_lb_search_probability, 0.0, 1.0); // TODO(user): Consider using annotations directly in the proto for these // validation. It is however not open sourced. diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index ccfaafa068b..06d89a45b29 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -1036,6 +1036,12 @@ message SatParameters { // minimizing) starting from the lower bound of the objective. optional bool use_objective_lb_search = 228 [default = false]; + // With the given probability, objective_lb_search will fix each terms of the + // objective following an random order computed each time search returns to + // the root node. + optional double focus_on_terms_in_objective_lb_search_probability = 231 + [default = 0.5]; + // This search differs from the previous search as it will not use assumptions // to bound the objective, and it will recreate a full model with the // hardcoded objective value. diff --git a/ortools/sat/sat_runner.cc b/ortools/sat/sat_runner.cc index 58b15ccde54..7430da1780a 100644 --- a/ortools/sat/sat_runner.cc +++ b/ortools/sat/sat_runner.cc @@ -11,12 +11,8 @@ // See the License for the specific language governing permissions and // limitations under the License. -#include #include -#include #include -#include -#include #include "absl/flags/flag.h" #include "absl/flags/parse.h" @@ -24,42 +20,22 @@ #include "absl/log/check.h" #include "absl/log/flags.h" #include "absl/log/initialize.h" -#include "absl/random/random.h" -#include "absl/status/status.h" #include "absl/strings/match.h" -#include "absl/strings/numbers.h" -#include "absl/strings/str_cat.h" -#include "absl/strings/str_format.h" #include "absl/strings/string_view.h" #include "google/protobuf/text_format.h" -#include "ortools/algorithms/sparse_permutation.h" #include "ortools/base/helpers.h" #include "ortools/base/logging.h" #include "ortools/base/options.h" -#include "ortools/base/timer.h" -#include "ortools/linear_solver/linear_solver.pb.h" -#include "ortools/lp_data/lp_data.h" -#include "ortools/lp_data/mps_reader.h" -#include "ortools/lp_data/proto_utils.h" +#include "ortools/base/path.h" #include "ortools/sat/boolean_problem.h" #include "ortools/sat/boolean_problem.pb.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_solver.h" -#include "ortools/sat/lp_utils.h" #include "ortools/sat/model.h" #include "ortools/sat/opb_reader.h" -#include "ortools/sat/optimization.h" -#include "ortools/sat/pb_constraint.h" -#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_cnf_reader.h" #include "ortools/sat/sat_parameters.pb.h" -#include "ortools/sat/sat_solver.h" -#include "ortools/sat/simplification.h" -#include "ortools/sat/symmetry.h" #include "ortools/util/file_util.h" -#include "ortools/util/logging.h" -#include "ortools/util/strong_integers.h" -#include "ortools/util/time_limit.h" ABSL_FLAG( std::string, input, "", @@ -83,7 +59,25 @@ namespace operations_research { namespace sat { namespace { -bool LoadBooleanProblem(const std::string& filename, CpModelProto* cp_model) { +void TryToRemoveSuffix(absl::string_view suffix, std::string* str) { + if (file::Extension(*str) == suffix) *str = file::Stem(*str); +} + +std::string ExtractName(const std::string& full_filename) { + std::string filename = std::string(file::Basename(full_filename)); + // The order is important as '.pb.txt.gz' is a common suffix. + TryToRemoveSuffix("gz", &filename); + TryToRemoveSuffix("txt", &filename); + TryToRemoveSuffix("pb", &filename); + TryToRemoveSuffix("pbtxt", &filename); + TryToRemoveSuffix("proto", &filename); + TryToRemoveSuffix("prototxt", &filename); + TryToRemoveSuffix("textproto", &filename); + TryToRemoveSuffix("bin", &filename); + return filename; +} + +bool LoadProblem(const std::string& filename, CpModelProto* cp_model) { if (absl::EndsWith(filename, ".opb") || absl::EndsWith(filename, ".opb.bz2")) { OpbReader reader; @@ -106,6 +100,9 @@ bool LoadBooleanProblem(const std::string& filename, CpModelProto* cp_model) { LOG(INFO) << "Reading a CpModelProto."; *cp_model = ReadFileToProtoOrDie(filename); } + if (cp_model->name().empty()) { + cp_model->set_name(ExtractName(filename)); + } return true; } @@ -127,7 +124,7 @@ int Run() { google::protobuf::Arena arena; CpModelProto* cp_model = google::protobuf::Arena::CreateMessage(&arena); - if (!LoadBooleanProblem(absl::GetFlag(FLAGS_input), cp_model)) { + if (!LoadProblem(absl::GetFlag(FLAGS_input), cp_model)) { CpSolverResponse response; response.set_status(CpSolverStatus::MODEL_INVALID); return EXIT_SUCCESS; diff --git a/ortools/sat/subsolver.h b/ortools/sat/subsolver.h index d1b6bc3f10b..95301be1156 100644 --- a/ortools/sat/subsolver.h +++ b/ortools/sat/subsolver.h @@ -27,7 +27,7 @@ #include #include "absl/strings/string_view.h" -#include "ortools/base/integral_types.h" +#include "ortools/base/types.h" #include "ortools/util/stats.h" #if !defined(__PORTABLE_PLATFORM__) diff --git a/ortools/sat/table.h b/ortools/sat/table.h index 6f8e8916b4c..b3255bd09bb 100644 --- a/ortools/sat/table.h +++ b/ortools/sat/table.h @@ -19,7 +19,7 @@ #include #include "absl/types/span.h" -#include "ortools/base/integral_types.h" +#include "ortools/base/types.h" #include "ortools/sat/integer.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" diff --git a/ortools/sat/work_assignment.cc b/ortools/sat/work_assignment.cc index d672d54b68b..ad45da2316f 100644 --- a/ortools/sat/work_assignment.cc +++ b/ortools/sat/work_assignment.cc @@ -178,7 +178,9 @@ absl::Span ProtoTrail::NodeIds(int level) const { } absl::Span ProtoTrail::Implications(int level) const { - DCHECK_LE(level, decision_indexes_.size()); + if (level > decision_indexes_.size()) { + return absl::MakeSpan(literals_.data(), 0); + } int start = level == 0 ? 0 : decision_indexes_[level - 1] + 1; int end = level == decision_indexes_.size() ? node_ids_.size() : decision_indexes_[level]; @@ -561,20 +563,19 @@ bool SharedTreeWorker::AddImplications( } bool SharedTreeWorker::SyncWithLocalTrail() { - if (sat_solver_->CurrentDecisionLevel() > assigned_tree_.MaxLevel()) { - return sat_solver_->FinishPropagation() && helper_->BeforeTakingDecision(); - } - while (sat_solver_->CurrentDecisionLevel() <= assigned_tree_.MaxLevel()) { + while (true) { + if (!sat_solver_->FinishPropagation()) return false; // Ensure we are at fixed point w.r.t. implications in the tree up to the // current level. - while (AddImplications( - assigned_tree_.Implications(sat_solver_->CurrentDecisionLevel()))) { - if (!sat_solver_->FinishPropagation()) return false; + if (AddImplications( + assigned_tree_.Implications(sat_solver_->CurrentDecisionLevel()))) { + continue; } if (!helper_->BeforeTakingDecision()) return false; const int level = sat_solver_->CurrentDecisionLevel(); - // Make sure the next assigned decision makes sense if there is one. + if (level >= assigned_tree_.MaxLevel()) break; if (level == assigned_tree_.MaxLevel()) break; + // The next decision is assigned, make sure it makes sense. const Literal next_decision = assigned_tree_literals_[level]; if (!sat_solver_->Assignment().LiteralIsAssigned(next_decision)) break; if (sat_solver_->Assignment().LiteralIsFalse(next_decision)) {