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

improve presolve for CP-SAT

Browse Source
This commit is contained in:
Laurent Perron
2019-12-09 17:57:13 +01:00
parent 34231dbbc3
commit b43d41b227
8 changed files with 85 additions and 41 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
ortools/sat/cp_model_presolve.cc
View File

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

4
ortools/sat/cp_model_search.cc
View File

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

8
ortools/sat/linear_constraint_manager.cc
View File

@@ -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
<< "'.";
}
}
}

78
ortools/sat/presolve_context.cc
View File

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

14
ortools/sat/presolve_context.h
View File

@@ -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<std::pair<int, int64>, absl::flat_hash_set<int>>
absl::flat_hash_map<std::pair<int, int64>,
absl::flat_hash_map<int, ConstraintProto*>>
eq_half_encoding;
absl::flat_hash_map<std::pair<int, int64>, absl::flat_hash_set<int>>
absl::flat_hash_map<std::pair<int, int64>,
absl::flat_hash_map<int, ConstraintProto*>>
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;

12
ortools/sat/presolve_util.cc
View File

@@ -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<std::pair<int, Domain>> 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<std::pair<int, Domain>> 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.

2
ortools/sat/presolve_util.h
View File

@@ -76,7 +76,7 @@ class DomainDeductions {
return Index(ref >= 0 ? 2 * ref : -2 * ref - 1);
}
std::vector<int> tmp_num_occurences_;
std::vector<int> tmp_num_occurrences_;
SparseBitset<Index> something_changed_;
gtl::ITIVector<Index, std::vector<int>> enforcement_to_vars_;

2
ortools/sat/sat_parameters.proto
View File

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