From 33fd1f910d0a9bb1aa922ff76aa5d502e3e1333f Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 12 May 2022 14:09:18 +0200 Subject: [PATCH] [CP-SAT] better presolve when an at_most_one/exactly_one appears a linear constraint --- ortools/sat/cp_model_presolve.cc | 163 ++++++++++++++++++-------- ortools/sat/cp_model_presolve.h | 6 +- ortools/sat/scheduling_constraints.cc | 2 +- 3 files changed, 117 insertions(+), 54 deletions(-) diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 891cee3fa6..cfbd5cf68b 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -2519,6 +2519,7 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index, } // The other transformations below require a non-reified constraint. + if (ct_index == -1) continue; if (!ct->enforcement_literal().empty()) continue; // Given a variable that only appear in one constraint and in the @@ -2681,6 +2682,16 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index, mapping_linear_ct->mutable_coeffs()->at(i)); return RemoveConstraint(ct); } + + // special case. + if (ct_index == -1) { + if (new_bounds) { + context_->UpdateRuleStats( + "linear: reduced variable domains in derived constraint"); + } + return false; + } + if (new_bounds) { context_->UpdateRuleStats("linear: reduced variable domains"); } @@ -6021,56 +6032,106 @@ bool CpModelPresolver::ProcessSetPPCSubset(int subset_c, int superset_c, return true; } - if (subset_ct->constraint_case() == ConstraintProto::kExactlyOne && + if ((subset_ct->constraint_case() == ConstraintProto::kExactlyOne || + subset_ct->constraint_case() == ConstraintProto::kAtMostOne) && superset_ct->constraint_case() == ConstraintProto::kLinear) { + tmp_set->clear(); + int64_t min_sum = 0; + int64_t max_sum = 0; + if (subset_ct->constraint_case() == ConstraintProto::kExactlyOne) { + min_sum = std::numeric_limits::max(); + max_sum = std::numeric_limits::min(); + tmp_set->insert(subset_ct->exactly_one().literals().begin(), + subset_ct->exactly_one().literals().end()); + } else { + tmp_set->insert(subset_ct->at_most_one().literals().begin(), + subset_ct->at_most_one().literals().end()); + } + + // Compute the min/max on the subset of the sum that correspond the + // exactly_one or at_most_one. + int num_matches = 0; + temp_ct_.Clear(); + Domain reachable(0); + for (int i = 0; i < superset_ct->linear().vars().size(); ++i) { + const int var = superset_ct->linear().vars(i); + const int64_t coeff = superset_ct->linear().coeffs(i); + if (tmp_set->contains(var)) { + ++num_matches; + min_sum = std::min(min_sum, coeff); + max_sum = std::max(max_sum, coeff); + } else { + reachable = + reachable + .AdditionWith( + context_->DomainOf(var).ContinuousMultiplicationBy(coeff)) + .RelaxIfTooComplex(); + temp_ct_.mutable_linear()->add_vars(var); + temp_ct_.mutable_linear()->add_coeffs(coeff); + } + } + + // If a linear constraint contains more than one at_most_one or exactly_one, + // after processing one, we might no longer have an inclusion. + // + // TODO(user): If we have multiple disjoint inclusion, we can propagate + // more. For instance on neos-1593097.mps we basically have a + // weighted_sum_over_at_most_one1 >= weighted_sum_over_at_most_one2. + if (num_matches != tmp_set->size()) return true; + if (subset_ct->constraint_case() == ConstraintProto::kExactlyOne) { + context_->UpdateRuleStats("setppc: exactly_one included in linear"); + } else { + context_->UpdateRuleStats("setppc: at_most_one included in linear"); + } + + reachable = reachable.AdditionWith(Domain(min_sum, max_sum)); + if (reachable.IsIncludedIn(ReadDomainFromProto(superset_ct->linear()))) { + // The constraint is trivial ! + context_->UpdateRuleStats("setppc: removed trivial linear constraint"); + *remove_superset = true; + return true; + } + + // We reuse the normal linear constraint code to propagate domains of + // the other variable using the inclusion information. + if (superset_ct->enforcement_literal().empty()) { + CHECK_GT(num_matches, 0); + FillDomainInProto(ReadDomainFromProto(superset_ct->linear()) + .AdditionWith(Domain(-max_sum, -min_sum)), + temp_ct_.mutable_linear()); + PropagateDomainsInLinear(/*ct_index=*/-1, &temp_ct_); + } + // If we have an exactly one in a linear, we can shift the coefficients of - // all these variables by any constant value. For now, since we only deal - // with positive coefficient, we shift by the min. + // all these variables by any constant value. For now, we only shift by the + // min if it is strictly positive. // // TODO(user): It might be more interesting to maximize the number of terms // that are shifted to zero to reduce the constraint size. - tmp_set->clear(); - tmp_set->insert(subset_ct->exactly_one().literals().begin(), - subset_ct->exactly_one().literals().end()); - int64_t min_coeff = std::numeric_limits::max(); - int num_matches = 0; - for (int i = 0; i < superset_ct->linear().vars().size(); ++i) { - const int var = superset_ct->linear().vars(i); - if (tmp_set->contains(var)) { - ++num_matches; - min_coeff = - std::min(min_coeff, std::abs(superset_ct->linear().coeffs(i))); + if (subset_ct->constraint_case() == ConstraintProto::kExactlyOne && + min_sum > 0) { + int new_size = 0; + for (int i = 0; i < superset_ct->linear().vars().size(); ++i) { + const int var = superset_ct->linear().vars(i); + int64_t coeff = superset_ct->linear().coeffs(i); + if (tmp_set->contains(var)) { + if (coeff == min_sum) continue; // delete term. + coeff -= min_sum; + } + superset_ct->mutable_linear()->set_vars(new_size, var); + superset_ct->mutable_linear()->set_coeffs(new_size, coeff); + ++new_size; } + + superset_ct->mutable_linear()->mutable_vars()->Truncate(new_size); + superset_ct->mutable_linear()->mutable_coeffs()->Truncate(new_size); + FillDomainInProto(ReadDomainFromProto(superset_ct->linear()) + .AdditionWith(Domain(-min_sum)), + superset_ct->mutable_linear()); + context_->UpdateConstraintVariableUsage(superset_c); + context_->UpdateRuleStats("setppc: reduced linear coefficients."); } - // If a linear constraint contains more than one at most one, after - // processing one, we might no longer have an inclusion. - if (num_matches != tmp_set->size()) return true; - - // TODO(user): It would be cool to propagate other variable domains with - // the knowledge that the partial sum in is [min_coeff, max_coeff]. I am - // a bit relunctant to duplicate the code for that here. - int new_size = 0; - for (int i = 0; i < superset_ct->linear().vars().size(); ++i) { - const int var = superset_ct->linear().vars(i); - int64_t coeff = superset_ct->linear().coeffs(i); - if (tmp_set->contains(var)) { - CHECK_GE(coeff, 0); - if (coeff == min_coeff) continue; // delete term. - coeff -= min_coeff; - } - superset_ct->mutable_linear()->set_vars(new_size, var); - superset_ct->mutable_linear()->set_coeffs(new_size, coeff); - ++new_size; - } - - superset_ct->mutable_linear()->mutable_vars()->Truncate(new_size); - superset_ct->mutable_linear()->mutable_coeffs()->Truncate(new_size); - FillDomainInProto(ReadDomainFromProto(superset_ct->linear()) - .AdditionWith(Domain(-min_coeff)), - superset_ct->mutable_linear()); - context_->UpdateConstraintVariableUsage(superset_c); - context_->UpdateRuleStats("setppc: reduced linear coefficients."); return true; } @@ -6138,24 +6199,22 @@ void CpModelPresolver::ProcessSetPPC() { const int size = ct->linear().vars().size(); if (size <= 2) continue; - // TODO(user): We only deal with every literal having a positive coeff - // here. We should probably do the same with all negative. We can also - // consider NegatedRef(var). + // TODO(user): We only deal with positive var here. Ideally we should + // match the VARIABLES of the at_most_one/exactly_one with the VARIABLES + // of the linear, and complement all variable to have a literal inclusion. temp_literals.clear(); for (int i = 0; i < size; ++i) { const int var = ct->linear().vars(i); - const int64_t coeff = ct->linear().coeffs(i); if (!context_->CanBeUsedAsLiteral(var)) continue; if (!RefIsPositive(var)) continue; - if (coeff < 0) continue; temp_literals.push_back( Literal(BooleanVariable(var), true).Index().value()); } - if (temp_literals.size() <= 2) continue; - - // Note that we only care about the linear being the superset. - relevant_constraints.push_back(c); - detector.AddPotentialSuperset(storage.Add(temp_literals)); + if (temp_literals.size() > 2) { + // Note that we only care about the linear being the superset. + relevant_constraints.push_back(c); + detector.AddPotentialSuperset(storage.Add(temp_literals)); + } } } diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index e6fd7cd341..d43dd8ce08 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -147,7 +147,7 @@ class CpModelPresolver { // For the linear constraints, we have more than one function. bool CanonicalizeLinear(ConstraintProto* ct); - bool PropagateDomainsInLinear(int c, ConstraintProto* ct); + bool PropagateDomainsInLinear(int ct_index, ConstraintProto* ct); bool RemoveSingletonInLinear(ConstraintProto* ct); bool PresolveSmallLinear(ConstraintProto* ct); bool PresolveLinearOfSizeOne(ConstraintProto* ct); @@ -258,6 +258,10 @@ class CpModelPresolver { // Used by CanonicalizeLinearExpressionInternal(). std::vector> tmp_terms_; + + // Used by ProcessSetPPCSubset() to propagate linear with an at_most_one or + // exactly_one included inside. + ConstraintProto temp_ct_; }; // This helper class perform copy with simplification from a model and a diff --git a/ortools/sat/scheduling_constraints.cc b/ortools/sat/scheduling_constraints.cc index be9533b7a7..102f64775a 100644 --- a/ortools/sat/scheduling_constraints.cc +++ b/ortools/sat/scheduling_constraints.cc @@ -206,7 +206,7 @@ bool SelectedMinPropagator::Propagate() { } } - // All propagations and checks belows rely of the presence of the target. + // All propagations and checks belows rely on the presence of the target. if (!assignment.LiteralIsTrue(enforcement_literal_)) return true; // Note that the case num_possible == 1, num_selected_vars == 0 shouldn't