210 const CpModelProto& cp_model_proto,
Model* model) {
211 if (cp_model_proto.search_strategy().empty())
return nullptr;
213 std::vector<DecisionStrategyProto> strategies;
214 for (
const DecisionStrategyProto& proto : cp_model_proto.search_strategy()) {
215 strategies.push_back(proto);
218 const auto& parameters = *model->
GetOrCreate<SatParameters>();
223 return [&view, ¶meters, random, strategies]() {
224 for (
const DecisionStrategyProto& strategy : strategies) {
225 int candidate_ref = -1;
226 int64_t candidate_value = std::numeric_limits<int64_t>::max();
232 const bool randomize_decision =
233 parameters.search_random_variable_pool_size() > 1;
235 randomize_decision ? parameters.search_random_variable_pool_size()
238 for (
const LinearExpressionProto& expr : strategy.exprs()) {
239 const int var = expr.vars(0);
240 if (view.IsFixed(var))
continue;
242 int64_t coeff = expr.coeffs(0);
243 int64_t offset = expr.offset();
244 int64_t lb = view.Min(var);
245 int64_t ub = view.Max(var);
255 switch (strategy.variable_selection_strategy()) {
256 case DecisionStrategyProto::CHOOSE_FIRST:
258 case DecisionStrategyProto::CHOOSE_LOWEST_MIN:
259 value = coeff * lb + offset;
261 case DecisionStrategyProto::CHOOSE_HIGHEST_MAX:
262 value = -(coeff * ub + offset);
264 case DecisionStrategyProto::CHOOSE_MIN_DOMAIN_SIZE:
268 case DecisionStrategyProto::CHOOSE_MAX_DOMAIN_SIZE:
270 value = -(ub - lb + 1);
273 LOG(FATAL) <<
"Unknown VariableSelectionStrategy "
274 << strategy.variable_selection_strategy();
277 if (randomize_decision) {
280 const double noise = absl::Uniform(*random, 0., 1.0);
281 top_variables.
Add(ref, {-value, noise});
282 candidate_value = std::min(candidate_value, value);
283 }
else if (value < candidate_value) {
285 candidate_value = value;
290 if (strategy.variable_selection_strategy() ==
291 DecisionStrategyProto::CHOOSE_FIRST &&
292 !randomize_decision) {
298 if (candidate_value == std::numeric_limits<int64_t>::max())
continue;
301 if (randomize_decision) {
303 candidate_ref = candidates[absl::Uniform(
304 *random, 0,
static_cast<int>(candidates.size()))];
307 DecisionStrategyProto::DomainReductionStrategy selection =
308 strategy.domain_reduction_strategy();
311 case DecisionStrategyProto::SELECT_MIN_VALUE:
312 selection = DecisionStrategyProto::SELECT_MAX_VALUE;
314 case DecisionStrategyProto::SELECT_MAX_VALUE:
315 selection = DecisionStrategyProto::SELECT_MIN_VALUE;
317 case DecisionStrategyProto::SELECT_LOWER_HALF:
318 selection = DecisionStrategyProto::SELECT_UPPER_HALF;
320 case DecisionStrategyProto::SELECT_UPPER_HALF:
321 selection = DecisionStrategyProto::SELECT_LOWER_HALF;
329 const int64_t lb = view.Min(var);
330 const int64_t ub = view.Max(var);
332 case DecisionStrategyProto::SELECT_MIN_VALUE:
333 return view.LowerOrEqual(var, lb);
334 case DecisionStrategyProto::SELECT_MAX_VALUE:
335 return view.GreaterOrEqual(var, ub);
336 case DecisionStrategyProto::SELECT_LOWER_HALF:
337 return view.LowerOrEqual(var, lb + (ub - lb) / 2);
338 case DecisionStrategyProto::SELECT_UPPER_HALF:
339 return view.GreaterOrEqual(var, ub - (ub - lb) / 2);
340 case DecisionStrategyProto::SELECT_MEDIAN_VALUE:
341 return view.MedianValue(var);
342 case DecisionStrategyProto::SELECT_RANDOM_HALF:
343 return view.RandomSplit(var, lb, ub);
345 LOG(FATAL) <<
"Unknown DomainReductionStrategy "
346 << strategy.domain_reduction_strategy();
449 const CpModelProto& cp_model_proto,
450 absl::Span<const IntegerVariable> variable_mapping,
453 std::vector<int> ref_to_display;
454 for (
int i = 0;
i < cp_model_proto.variables_size(); ++
i) {
456 if (cp_model_proto.variables(
i).name().empty())
continue;
457 ref_to_display.push_back(
i);
459 std::sort(ref_to_display.begin(), ref_to_display.end(), [&](
int i,
int j) {
460 return cp_model_proto.variables(i).name() <
461 cp_model_proto.variables(j).name();
464 std::vector<std::pair<int64_t, int64_t>> old_domains(variable_mapping.size());
465 return [instrumented_strategy, model, variable_mapping, &cp_model_proto,
466 old_domains, ref_to_display]()
mutable {
468 if (!decision.
HasValue())
return decision;
472 LOG(INFO) <<
"Boolean decision " << l;
474 for (
const IntegerLiteral i_lit : encoder->GetIntegerLiterals(l)) {
475 LOG(INFO) <<
" - associated with " << i_lit;
477 for (
const auto [var, value] : encoder->GetEqualityLiterals(l)) {
478 LOG(INFO) <<
" - associated with " << var <<
" == " << value;
483 const int level = model->
Get<
Trail>()->CurrentDecisionLevel();
484 std::string to_display =
485 absl::StrCat(
"Diff since last call, level=", level,
"\n");
487 for (
const int ref : ref_to_display) {
488 const IntegerVariable var = variable_mapping[ref];
489 const std::pair<int64_t, int64_t> new_domain(
492 if (new_domain != old_domains[ref]) {
493 absl::StrAppend(&to_display, cp_model_proto.variables(ref).name(),
" [",
494 old_domains[ref].first,
",", old_domains[ref].second,
495 "] -> [", new_domain.first,
",", new_domain.second,
497 old_domains[ref] = new_domain;
500 LOG(INFO) << to_display;
506 SatParameters base_params) {
507 absl::flat_hash_map<std::string, SatParameters> strategies;
512 base_params.set_log_search_progress(
false);
515 strategies[
"default"] = base_params;
519 SatParameters new_params = base_params;
520 new_params.set_linearization_level(0);
521 strategies[
"no_lp"] = new_params;
522 new_params.set_linearization_level(1);
523 strategies[
"default_lp"] = new_params;
524 new_params.set_linearization_level(2);
525 new_params.set_add_lp_constraints_lazily(
false);
526 strategies[
"max_lp"] = new_params;
527 new_params.set_use_symmetry_in_lp(
true);
528 strategies[
"max_lp_sym"] = new_params;
538 SatParameters new_params = base_params;
539 new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
540 new_params.set_optimize_with_core(
true);
541 new_params.set_linearization_level(0);
542 strategies[
"core"] = new_params;
547 SatParameters new_params = base_params;
548 new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
549 new_params.set_optimize_with_core(
true);
550 new_params.set_linearization_level(1);
551 strategies[
"core_default_lp"] = new_params;
555 SatParameters new_params = base_params;
556 new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
557 new_params.set_optimize_with_core(
true);
558 new_params.set_linearization_level(2);
559 strategies[
"core_max_lp"] = new_params;
563 SatParameters new_params = base_params;
564 new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
565 new_params.set_optimize_with_core(
true);
566 new_params.set_optimize_with_max_hs(
true);
567 strategies[
"max_hs"] = new_params;
571 SatParameters new_params = base_params;
572 new_params.set_optimize_with_lb_tree_search(
true);
575 new_params.set_share_objective_bounds(
false);
577 new_params.set_linearization_level(0);
578 strategies[
"lb_tree_search_no_lp"] = new_params;
580 new_params.set_linearization_level(2);
581 if (base_params.use_dual_scheduling_heuristics()) {
582 AddExtraSchedulingPropagators(new_params);
585 new_params.set_add_lp_constraints_lazily(
false);
586 new_params.set_root_lp_iterations(100'000);
587 strategies[
"lb_tree_search"] = new_params;
591 SatParameters new_params = base_params;
592 new_params.set_use_objective_lb_search(
true);
594 new_params.set_linearization_level(0);
595 strategies[
"objective_lb_search_no_lp"] = new_params;
597 new_params.set_linearization_level(1);
598 strategies[
"objective_lb_search"] = new_params;
600 if (base_params.use_dual_scheduling_heuristics()) {
601 AddExtraSchedulingPropagators(new_params);
603 new_params.set_linearization_level(2);
604 strategies[
"objective_lb_search_max_lp"] = new_params;
608 SatParameters new_params = base_params;
609 new_params.set_use_objective_shaving_search(
true);
610 new_params.set_cp_model_presolve(
true);
611 new_params.set_cp_model_probing_level(0);
612 new_params.set_symmetry_level(0);
613 if (base_params.use_dual_scheduling_heuristics()) {
614 AddExtraSchedulingPropagators(new_params);
617 strategies[
"objective_shaving"] = new_params;
619 new_params.set_linearization_level(0);
620 strategies[
"objective_shaving_no_lp"] = new_params;
622 new_params.set_linearization_level(2);
623 strategies[
"objective_shaving_max_lp"] = new_params;
627 SatParameters new_params = base_params;
628 new_params.set_use_variables_shaving_search(
true);
629 new_params.set_cp_model_presolve(
true);
630 new_params.set_cp_model_probing_level(0);
631 new_params.set_symmetry_level(0);
632 new_params.set_share_objective_bounds(
false);
633 new_params.set_share_level_zero_bounds(
false);
635 strategies[
"variables_shaving"] = new_params;
637 new_params.set_linearization_level(0);
638 strategies[
"variables_shaving_no_lp"] = new_params;
640 if (base_params.use_dual_scheduling_heuristics()) {
641 AddExtraSchedulingPropagators(new_params);
643 new_params.set_linearization_level(2);
644 strategies[
"variables_shaving_max_lp"] = new_params;
648 SatParameters new_params = base_params;
649 new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
650 new_params.set_use_probing_search(
true);
651 new_params.set_at_most_one_max_expansion_size(2);
652 if (base_params.use_dual_scheduling_heuristics()) {
653 AddExtraSchedulingPropagators(new_params);
655 strategies[
"probing"] = new_params;
657 new_params.set_linearization_level(0);
658 strategies[
"probing_no_lp"] = new_params;
660 new_params.set_linearization_level(2);
662 new_params.set_add_lp_constraints_lazily(
false);
663 new_params.set_root_lp_iterations(100'000);
664 strategies[
"probing_max_lp"] = new_params;
669 SatParameters new_params = base_params;
670 new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
671 strategies[
"auto"] = new_params;
673 new_params.set_search_branching(SatParameters::FIXED_SEARCH);
674 new_params.set_use_dynamic_precedence_in_disjunctive(
false);
675 new_params.set_use_dynamic_precedence_in_cumulative(
false);
676 strategies[
"fixed"] = new_params;
682 SatParameters new_params = base_params;
683 new_params.set_search_branching(
684 SatParameters::PORTFOLIO_WITH_QUICK_RESTART_SEARCH);
685 strategies[
"quick_restart"] = new_params;
687 new_params.set_linearization_level(0);
688 strategies[
"quick_restart_no_lp"] = new_params;
690 new_params.set_linearization_level(2);
691 strategies[
"quick_restart_max_lp"] = new_params;
695 SatParameters new_params = base_params;
696 new_params.set_linearization_level(2);
697 new_params.set_search_branching(SatParameters::LP_SEARCH);
698 if (base_params.use_dual_scheduling_heuristics()) {
699 AddExtraSchedulingPropagators(new_params);
701 strategies[
"reduced_costs"] = new_params;
706 SatParameters new_params = base_params;
707 new_params.set_linearization_level(2);
708 new_params.set_search_branching(SatParameters::PSEUDO_COST_SEARCH);
709 new_params.set_exploit_best_solution(
true);
710 strategies[
"pseudo_costs"] = new_params;
715 SatParameters new_params = base_params;
716 new_params.set_boolean_encoding_level(0);
717 strategies[
"less_encoding"] = new_params;
722 SatParameters new_params = base_params;
723 new_params.set_use_shared_tree_search(
true);
724 new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
725 new_params.set_linearization_level(0);
729 new_params.set_optimize_with_core(
false);
730 new_params.set_optimize_with_lb_tree_search(
false);
731 new_params.set_optimize_with_max_hs(
false);
738 new_params.set_polarity_exploit_ls_hints(
false);
740 strategies[
"shared_tree"] = new_params;
745 SatParameters lns_params = base_params;
746 lns_params.set_stop_after_first_solution(
false);
747 lns_params.set_cp_model_presolve(
true);
750 lns_params.set_use_sat_inprocessing(
false);
751 lns_params.set_cp_model_probing_level(0);
752 lns_params.set_symmetry_level(0);
753 lns_params.set_find_big_linear_overlap(
false);
755 lns_params.set_log_search_progress(
false);
756 lns_params.set_debug_crash_on_bad_hint(
false);
757 lns_params.set_solution_pool_size(1);
758 strategies[
"lns"] = lns_params;
762 auto it = absl::c_find_if(
763 base_params.subsolver_params(),
764 [](
const SatParameters& params) { return params.name() ==
"lns"; });
765 if (it != base_params.subsolver_params().end()) {
766 lns_params.MergeFrom(*it);
769 SatParameters lns_params_base = lns_params;
770 lns_params_base.set_linearization_level(0);
771 lns_params_base.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
772 strategies[
"lns_base"] = lns_params_base;
774 SatParameters lns_params_stalling = lns_params;
775 lns_params_stalling.set_search_branching(SatParameters::PORTFOLIO_SEARCH);
776 lns_params_stalling.set_search_random_variable_pool_size(5);
777 strategies[
"lns_stalling"] = lns_params_stalling;
781 SatParameters lns_params_routing = lns_params;
782 lns_params_routing.set_linearization_level(2);
783 lns_params_routing.set_search_branching(SatParameters::AUTOMATIC_SEARCH);
784 strategies[
"lns_routing"] = lns_params_routing;
789 for (
const SatParameters& params : base_params.subsolver_params()) {
790 auto it = strategies.find(params.name());
791 if (it != strategies.end()) {
792 it->second.MergeFrom(params);
796 SatParameters new_params = base_params;
797 new_params.MergeFrom(params);
798 strategies[params.name()] = new_params;
803 for (
auto& [name, params] : strategies) {
804 params.set_name(name);
818 const SatParameters& base_params,
const CpModelProto& cp_model,
830 const bool use_fixed_strategy = !cp_model.search_strategy().empty() ||
831 ModelHasSchedulingConstraints(cp_model);
837 std::vector<std::string> names;
840 for (
const std::string& name : base_params.extra_subsolvers()) {
841 names.push_back(name);
845 if (base_params.subsolvers().empty()) {
847 names.push_back(
"default_lp");
848 names.push_back(
"fixed");
849 names.push_back(
"core");
850 names.push_back(
"no_lp");
851 if (cp_model.has_symmetry()) {
852 names.push_back(
"max_lp_sym");
856 names.push_back(
"max_lp");
858 names.push_back(
"quick_restart");
859 names.push_back(
"reduced_costs");
860 names.push_back(
"quick_restart_no_lp");
861 names.push_back(
"pseudo_costs");
862 names.push_back(
"lb_tree_search");
863 names.push_back(
"probing");
864 names.push_back(
"objective_lb_search");
865 names.push_back(
"objective_shaving_no_lp");
866 names.push_back(
"objective_shaving_max_lp");
867 names.push_back(
"probing_max_lp");
868 names.push_back(
"probing_no_lp");
869 names.push_back(
"objective_lb_search_no_lp");
870 names.push_back(
"objective_lb_search_max_lp");
871 if (cp_model.has_symmetry()) {
872 names.push_back(
"max_lp");
875 for (
const std::string& name : base_params.subsolvers()) {
878 if (name ==
"core_or_no_lp") {
879 if (!cp_model.has_objective() ||
880 cp_model.objective().vars_size() <= 1) {
881 names.push_back(
"no_lp");
883 names.push_back(
"core");
886 names.push_back(name);
893 for (
const std::string& name : names) {
894 if (filter->
Keep(name)) {
895 names[new_size++] = name;
898 names.resize(new_size);
901 std::vector<SatParameters> result;
902 for (
const std::string& name : names) {
903 SatParameters params = strategies.at(name);
906 if (!use_fixed_strategy &&
907 params.search_branching() == SatParameters::FIXED_SEARCH) {
914 if (params.use_probing_search() && params.interleave_search())
continue;
918 if ((params.use_objective_shaving_search() ||
919 params.use_variables_shaving_search()) &&
920 params.interleave_search()) {
926 if (params.use_probing_search() && cp_model.variables().empty())
continue;
928 if (cp_model.has_objective() && !cp_model.objective().vars().empty()) {
930 if (cp_model.objective().vars().size() == 1 &&
931 params.optimize_with_core()) {
935 if (name ==
"less_encoding")
continue;
940 if (params.interleave_search() &&
941 (params.optimize_with_lb_tree_search() ||
942 params.use_objective_lb_search())) {
947 if (params.optimize_with_lb_tree_search())
continue;
948 if (params.optimize_with_core())
continue;
949 if (params.use_objective_lb_search())
continue;
950 if (params.use_objective_shaving_search())
continue;
951 if (params.search_branching() == SatParameters::LP_SEARCH)
continue;
952 if (params.search_branching() == SatParameters::PSEUDO_COST_SEARCH) {
958 params.set_name(name);
960 base_params.random_seed(),
static_cast<int64_t
>(result.size()) + 1));
961 result.push_back(params);
968 if (base_params.interleave_search())
return result;
971 int num_to_keep = base_params.num_full_subsolvers();
972 if (num_to_keep == 0) {
975 const int num_available =
976 std::max(0, base_params.num_workers() - num_already_present);
978 const auto heuristic_num_workers = [](
int num_workers) {
979 DCHECK_GE(num_workers, 0);
980 if (num_workers == 1)
return 1;
981 if (num_workers <= 4)
return num_workers - 1;
982 if (num_workers <= 8)
return num_workers - 2;
983 if (num_workers <= 16)
return num_workers - (num_workers / 4 + 1);
984 return num_workers - (num_workers / 2 - 3);
987 num_to_keep = heuristic_num_workers(num_available);
990 if (result.size() > num_to_keep) {
991 result.resize(std::max(0, num_to_keep));
997 const SatParameters& base_params) {
998 std::vector<SatParameters> result;
1000 const auto get_base = [&result, &base_params](
bool fj) {
1001 SatParameters new_params = base_params;
1002 new_params.set_log_search_progress(
false);
1003 new_params.set_use_feasibility_jump(fj);
1005 const int base_seed = base_params.random_seed();
1006 new_params.set_random_seed(
CombineSeed(base_seed, result.size()));
1011 if (base_params.use_feasibility_jump()) {
1012 SatParameters new_params = get_base(
true);
1013 new_params.set_name(
"fj");
1014 new_params.set_feasibility_jump_linearization_level(0);
1015 result.push_back(new_params);
1019 for (
int i = 0;
i < 2; ++
i) {
1020 SatParameters new_params = get_base(
false);
1021 new_params.set_search_random_variable_pool_size(5);
1022 new_params.set_search_branching(SatParameters::RANDOMIZED_SEARCH);
1024 new_params.set_name(
"fs_random_no_lp");
1025 new_params.set_linearization_level(0);
1027 new_params.set_name(
"fs_random");
1029 result.push_back(new_params);
1033 if (base_params.use_feasibility_jump()) {
1034 SatParameters new_params = get_base(
true);
1035 new_params.set_name(
"fj");
1036 new_params.set_feasibility_jump_linearization_level(0);
1037 result.push_back(new_params);
1041 for (
int i = 0;
i < 2; ++
i) {
1042 SatParameters new_params = get_base(
false);
1043 new_params.set_search_random_variable_pool_size(5);
1044 new_params.set_search_branching(
1045 SatParameters::PORTFOLIO_WITH_QUICK_RESTART_SEARCH);
1047 new_params.set_name(
"fs_random_quick_restart_no_lp");
1048 new_params.set_linearization_level(0);
1050 new_params.set_name(
"fs_random_quick_restart");
1052 result.push_back(new_params);
1058 if (base_params.use_feasibility_jump()) {
1059 SatParameters new_params = get_base(
true);
1060 new_params.set_name(
"fj_lin");
1061 new_params.set_feasibility_jump_linearization_level(2);
1062 result.push_back(new_params);