From ba15d312ba4cf5ed1cf802a83aec23cdd1c17aca Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Wed, 11 May 2022 17:23:59 +0200 Subject: [PATCH] [CP-SAT] improve cuts diversity; fix infinite loop in the ttef constraint; improve var domination; remove wrong DCHECK --- ortools/sat/BUILD.bazel | 4 - ortools/sat/cp_model_loader.cc | 3 +- ortools/sat/cp_model_solver.cc | 93 ++++++++++---------- ortools/sat/cp_model_symmetries.cc | 3 +- ortools/sat/cuts.cc | 1 - ortools/sat/drat_proof_handler.cc | 3 +- ortools/sat/integer_expr.cc | 1 - ortools/sat/linear_programming_constraint.cc | 9 +- ortools/sat/linear_relaxation.cc | 1 - ortools/sat/sat_parameters.proto | 5 +- ortools/sat/scheduling_constraints.cc | 2 - ortools/sat/simplification.cc | 5 +- ortools/sat/timetable_edgefinding.cc | 17 ++-- ortools/sat/var_domination.cc | 87 +++++++++++------- ortools/sat/var_domination.h | 7 +- 15 files changed, 123 insertions(+), 118 deletions(-) diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 6d590415ce..016bc75cd6 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -236,7 +236,6 @@ cc_library( "@com_google_absl//absl/base:core_headers", "@com_google_absl//absl/container:btree", "@com_google_absl//absl/container:flat_hash_set", - "@com_google_absl//absl/memory", "@com_google_absl//absl/status", "@com_google_absl//absl/strings", "@com_google_absl//absl/strings:str_format", @@ -598,7 +597,6 @@ cc_library( "//ortools/util:strong_integers", "//ortools/util:time_limit", "@com_google_absl//absl/container:btree", - "@com_google_absl//absl/memory", "@com_google_absl//absl/types:span", ], ) @@ -1447,7 +1445,6 @@ cc_library( "//ortools/base:strong_vector", "//ortools/util:strong_integers", "@com_google_absl//absl/hash", - "@com_google_absl//absl/memory", "@com_google_absl//absl/status", "@com_google_absl//absl/types:span", ], @@ -1508,7 +1505,6 @@ cc_library( "//ortools/base:hash", "//ortools/util:logging", "@com_google_absl//absl/container:flat_hash_map", - "@com_google_absl//absl/memory", "@com_google_protobuf//:protobuf", ], ) diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 55a02dce11..bd18196aae 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -24,7 +24,6 @@ #include "absl/container/btree_set.h" #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" -#include "absl/memory/memory.h" #include "absl/meta/type_traits.h" #include "absl/strings/str_cat.h" #include "absl/types/span.h" @@ -312,7 +311,7 @@ void LoadBooleanSymmetries(const CpModelProto& model_proto, Model* m) { // Convert the variable symmetry to a "literal" one. auto literal_permutation = - absl::make_unique(num_literals); + std::make_unique(num_literals); int support_index = 0; const int num_cycle = perm.cycle_sizes().size(); for (int i = 0; i < num_cycle; ++i) { diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 6428ece05e..ae8421881d 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -38,7 +38,6 @@ #include "absl/container/btree_set.h" #include "absl/container/flat_hash_set.h" #include "absl/flags/flag.h" -#include "absl/memory/memory.h" #include "absl/status/status.h" #include "absl/status/statusor.h" #include "absl/strings/str_cat.h" @@ -1861,10 +1860,10 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto, File* output; CHECK_OK(file::Open(absl::GetFlag(FLAGS_drat_output), "w", &output, file::Defaults())); - drat_proof_handler = absl::make_unique( + drat_proof_handler = std::make_unique( /*in_binary_format=*/false, output, absl::GetFlag(FLAGS_drat_check)); } else { - drat_proof_handler = absl::make_unique(); + drat_proof_handler = std::make_unique(); } solver->SetDratProofHandler(drat_proof_handler.get()); } @@ -2085,7 +2084,7 @@ class FullProblemSolver : public SubSolver { : SubSolver(name), shared_(shared), split_in_chunks_(split_in_chunks), - local_model_(absl::make_unique(name)) { + local_model_(std::make_unique(name)) { // Setup the local model parameters and time limit. *(local_model_->GetOrCreate()) = local_parameters; shared_->time_limit->UpdateLocalLimit( @@ -2269,7 +2268,7 @@ class FeasibilityPumpSolver : public SubSolver { SharedClasses* shared) : SubSolver("feasibility_pump"), shared_(shared), - local_model_(absl::make_unique(name_)) { + local_model_(std::make_unique(name_)) { // Setup the local model parameters and time limit. *(local_model_->GetOrCreate()) = local_parameters; shared_->time_limit->UpdateLocalLimit( @@ -2476,7 +2475,7 @@ class LnsSolver : public SubSolver { // Presolve and solve the LNS fragment. CpModelProto lns_fragment; CpModelProto mapping_proto; - auto context = absl::make_unique( + auto context = std::make_unique( &local_model, &lns_fragment, &mapping_proto); *lns_fragment.mutable_variables() = neighborhood.delta.variables(); @@ -2759,20 +2758,20 @@ void SolveCpModelParallel(const CpModelProto& model_proto, std::unique_ptr shared_bounds_manager; if (params.share_level_zero_bounds()) { - shared_bounds_manager = absl::make_unique(model_proto); + shared_bounds_manager = std::make_unique(model_proto); } std::unique_ptr shared_relaxation_solutions; if (params.use_relaxation_lns()) { shared_relaxation_solutions = - absl::make_unique( + std::make_unique( /*num_solutions_to_keep=*/10); global_model->Register( shared_relaxation_solutions.get()); } - auto shared_lp_solutions = absl::make_unique( + auto shared_lp_solutions = std::make_unique( /*num_solutions_to_keep=*/10); global_model->Register(shared_lp_solutions.get()); @@ -2784,14 +2783,14 @@ void SolveCpModelParallel(const CpModelProto& model_proto, !params.use_lns_only() && !params.interleave_search(); if (use_feasibility_pump) { shared_incomplete_solutions = - absl::make_unique(); + std::make_unique(); global_model->Register( shared_incomplete_solutions.get()); } std::unique_ptr shared_clauses; if (params.share_binary_clauses()) { - shared_clauses = absl::make_unique(); + shared_clauses = std::make_unique(); } SharedClasses shared; @@ -2810,7 +2809,7 @@ void SolveCpModelParallel(const CpModelProto& model_proto, std::vector> subsolvers; // Add a synchronization point for the shared classes. - subsolvers.push_back(absl::make_unique([&shared]() { + subsolvers.push_back(std::make_unique([&shared]() { shared.response->Synchronize(); shared.response->MutableSolutionsRepository()->Synchronize(); if (shared.bounds != nullptr) { @@ -2831,7 +2830,7 @@ void SolveCpModelParallel(const CpModelProto& model_proto, SatParameters local_params = params; local_params.set_stop_after_first_solution(true); local_params.set_linearization_level(0); - subsolvers.push_back(absl::make_unique( + subsolvers.push_back(std::make_unique( "first_solution", local_params, /*split_in_chunks=*/false, &shared)); } else { @@ -2840,7 +2839,7 @@ void SolveCpModelParallel(const CpModelProto& model_proto, // TODO(user): This is currently not supported here. if (params.optimize_with_max_hs()) continue; - subsolvers.push_back(absl::make_unique( + subsolvers.push_back(std::make_unique( local_params.name(), local_params, /*split_in_chunks=*/params.interleave_search(), &shared)); } @@ -2850,14 +2849,14 @@ void SolveCpModelParallel(const CpModelProto& model_proto, // Add FeasibilityPumpSolver if enabled. if (use_feasibility_pump) { subsolvers.push_back( - absl::make_unique(params, &shared)); + std::make_unique(params, &shared)); } // Add LNS SubSolver(s). // Add the NeighborhoodGeneratorHelper as a special subsolver so that its // Synchronize() is called before any LNS neighborhood solvers. - auto unique_helper = absl::make_unique( + auto unique_helper = std::make_unique( &model_proto, ¶ms, shared.response, shared.bounds); NeighborhoodGeneratorHelper* helper = unique_helper.get(); subsolvers.push_back(std::move(unique_helper)); @@ -2876,20 +2875,20 @@ void SolveCpModelParallel(const CpModelProto& model_proto, if (model_proto.has_objective()) { // Enqueue all the possible LNS neighborhood subsolvers. // Each will have their own metrics. - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("rnd_var_lns_", local_params.name())), local_params, helper, &shared)); - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("rnd_cst_lns_", local_params.name())), local_params, helper, &shared)); - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("graph_var_lns_", local_params.name())), local_params, helper, &shared)); - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("graph_cst_lns_", local_params.name())), local_params, helper, &shared)); @@ -2898,13 +2897,13 @@ void SolveCpModelParallel(const CpModelProto& model_proto, if (!helper->TypeToConstraints(ConstraintProto::kNoOverlap).empty() || !helper->TypeToConstraints(ConstraintProto::kNoOverlap2D).empty() || !helper->TypeToConstraints(ConstraintProto::kCumulative).empty()) { - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("scheduling_time_window_lns_", local_params.name())), local_params, helper, &shared)); - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("scheduling_random_lns_", local_params.name())), local_params, helper, &shared)); @@ -2913,8 +2912,8 @@ void SolveCpModelParallel(const CpModelProto& model_proto, const std::vector> intervals_in_constraints = helper->GetUniqueIntervalSets(); if (intervals_in_constraints.size() > 2) { - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, intervals_in_constraints, absl::StrCat("scheduling_resource_windows_lns_", local_params.name())), @@ -2927,19 +2926,19 @@ void SolveCpModelParallel(const CpModelProto& model_proto, const int num_routes = helper->TypeToConstraints(ConstraintProto::kRoutes).size(); if (num_circuit + num_routes > 0) { - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("routing_random_lns_", local_params.name())), local_params, helper, &shared)); - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("routing_path_lns_", local_params.name())), local_params, helper, &shared)); } if (num_routes > 0 || num_circuit > 1) { - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("routing_full_path_lns_", local_params.name())), local_params, helper, &shared)); @@ -2954,16 +2953,16 @@ void SolveCpModelParallel(const CpModelProto& model_proto, // create RINS/RENS lns generators. // RINS. - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, shared.response, shared.relaxation_solutions, shared.lp_solutions, /*incomplete_solutions=*/nullptr, absl::StrCat("rins_lns_", local_params.name())), local_params, helper, &shared)); // RENS. - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, /*respons_manager=*/nullptr, shared.relaxation_solutions, shared.lp_solutions, shared.incomplete_solutions, absl::StrCat("rens_lns_", local_params.name())), @@ -2971,14 +2970,14 @@ void SolveCpModelParallel(const CpModelProto& model_proto, } if (params.use_relaxation_lns()) { - subsolvers.push_back(absl::make_unique( - absl::make_unique< + subsolvers.push_back(std::make_unique( + std::make_unique< ConsecutiveConstraintsRelaxationNeighborhoodGenerator>( helper, absl::StrCat("rnd_rel_lns_", local_params.name())), local_params, helper, &shared)); - subsolvers.push_back(absl::make_unique( - absl::make_unique( + subsolvers.push_back(std::make_unique( + std::make_unique( helper, absl::StrCat("wgt_rel_lns_", local_params.name())), local_params, helper, &shared)); } @@ -2987,7 +2986,7 @@ void SolveCpModelParallel(const CpModelProto& model_proto, // Add a synchronization point for the gap integral that is executed last. // This way, after each batch, the proper deterministic time is updated and // then the function to integrate take the value of the new gap. - subsolvers.push_back(absl::make_unique( + subsolvers.push_back(std::make_unique( [&shared]() { shared.response->UpdateGapIntegral(); })); // Log the name of all our SubSolvers. @@ -3285,8 +3284,8 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) { absl::StrFormat("Starting presolve at %.2fs", wall_timer->Get())); CpModelProto new_cp_model_proto; CpModelProto mapping_proto; - auto context = absl::make_unique(model, &new_cp_model_proto, - &mapping_proto); + auto context = std::make_unique(model, &new_cp_model_proto, + &mapping_proto); if (!ImportModelWithBasicPresolveIntoContext(model_proto, context.get())) { VLOG(1) << "Model found infeasible during copy"; diff --git a/ortools/sat/cp_model_symmetries.cc b/ortools/sat/cp_model_symmetries.cc index fb4604c08e..c01107e27e 100644 --- a/ortools/sat/cp_model_symmetries.cc +++ b/ortools/sat/cp_model_symmetries.cc @@ -24,7 +24,6 @@ #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" -#include "absl/memory/memory.h" #include "absl/meta/type_traits.h" #include "absl/status/status.h" #include "absl/strings/str_cat.h" @@ -114,7 +113,7 @@ std::unique_ptr GenerateGraphForSymmetryDetection( CHECK(initial_equivalence_classes != nullptr); const int num_variables = problem.variables_size(); - auto graph = absl::make_unique(); + auto graph = std::make_unique(); // Each node will be created with a given color. Two nodes of different color // can never be send one into another by a symmetry. The first element of diff --git a/ortools/sat/cuts.cc b/ortools/sat/cuts.cc index dfaba9128e..b6109e6dc7 100644 --- a/ortools/sat/cuts.cc +++ b/ortools/sat/cuts.cc @@ -27,7 +27,6 @@ #include "absl/container/btree_set.h" #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" -#include "absl/memory/memory.h" #include "absl/meta/type_traits.h" #include "ortools/base/logging.h" #include "ortools/base/stl_util.h" diff --git a/ortools/sat/drat_proof_handler.cc b/ortools/sat/drat_proof_handler.cc index 5c655f40a1..5917e9fe1e 100644 --- a/ortools/sat/drat_proof_handler.cc +++ b/ortools/sat/drat_proof_handler.cc @@ -23,7 +23,6 @@ #if !defined(__PORTABLE_PLATFORM__) #include "ortools/base/file.h" #endif // !defined(__PORTABLE_PLATFORM__) -#include "absl/memory/memory.h" #include "absl/types/span.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/drat_checker.h" @@ -42,7 +41,7 @@ DratProofHandler::DratProofHandler(bool in_binary_format, File* output, : variable_index_(0), drat_writer_(new DratWriter(in_binary_format, output)) { if (check) { - drat_checker_ = absl::make_unique(); + drat_checker_ = std::make_unique(); } } diff --git a/ortools/sat/integer_expr.cc b/ortools/sat/integer_expr.cc index 59a5ff0711..6a5f6c6d10 100644 --- a/ortools/sat/integer_expr.cc +++ b/ortools/sat/integer_expr.cc @@ -21,7 +21,6 @@ #include #include "absl/container/flat_hash_map.h" -#include "absl/memory/memory.h" #include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index 4349ae7518..733c6ce278 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -774,10 +774,15 @@ bool LinearProgrammingConstraint::AddCutFromConstraints( // and if we complement or not before the MIR rounding. Other solvers seems // to try different complementation strategies in a "potprocessing" and we // don't. Try this too. + // + // TODO(user): substitute_only_inner_variables = true is really helpful on + // some instance like "mtest4ma.mps". We should probably have a dedicated + // heuristic depending on the type of cut we do below. + const bool substitute_only_inner_variables = absl::Bernoulli(*random_, 0.5); tmp_ib_slack_infos_.clear(); implied_bounds_processor_.ProcessUpperBoundedConstraintWithSlackCreation( - /*substitute_only_inner_variables=*/false, first_new_var, - expanded_lp_solution_, &cut_, &tmp_ib_slack_infos_); + substitute_only_inner_variables, first_new_var, expanded_lp_solution_, + &cut_, &tmp_ib_slack_infos_); DCHECK(implied_bounds_processor_.DebugSlack(first_new_var, copy_in_debug, cut_, tmp_ib_slack_infos_)); diff --git a/ortools/sat/linear_relaxation.cc b/ortools/sat/linear_relaxation.cc index d64a149f18..a637ea9429 100644 --- a/ortools/sat/linear_relaxation.cc +++ b/ortools/sat/linear_relaxation.cc @@ -679,7 +679,6 @@ void AppendNoOverlapRelaxationAndCutGenerator(const ConstraintProto& ct, energies.push_back(CanonicalizeExpr(e.BuildExpression())); } - // We can now add the relaxation and the cut generators. AddCumulativeRelaxation(helper, demands, /*capacity=*/one, energies, model, relaxation); if (model->GetOrCreate()->linearization_level() > 1) { diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index 2a403b6691..927b742987 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -737,8 +737,9 @@ message SatParameters { [default = false]; // When set, it activates a few scheduling parameters to improve the lower - // bound of scheduling problems. - optional bool use_dual_scheduling_heuristics = 214 [default = false]; + // bound of scheduling problems. This is only effective with multiple workers + // as it modifies the reduced_cost, lb_tree_search, and probing workers. + optional bool use_dual_scheduling_heuristics = 214 [default = true]; // A non-negative level indicating the type of constraints we consider in the // LP relaxation. At level zero, no LP relaxation is used. At level 1, only diff --git a/ortools/sat/scheduling_constraints.cc b/ortools/sat/scheduling_constraints.cc index 57f4ea34a1..be9533b7a7 100644 --- a/ortools/sat/scheduling_constraints.cc +++ b/ortools/sat/scheduling_constraints.cc @@ -209,8 +209,6 @@ bool SelectedMinPropagator::Propagate() { // All propagations and checks belows rely of the presence of the target. if (!assignment.LiteralIsTrue(enforcement_literal_)) return true; - DCHECK_GE(integer_trail_->LowerBound(target_), min_of_mins); - // Note that the case num_possible == 1, num_selected_vars == 0 shouldn't // happen because we assume that the enforcement <=> at_least_one_present // clause has already been propagated. diff --git a/ortools/sat/simplification.cc b/ortools/sat/simplification.cc index c8edbc53dd..180165997f 100644 --- a/ortools/sat/simplification.cc +++ b/ortools/sat/simplification.cc @@ -21,7 +21,6 @@ #include #include -#include "absl/memory/memory.h" #include "absl/types/span.h" #include "ortools/algorithms/dynamic_partition.h" #include "ortools/base/adjustable_priority_queue-inl.h" @@ -1364,7 +1363,7 @@ SatSolver::Status SolveWithPresolve(std::unique_ptr* solver, VLOG(1) << "UNSAT during presolve."; // This is just here to reset the SatSolver::Solve() statistics. - (*solver) = absl::make_unique(); + (*solver) = std::make_unique(); return SatSolver::INFEASIBLE; } @@ -1374,7 +1373,7 @@ SatSolver::Status SolveWithPresolve(std::unique_ptr* solver, } // Load the presolved problem in a new solver. - (*solver) = absl::make_unique(); + (*solver) = std::make_unique(); (*solver)->SetDratProofHandler(drat_proof_handler); (*solver)->SetParameters(parameters); presolver.LoadProblemIntoSatSolver((*solver).get()); diff --git a/ortools/sat/timetable_edgefinding.cc b/ortools/sat/timetable_edgefinding.cc index 56c5c726b3..09f38a6607 100644 --- a/ortools/sat/timetable_edgefinding.cc +++ b/ortools/sat/timetable_edgefinding.cc @@ -50,21 +50,14 @@ void TimeTableEdgeFinding::RegisterWith(GenericLiteralWatcher* watcher) { for (int t = 0; t < num_tasks_; t++) { watcher->WatchLowerBound(demands_[t].var, id); } + watcher->NotifyThatPropagatorMayNotReachFixedPointInOnePass(id); } bool TimeTableEdgeFinding::Propagate() { - while (true) { - const int64_t old_timestamp = integer_trail_->num_enqueues(); - - if (!helper_->SynchronizeAndSetTimeDirection(true)) return false; - if (!TimeTableEdgeFindingPass()) return false; - - if (!helper_->SynchronizeAndSetTimeDirection(false)) return false; - if (!TimeTableEdgeFindingPass()) return false; - - // Stop if no propagation. - if (old_timestamp == integer_trail_->num_enqueues()) break; - } + if (!helper_->SynchronizeAndSetTimeDirection(true)) return false; + if (!TimeTableEdgeFindingPass()) return false; + if (!helper_->SynchronizeAndSetTimeDirection(false)) return false; + if (!TimeTableEdgeFindingPass()) return false; return true; } diff --git a/ortools/sat/var_domination.cc b/ortools/sat/var_domination.cc index feac983cf6..869a6dc7d5 100644 --- a/ortools/sat/var_domination.cc +++ b/ortools/sat/var_domination.cc @@ -23,7 +23,6 @@ #include #include -#include "absl/memory/memory.h" #include "absl/strings/str_cat.h" #include "absl/types/span.h" #include "ortools/algorithms/dynamic_partition.h" @@ -44,7 +43,7 @@ namespace sat { void VarDomination::Reset(int num_variables) { phase_ = 0; num_vars_with_negation_ = 2 * num_variables; - partition_ = absl::make_unique(num_vars_with_negation_); + partition_ = std::make_unique(num_vars_with_negation_); can_freely_decrease_.assign(num_vars_with_negation_, true); @@ -791,11 +790,16 @@ void DetectDominanceRelations( int64_t max_activity = std::numeric_limits::max(); for (int var = 0; var < num_vars; ++var) { + // Ignore variables that have been substitued already or are unused. + if (context.IsFixed(var) || context.VariableWasRemoved(var) || + context.VariableIsNotUsedAnymore(var)) { + dual_bound_strengthening->CannotMove({var}); + var_domination->CanOnlyDominateEachOther({var}); + continue; + } + // Deal with the affine relations that are not part of the proto. // Those only need to be processed in the first pass. - // - // TODO(user): This is not ideal since if only the representative is still - // used, we shouldn't restrict any dominance relation involving it. const AffineRelation::Relation r = context.GetAffineRelation(var); if (r.representative != var) { dual_bound_strengthening->CannotMove({var, r.representative}); @@ -809,13 +813,6 @@ void DetectDominanceRelations( var_domination->CanOnlyDominateEachOther({r.representative}); } } - - // Also ignore variables that have been substitued already or are unused. - if (context.IsFixed(var) || context.VariableWasRemoved(var) || - context.VariableIsNotUsedAnymore(var)) { - dual_bound_strengthening->CannotMove({var}); - var_domination->CanOnlyDominateEachOther({var}); - } } // TODO(user): Benchmark and experiment with 3 phases algo: @@ -984,6 +981,41 @@ void DetectDominanceRelations( << " num_dominance_relations=" << num_dominance_relations; } +namespace { + +bool ProcessAtMostOne(absl::Span literals, + const std::string& message, + const VarDomination& var_domination, + absl::StrongVector* in_constraints, + PresolveContext* context) { + for (const int ref : literals) { + (*in_constraints)[VarDomination::RefToIntegerVariable(ref)] = true; + } + for (const int ref : literals) { + if (context->IsFixed(ref)) continue; + + const auto dominating_ivars = var_domination.DominatingVariables(ref); + if (dominating_ivars.empty()) continue; + for (const IntegerVariable ivar : dominating_ivars) { + if (!(*in_constraints)[ivar]) continue; + if (context->IsFixed(VarDomination::IntegerVariableToRef(ivar))) { + continue; + } + + // We can set the dominated variable to false. + context->UpdateRuleStats(message); + if (!context->SetLiteralToFalse(ref)) return false; + break; + } + } + for (const int ref : literals) { + (*in_constraints)[VarDomination::RefToIntegerVariable(ref)] = false; + } + return true; +} + +} // namespace + bool ExploitDominanceRelations(const VarDomination& var_domination, PresolveContext* context) { const CpModelProto& cp_model = *context->working_model; @@ -1044,34 +1076,21 @@ bool ExploitDominanceRelations(const VarDomination& var_domination, if (!ct.enforcement_literal().empty()) continue; - // TODO(user): Also deal with exactly one. // TODO(user): More generally, combine with probing? if a dominated variable // implies one of its dominant to zero, then it can be set to zero. It seems // adding the implication below should have the same effect? but currently // it requires a lot of presolve rounds. if (ct.constraint_case() == ConstraintProto::kAtMostOne) { - for (const int ref : ct.at_most_one().literals()) { - in_constraints[VarDomination::RefToIntegerVariable(ref)] = true; + if (!ProcessAtMostOne(ct.at_most_one().literals(), + "domination: in at most one", var_domination, + &in_constraints, context)) { + return false; } - for (const int ref : ct.at_most_one().literals()) { - if (context->IsFixed(ref)) continue; - - const auto dominating_ivars = var_domination.DominatingVariables(ref); - if (dominating_ivars.empty()) continue; - for (const IntegerVariable ivar : dominating_ivars) { - if (!in_constraints[ivar]) continue; - if (context->IsFixed(VarDomination::IntegerVariableToRef(ivar))) { - continue; - } - - // We can set the dominated variable to false. - context->UpdateRuleStats("domination: in at most one"); - if (!context->SetLiteralToFalse(ref)) return false; - break; - } - } - for (const int ref : ct.at_most_one().literals()) { - in_constraints[VarDomination::RefToIntegerVariable(ref)] = false; + } else if (ct.constraint_case() == ConstraintProto::kExactlyOne) { + if (!ProcessAtMostOne(ct.exactly_one().literals(), + "domination: in exactly one", var_domination, + &in_constraints, context)) { + return false; } } diff --git a/ortools/sat/var_domination.h b/ortools/sat/var_domination.h index bea6c9ccee..a326f43a29 100644 --- a/ortools/sat/var_domination.h +++ b/ortools/sat/var_domination.h @@ -54,7 +54,7 @@ class VarDomination { VarDomination() {} // This is the translation used from "ref" to IntegerVariable. The API - // understand the cp_mode.proto ref, but internally we only store + // understand the cp_model.proto ref, but internally we only store // IntegerVariable. static IntegerVariable RefToIntegerVariable(int ref) { return RefIsPositive(ref) ? IntegerVariable(2 * ref) @@ -65,7 +65,7 @@ class VarDomination { : NegatedRef(var.value() / 2); } - // Reset the class to a clean state. + // Resets the class to a clean state. // At the beginning, we assume that there is no constraint. void Reset(int num_variables); @@ -111,7 +111,8 @@ class VarDomination { void EndSecondPhase(); // This is true if this variable was never restricted by any call. We can thus - // fix it to its lower bound. + // fix it to its lower bound. Note that we don't do that here as the + // DualBoundStrengthening class will take care of that. bool CanFreelyDecrease(int ref) const; bool CanFreelyDecrease(IntegerVariable var) const;