always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[CP-SAT] improve cuts diversity; fix infinite loop in the ttef constraint; improve var domination; remove wrong DCHECK

Browse Source
This commit is contained in:
Laurent Perron
2022-05-11 17:23:59 +02:00
parent 71336d84b8
commit ba15d312ba
15 changed files with 123 additions and 118 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
ortools/sat/BUILD.bazel
View File

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

3
ortools/sat/cp_model_loader.cc
View File

@@ -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<SparsePermutation>(num_literals);
std::make_unique<SparsePermutation>(num_literals);
int support_index = 0;
const int num_cycle = perm.cycle_sizes().size();
for (int i = 0; i < num_cycle; ++i) {

93
ortools/sat/cp_model_solver.cc
View File

@@ -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<DratProofHandler>(
drat_proof_handler = std::make_unique<DratProofHandler>(
/*in_binary_format=*/false, output, absl::GetFlag(FLAGS_drat_check));
} else {
drat_proof_handler = absl::make_unique<DratProofHandler>();
drat_proof_handler = std::make_unique<DratProofHandler>();
}
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<Model>(name)) {
local_model_(std::make_unique<Model>(name)) {
// Setup the local model parameters and time limit.
*(local_model_->GetOrCreate<SatParameters>()) = 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<Model>(name_)) {
local_model_(std::make_unique<Model>(name_)) {
// Setup the local model parameters and time limit.
*(local_model_->GetOrCreate<SatParameters>()) = 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<PresolveContext>(
auto context = std::make_unique<PresolveContext>(
&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<SharedBoundsManager> shared_bounds_manager;
if (params.share_level_zero_bounds()) {
shared_bounds_manager = absl::make_unique<SharedBoundsManager>(model_proto);
shared_bounds_manager = std::make_unique<SharedBoundsManager>(model_proto);
}
std::unique_ptr<SharedRelaxationSolutionRepository>
shared_relaxation_solutions;
if (params.use_relaxation_lns()) {
shared_relaxation_solutions =
absl::make_unique<SharedRelaxationSolutionRepository>(
std::make_unique<SharedRelaxationSolutionRepository>(
/*num_solutions_to_keep=*/10);
global_model->Register<SharedRelaxationSolutionRepository>(
shared_relaxation_solutions.get());
}
auto shared_lp_solutions = absl::make_unique<SharedLPSolutionRepository>(
auto shared_lp_solutions = std::make_unique<SharedLPSolutionRepository>(
/*num_solutions_to_keep=*/10);
global_model->Register<SharedLPSolutionRepository>(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<SharedIncompleteSolutionManager>();
std::make_unique<SharedIncompleteSolutionManager>();
global_model->Register<SharedIncompleteSolutionManager>(
shared_incomplete_solutions.get());
}
std::unique_ptr<SharedClausesManager> shared_clauses;
if (params.share_binary_clauses()) {
shared_clauses = absl::make_unique<SharedClausesManager>();
shared_clauses = std::make_unique<SharedClausesManager>();
}
SharedClasses shared;
@@ -2810,7 +2809,7 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
std::vector<std::unique_ptr<SubSolver>> subsolvers;
// Add a synchronization point for the shared classes.
subsolvers.push_back(absl::make_unique<SynchronizationPoint>([&shared]() {
subsolvers.push_back(std::make_unique<SynchronizationPoint>([&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<FullProblemSolver>(
subsolvers.push_back(std::make_unique<FullProblemSolver>(
"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<FullProblemSolver>(
subsolvers.push_back(std::make_unique<FullProblemSolver>(
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<FeasibilityPumpSolver>(params, &shared));
std::make_unique<FeasibilityPumpSolver>(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<NeighborhoodGeneratorHelper>(
auto unique_helper = std::make_unique<NeighborhoodGeneratorHelper>(
&model_proto, &params, 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<LnsSolver>(
absl::make_unique<RelaxRandomVariablesGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RelaxRandomVariablesGenerator>(
helper, absl::StrCat("rnd_var_lns_", local_params.name())),
local_params, helper, &shared));
subsolvers.push_back(absl::make_unique<LnsSolver>(
absl::make_unique<RelaxRandomConstraintsGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RelaxRandomConstraintsGenerator>(
helper, absl::StrCat("rnd_cst_lns_", local_params.name())),
local_params, helper, &shared));
subsolvers.push_back(absl::make_unique<LnsSolver>(
absl::make_unique<VariableGraphNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<VariableGraphNeighborhoodGenerator>(
helper, absl::StrCat("graph_var_lns_", local_params.name())),
local_params, helper, &shared));
subsolvers.push_back(absl::make_unique<LnsSolver>(
absl::make_unique<ConstraintGraphNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<ConstraintGraphNeighborhoodGenerator>(
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<LnsSolver>(
absl::make_unique<SchedulingTimeWindowNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<SchedulingTimeWindowNeighborhoodGenerator>(
helper, absl::StrCat("scheduling_time_window_lns_",
local_params.name())),
local_params, helper, &shared));
subsolvers.push_back(absl::make_unique<LnsSolver>(
absl::make_unique<SchedulingNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<SchedulingNeighborhoodGenerator>(
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<std::vector<int>> intervals_in_constraints =
helper->GetUniqueIntervalSets();
if (intervals_in_constraints.size() > 2) {
subsolvers.push_back(absl::make_unique<LnsSolver>(
absl::make_unique<SchedulingResourceWindowsNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<SchedulingResourceWindowsNeighborhoodGenerator>(
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<LnsSolver>(
absl::make_unique<RoutingRandomNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RoutingRandomNeighborhoodGenerator>(
helper, absl::StrCat("routing_random_lns_", local_params.name())),
local_params, helper, &shared));
subsolvers.push_back(absl::make_unique<LnsSolver>(
absl::make_unique<RoutingPathNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RoutingPathNeighborhoodGenerator>(
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<LnsSolver>(
absl::make_unique<RoutingFullPathNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RoutingFullPathNeighborhoodGenerator>(
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<LnsSolver>(
absl::make_unique<RelaxationInducedNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RelaxationInducedNeighborhoodGenerator>(
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<LnsSolver>(
absl::make_unique<RelaxationInducedNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<RelaxationInducedNeighborhoodGenerator>(
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<LnsSolver>(
absl::make_unique<
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<
ConsecutiveConstraintsRelaxationNeighborhoodGenerator>(
helper, absl::StrCat("rnd_rel_lns_", local_params.name())),
local_params, helper, &shared));
subsolvers.push_back(absl::make_unique<LnsSolver>(
absl::make_unique<WeightedRandomRelaxationNeighborhoodGenerator>(
subsolvers.push_back(std::make_unique<LnsSolver>(
std::make_unique<WeightedRandomRelaxationNeighborhoodGenerator>(
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<SynchronizationPoint>(
subsolvers.push_back(std::make_unique<SynchronizationPoint>(
[&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<PresolveContext>(model, &new_cp_model_proto,
&mapping_proto);
auto context = std::make_unique<PresolveContext>(model, &new_cp_model_proto,
&mapping_proto);
if (!ImportModelWithBasicPresolveIntoContext(model_proto, context.get())) {
VLOG(1) << "Model found infeasible during copy";

3
ortools/sat/cp_model_symmetries.cc
View File

@@ -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<Graph> GenerateGraphForSymmetryDetection(
CHECK(initial_equivalence_classes != nullptr);
const int num_variables = problem.variables_size();
auto graph = absl::make_unique<Graph>();
auto graph = std::make_unique<Graph>();
// 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

1
ortools/sat/cuts.cc
View File

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

3
ortools/sat/drat_proof_handler.cc
View File

@@ -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<DratChecker>();
drat_checker_ = std::make_unique<DratChecker>();
}
}

1
ortools/sat/integer_expr.cc
View File

@@ -21,7 +21,6 @@
#include <vector>
#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"

9
ortools/sat/linear_programming_constraint.cc
View File

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

1
ortools/sat/linear_relaxation.cc
View File

@@ -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<SatParameters>()->linearization_level() > 1) {

5
ortools/sat/sat_parameters.proto
View File

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

2
ortools/sat/scheduling_constraints.cc
View File

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

5
ortools/sat/simplification.cc
View File

@@ -21,7 +21,6 @@
#include <utility>
#include <vector>
#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<SatSolver>* solver,
VLOG(1) << "UNSAT during presolve.";
// This is just here to reset the SatSolver::Solve() statistics.
(*solver) = absl::make_unique<SatSolver>();
(*solver) = std::make_unique<SatSolver>();
return SatSolver::INFEASIBLE;
}
@@ -1374,7 +1373,7 @@ SatSolver::Status SolveWithPresolve(std::unique_ptr<SatSolver>* solver,
}
// Load the presolved problem in a new solver.
(*solver) = absl::make_unique<SatSolver>();
(*solver) = std::make_unique<SatSolver>();
(*solver)->SetDratProofHandler(drat_proof_handler);
(*solver)->SetParameters(parameters);
presolver.LoadProblemIntoSatSolver((*solver).get());

17
ortools/sat/timetable_edgefinding.cc
View File

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

87
ortools/sat/var_domination.cc
View File

@@ -23,7 +23,6 @@
#include <string>
#include <vector>
#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<DynamicPartition>(num_vars_with_negation_);
partition_ = std::make_unique<DynamicPartition>(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<int64_t>::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<const int> literals,
const std::string& message,
const VarDomination& var_domination,
absl::StrongVector<IntegerVariable, bool>* 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;
}
}

7
ortools/sat/var_domination.h
View File

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