From b43d41b22755d6dab4221c30f216efb767d6dccd Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 9 Dec 2019 17:57:13 +0100 Subject: [PATCH] improve presolve for CP-SAT --- ortools/sat/cp_model_presolve.cc | 6 +- ortools/sat/cp_model_search.cc | 4 -- ortools/sat/linear_constraint_manager.cc | 8 ++- ortools/sat/presolve_context.cc | 78 ++++++++++++++++++------ ortools/sat/presolve_context.h | 14 +++-- ortools/sat/presolve_util.cc | 12 ++-- ortools/sat/presolve_util.h | 2 +- ortools/sat/sat_parameters.proto | 2 +- 8 files changed, 85 insertions(+), 41 deletions(-) diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 84549e827f..e37529fc90 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -211,7 +211,7 @@ bool CpModelPresolver::PresolveBoolOr(ConstraintProto* ct) { return RemoveConstraint(ct); } // We can just set the variable to true in this case since it is not - // used in any other constraint (note that we artifically bump the + // used in any other constraint (note that we artificially bump the // objective var usage by 1). if (context_->VariableIsUniqueAndRemovable(literal)) { context_->UpdateRuleStats("bool_or: singleton"); @@ -1100,7 +1100,7 @@ bool CpModelPresolver::PresolveSmallLinear(ConstraintProto* ct) { if (linear.domain_size() == 2 && linear.domain(0) == linear.domain(1)) { const int64 value = RefIsPositive(ref) ? linear.domain(0) * coeff : -linear.domain(0) * coeff; - if (context_->StoreLiteralImpliesVarEqValue(literal, var, value)) { + if (context_->StoreLiteralImpliesVarEqValue(literal, var, value, ct)) { // The domain is not actually modified, but we want to rescan the // constraints linked to this variable. See TODO below. context_->modified_domains.Set(var); @@ -1111,7 +1111,7 @@ bool CpModelPresolver::PresolveSmallLinear(ConstraintProto* ct) { if (complement.Size() != 1) return false; const int64 value = RefIsPositive(ref) ? complement.Min() * coeff : -complement.Min() * coeff; - if (context_->StoreLiteralImpliesVarNEqValue(literal, var, value)) { + if (context_->StoreLiteralImpliesVarNEqValue(literal, var, value, ct)) { // The domain is not actually modified, but we want to rescan the // constraints linked to this variable. See TODO below. context_->modified_domains.Set(var); diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 51f32aa49a..b4403161fb 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -342,7 +342,6 @@ SatParameters DiversifySearchParameters(const SatParameters& params, if (--index == 0) { // Reinforce LP relaxation. new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH); new_params.set_linearization_level(2); - new_params.set_add_cg_cuts(true); new_params.set_use_branching_in_lp(true); *name = "max_lp"; return new_params; @@ -389,7 +388,6 @@ SatParameters DiversifySearchParameters(const SatParameters& params, if (--index == 0) { // Reinforce LP relaxation. new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH); new_params.set_linearization_level(2); - new_params.set_add_cg_cuts(true); *name = "max_lp"; return new_params; } @@ -442,7 +440,6 @@ SatParameters DiversifySearchParameters(const SatParameters& params, if (--index == 0) { // Reinforce LP relaxation. new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH); new_params.set_linearization_level(2); - new_params.set_add_cg_cuts(true); new_params.set_use_branching_in_lp(true); *name = "max_lp"; return new_params; @@ -509,7 +506,6 @@ SatParameters DiversifySearchParameters(const SatParameters& params, if (--index == 0) { // Reinforce LP relaxation. new_params.set_search_branching(SatParameters::AUTOMATIC_SEARCH); new_params.set_linearization_level(2); - new_params.set_add_cg_cuts(true); *name = "max_lp"; return new_params; } diff --git a/ortools/sat/linear_constraint_manager.cc b/ortools/sat/linear_constraint_manager.cc index ada7f8e752..4f4149ae98 100644 --- a/ortools/sat/linear_constraint_manager.cc +++ b/ortools/sat/linear_constraint_manager.cc @@ -76,9 +76,11 @@ LinearConstraintManager::~LinearConstraintManager() { if (num_coeff_strenghtening_ > 0) { VLOG(2) << "num_coeff_strenghtening: " << num_coeff_strenghtening_; } - for (const auto entry : type_to_num_cuts_) { - VLOG(1) << "Added " << entry.second << " cuts of type '" << entry.first - << "'."; + if (sat_parameters_.log_search_progress()) { + for (const auto entry : type_to_num_cuts_) { + LOG(INFO) << "Added " << entry.second << " cuts of type '" << entry.first + << "'."; + } } } diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 3fcb27b7ad..1e77fd2752 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -47,7 +47,6 @@ void PresolveContext::AddImplication(int a, int b) { ConstraintProto* const ct = working_model->add_constraints(); ct->add_enforcement_literal(a); ct->mutable_bool_and()->add_literals(b); - UpdateNewConstraintsVariableUsage(); } // b => x in [lb, ub]. @@ -61,7 +60,6 @@ void PresolveContext::AddImplyInDomain(int b, int x, const Domain& domain) { mutable_linear->mutable_vars()->Resize(1, x); mutable_linear->mutable_coeffs()->Resize(1, 1); FillDomainInProto(domain, mutable_linear); - UpdateNewConstraintsVariableUsage(); } bool PresolveContext::DomainIsEmpty(int ref) const { @@ -293,9 +291,6 @@ void PresolveContext::StoreAffineRelation(const ConstraintProto& ct, int ref_x, } } -// TODO(user): When merging literals, experiments shows that adding 2 -// implications leads to less Boolean variables on the created model. -// To investigate. void PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) { if (ref_a == ref_b) return; if (ref_a == NegatedRef(ref_b)) { @@ -303,6 +298,33 @@ void PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) { return; } + if (IsFixed(ref_a)) { + const bool val_a = LiteralIsTrue(ref_a); + if (IsFixed(ref_b)) { + const bool val_b = LiteralIsTrue(ref_b); + if (val_a != val_b) { + CHECK(!NotifyThatModelIsUnsat()); + } + } else { + UpdateRuleStats("variables: propagate equivalent fixed literal"); + if (val_a) { + CHECK(SetLiteralToTrue(ref_b)); + } else { + CHECK(SetLiteralToFalse(ref_b)); + } + } + return; + } else if (IsFixed(ref_b)) { + const bool val_b = LiteralIsTrue(ref_b); + UpdateRuleStats("variables: propagate equivalent fixed literal"); + if (val_b) { + CHECK(SetLiteralToTrue(ref_a)); + } else { + CHECK(SetLiteralToFalse(ref_a)); + } + return; + } + // For now, we do need to add the relation ref_a == ref_b so we have a // proper variable usage count and propagation between ref_a and ref_b. // @@ -383,8 +405,8 @@ void PresolveContext::InsertVarValueEncoding(int literal, int ref, // Other value in the domain was already encoded. const int previous_other_literal = other_it->second; if (previous_other_literal != NegatedRef(literal)) { - AddImplication(literal, NegatedRef(previous_other_literal)); - AddImplication(NegatedRef(previous_other_literal), literal); + StoreBooleanEqualityRelation(literal, + NegatedRef(previous_other_literal)); } } else { encoding[other_key] = NegatedRef(literal); @@ -409,14 +431,14 @@ void PresolveContext::InsertVarValueEncoding(int literal, int ref, } else { const int previous_literal = insert.first->second; if (literal != previous_literal) { - AddImplication(literal, previous_literal); - AddImplication(previous_literal, literal); + StoreBooleanEqualityRelation(literal, previous_literal); } } } bool PresolveContext::InsertHalfVarValueEncoding(int literal, int var, - int64 value, bool imply_eq) { + int64 value, bool imply_eq, + ConstraintProto* ct) { CHECK(RefIsPositive(var)); // Creates the linking maps on demand. @@ -425,13 +447,13 @@ bool PresolveContext::InsertHalfVarValueEncoding(int literal, int var, auto& other_map = imply_eq ? neq_half_encoding[key] : eq_half_encoding[key]; // Insert the reference literal in the half encoding map. - const auto& new_info = direct_map.insert(literal); + const auto& new_info = direct_map.insert(std::make_pair(literal, ct)); if (new_info.second) { VLOG(2) << "Collect lit(" << literal << ") implies var(" << var << (imply_eq ? ") == " : ") != ") << value; UpdateRuleStats("variables: detect half reified value encoding"); - if (other_map.contains(NegatedRef(literal))) { + if (gtl::ContainsKey(other_map, NegatedRef(literal))) { const int ref_lit = imply_eq ? literal : NegatedRef(literal); const auto insert_encoding_status = encoding.insert(std::make_pair(std::make_pair(var, value), ref_lit)); @@ -443,8 +465,25 @@ bool PresolveContext::InsertHalfVarValueEncoding(int literal, int var, const int previous_lit = insert_encoding_status.first->second; VLOG(2) << "Detect duplicate encoding lit(" << ref_lit << ") == lit(" << previous_lit << ") <=> var(" << var << ") == " << value; - AddImplication(previous_lit, ref_lit); - AddImplication(ref_lit, previous_lit); + StoreBooleanEqualityRelation(previous_lit, ref_lit); + + const AffineRelation::Relation r = GetAffineRelation(previous_lit); + if (r.representative != previous_lit) { + const int new_ref_lit = + r.coeff > 0 ? r.representative : NegatedRef(r.representative); + VLOG(2) + << "Different representative of previous literal, updating to " + << new_ref_lit; + encoding[key] = new_ref_lit; + } + + // Remove the two half encoding constraints from the model. + VLOG(2) << "Delete " << ct->DebugString(); + ct->Clear(); + direct_map.erase(literal); + VLOG(2) << "Delete " << other_map[NegatedRef(literal)]->DebugString(); + other_map[NegatedRef(literal)]->Clear(); + other_map.erase(NegatedRef(literal)); UpdateRuleStats( "variables: merge equivalent var value encoding literals"); } @@ -455,13 +494,16 @@ bool PresolveContext::InsertHalfVarValueEncoding(int literal, int var, } bool PresolveContext::StoreLiteralImpliesVarEqValue(int literal, int var, - int64 value) { - return InsertHalfVarValueEncoding(literal, var, value, /*imply_eq=*/true); + int64 value, + ConstraintProto* ct) { + return InsertHalfVarValueEncoding(literal, var, value, /*imply_eq=*/true, ct); } bool PresolveContext::StoreLiteralImpliesVarNEqValue(int literal, int var, - int64 value) { - return InsertHalfVarValueEncoding(literal, var, value, /*imply_eq=*/false); + int64 value, + ConstraintProto* ct) { + return InsertHalfVarValueEncoding(literal, var, value, /*imply_eq=*/false, + ct); } int PresolveContext::GetOrCreateVarValueEncoding(int ref, int64 value) { diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 73c4be4495..847adc2065 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -143,11 +143,13 @@ struct PresolveContext { // Stores the fact that literal implies var == value. // It returns true if that information is new. - bool StoreLiteralImpliesVarEqValue(int literal, int var, int64 value); + bool StoreLiteralImpliesVarEqValue(int literal, int var, int64 value, + ConstraintProto* ct); // Stores the fact that literal implies var != value. // It returns true if that information is new. - bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64 value); + bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64 value, + ConstraintProto* ct); // Objective handling functions. We load it at the beginning so that during // presolve we can work on the more efficient hash_map representation. @@ -217,9 +219,11 @@ struct PresolveContext { // i.e.: literal => var ==/!= value // The state is accumulated (adding x => var == value then !x => var != value) // will deduce that x equivalent to var == value. - absl::flat_hash_map, absl::flat_hash_set> + absl::flat_hash_map, + absl::flat_hash_map> eq_half_encoding; - absl::flat_hash_map, absl::flat_hash_set> + absl::flat_hash_map, + absl::flat_hash_map> neq_half_encoding; // Variable <-> constraint graph. @@ -292,7 +296,7 @@ struct PresolveContext { // InsertHalfVarValueEncoding(literal, var, value, true); // InsertHalfVarValueEncoding(NegatedRef(literal), var, value, false); bool InsertHalfVarValueEncoding(int literal, int var, int64 value, - bool imply_eq); + bool imply_eq, ConstraintProto* ct); // Initially false, and set to true on the first inconsistency. bool is_unsat = false; diff --git a/ortools/sat/presolve_util.cc b/ortools/sat/presolve_util.cc index 4c1069036f..3be0bd6c69 100644 --- a/ortools/sat/presolve_util.cc +++ b/ortools/sat/presolve_util.cc @@ -26,8 +26,8 @@ void DomainDeductions::AddDeduction(int literal_ref, int var, Domain domain) { something_changed_.Resize(index + 1); enforcement_to_vars_.resize(index.value() + 1); } - if (var >= tmp_num_occurences_.size()) { - tmp_num_occurences_.resize(var + 1, 0); + if (var >= tmp_num_occurrences_.size()) { + tmp_num_occurrences_.resize(var + 1, 0); } const auto insert = deductions_.insert({{index, var}, domain}); if (insert.second) { @@ -65,11 +65,11 @@ std::vector> DomainDeductions::ProcessClause( for (const int ref : clause) { const Index index = IndexFromLiteral(ref); for (const int var : enforcement_to_vars_[index]) { - if (tmp_num_occurences_[var] == 0) { + if (tmp_num_occurrences_[var] == 0) { to_clean.push_back(var); } - tmp_num_occurences_[var]++; - if (tmp_num_occurences_[var] == clause.size()) { + tmp_num_occurrences_[var]++; + if (tmp_num_occurrences_[var] == clause.size()) { to_process.push_back(var); } } @@ -77,7 +77,7 @@ std::vector> DomainDeductions::ProcessClause( // Clear the counts. for (const int var : to_clean) { - tmp_num_occurences_[var] = 0; + tmp_num_occurrences_[var] = 0; } // Compute the domain unions. diff --git a/ortools/sat/presolve_util.h b/ortools/sat/presolve_util.h index 6f9d139a5a..7f0d5c4573 100644 --- a/ortools/sat/presolve_util.h +++ b/ortools/sat/presolve_util.h @@ -76,7 +76,7 @@ class DomainDeductions { return Index(ref >= 0 ? 2 * ref : -2 * ref - 1); } - std::vector tmp_num_occurences_; + std::vector tmp_num_occurrences_; SparseBitset something_changed_; gtl::ITIVector> enforcement_to_vars_; diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index eebafd43e6..86dfc3660d 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -554,7 +554,7 @@ message SatParameters { // Whether we generate and add Chvatal-Gomory cuts to the LP at root node. // Note that for now, this is not heavily tunned. - optional bool add_cg_cuts = 117 [default = false]; + optional bool add_cg_cuts = 117 [default = true]; // Whether we generate MIR cuts at root node. // Note that for now, this is not heavily tunned.