From f3f9bc44a2b297935901c9f5e5d461e0a79b0bcd Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Tue, 26 Mar 2024 12:35:12 +0100 Subject: [PATCH] [CP-SAT] improve diffn and linear loading --- ortools/sat/cp_model_loader.cc | 54 +++---- ortools/sat/diffn.cc | 2 +- ortools/sat/integer.h | 2 +- ortools/sat/integer_expr.h | 280 +++++++++++---------------------- ortools/sat/precedences.h | 46 ++---- 5 files changed, 130 insertions(+), 254 deletions(-) diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 09c9b13d7b..afeb1caa85 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -1384,39 +1384,27 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { } if (ct.linear().domain_size() == 2) { - int64_t lb = ct.linear().domain(0); - int64_t ub = ct.linear().domain(1); - if (min_sum >= lb) lb = std::numeric_limits::min(); - if (max_sum <= ub) ub = std::numeric_limits::max(); - - if (!HasEnforcementLiteral(ct)) { - if (all_booleans) { - // TODO(user): we should probably also implement an - // half-reified version of this constraint. - std::vector cst; - for (int i = 0; i < vars.size(); ++i) { - const int ref = ct.linear().vars(i); - cst.push_back({mapping->Literal(ref), coeffs[i]}); - } - m->Add(BooleanLinearConstraint(lb, ub, &cst)); - } else { - if (lb != std::numeric_limits::min()) { - m->Add(WeightedSumGreaterOrEqual(vars, coeffs, lb)); - } - if (ub != std::numeric_limits::max()) { - m->Add(WeightedSumLowerOrEqual(vars, coeffs, ub)); - } + const int64_t lb = ct.linear().domain(0); + const int64_t ub = ct.linear().domain(1); + const std::vector enforcement_literals = + mapping->Literals(ct.enforcement_literal()); + if (all_booleans && enforcement_literals.empty()) { + // TODO(user): we should probably also implement an + // half-reified version of this constraint. + std::vector cst; + for (int i = 0; i < vars.size(); ++i) { + const int ref = ct.linear().vars(i); + cst.push_back({mapping->Literal(ref), coeffs[i]}); } + m->GetOrCreate()->AddLinearConstraint( + /*use_lower_bound=*/(min_sum < lb), lb, + /*use_upper_bound=*/(max_sum > ub), ub, &cst); } else { - const std::vector enforcement_literals = - mapping->Literals(ct.enforcement_literal()); - if (lb != std::numeric_limits::min()) { - m->Add(ConditionalWeightedSumGreaterOrEqual(enforcement_literals, vars, - coeffs, lb)); + if (min_sum < lb) { + AddWeightedSumGreaterOrEqual(enforcement_literals, vars, coeffs, lb, m); } - if (ub != std::numeric_limits::max()) { - m->Add(ConditionalWeightedSumLowerOrEqual(enforcement_literals, vars, - coeffs, ub)); + if (max_sum > ub) { + AddWeightedSumLowerOrEqual(enforcement_literals, vars, coeffs, ub, m); } } return; @@ -1463,12 +1451,10 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) { for_enumeration.push_back(subdomain_literal); if (min_sum < lb) { - m->Add(ConditionalWeightedSumGreaterOrEqual({subdomain_literal}, vars, - coeffs, lb)); + AddWeightedSumGreaterOrEqual({subdomain_literal}, vars, coeffs, lb, m); } if (max_sum > ub) { - m->Add(ConditionalWeightedSumLowerOrEqual({subdomain_literal}, vars, - coeffs, ub)); + AddWeightedSumLowerOrEqual({subdomain_literal}, vars, coeffs, ub, m); } } diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index 2ffc5028da..cd2d84b735 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -428,7 +428,7 @@ NonOverlappingRectanglesEnergyPropagator::FindConflict( .use_pairwise = true, .use_dff_f0 = true, .use_dff_f2 = true, - .brute_force_threshold = 6, + .brute_force_threshold = 7, .dff2_max_number_of_parameters_to_check = 100}); if (opp_result.GetResult() == OrthogonalPackingResult::Status::INFEASIBLE && (best_conflict.opp_result.GetResult() != diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 42f0968268..b1856dc3ad 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -1912,7 +1912,7 @@ inline std::function Equality(IntegerVariable v, int64_t value) { // is the same as using different underlying variable for an integer literal and // its negation. inline std::function Implication( - const std::vector& enforcement_literals, IntegerLiteral i) { + absl::Span enforcement_literals, IntegerLiteral i) { return [=](Model* model) { IntegerTrail* integer_trail = model->GetOrCreate(); if (i.bound <= integer_trail->LowerBound(i.var)) { diff --git a/ortools/sat/integer_expr.h b/ortools/sat/integer_expr.h index 2c9e099dea..2c4289857a 100644 --- a/ortools/sat/integer_expr.h +++ b/ortools/sat/integer_expr.h @@ -417,65 +417,9 @@ template inline std::function WeightedSumLowerOrEqual( const std::vector& vars, const VectorInt& coefficients, int64_t upper_bound) { - // Special cases. - CHECK_GE(vars.size(), 1); - if (vars.size() == 1) { - const int64_t c = coefficients[0]; - CHECK_NE(c, 0); - if (c > 0) { - return LowerOrEqual( - vars[0], - FloorRatio(IntegerValue(upper_bound), IntegerValue(c)).value()); - } else { - return GreaterOrEqual( - vars[0], - CeilRatio(IntegerValue(-upper_bound), IntegerValue(-c)).value()); - } - } - return [=](Model* model) { - const SatParameters& params = *model->GetOrCreate(); - if (!params.new_linear_propagation()) { - if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) && - (coefficients[1] == 1 || coefficients[1] == -1)) { - return Sum2LowerOrEqual( - coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]), - coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), - upper_bound)(model); - } - if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) && - (coefficients[1] == 1 || coefficients[1] == -1) && - (coefficients[2] == 1 || coefficients[2] == -1)) { - return Sum3LowerOrEqual( - coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]), - coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), - coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), - upper_bound)(model); - } - } - - if (params.new_linear_propagation()) { - const bool ok = model->GetOrCreate()->AddConstraint( - {}, vars, - std::vector(coefficients.begin(), coefficients.end()), - IntegerValue(upper_bound)); - if (!ok) { - auto* sat_solver = model->GetOrCreate(); - if (sat_solver->CurrentDecisionLevel() == 0) { - sat_solver->NotifyThatModelIsUnsat(); - } else { - LOG(FATAL) << "We currently do not support adding conflicting " - "constraint at positive level."; - } - } - } else { - IntegerSumLE* constraint = new IntegerSumLE( - {}, vars, - std::vector(coefficients.begin(), coefficients.end()), - IntegerValue(upper_bound), model); - constraint->RegisterWith(model->GetOrCreate()); - model->TakeOwnership(constraint); - } + return AddWeightedSumLowerOrEqual({}, vars, coefficients, upper_bound, + model); }; } @@ -502,52 +446,60 @@ inline std::function FixedWeightedSum( } // enforcement_literals => sum <= upper_bound -template -inline std::function ConditionalWeightedSumLowerOrEqual( - const std::vector& enforcement_literals, - const std::vector& vars, const VectorInt& coefficients, - int64_t upper_bound) { - // Special cases. - CHECK_GE(vars.size(), 1); +inline void AddWeightedSumLowerOrEqual( + absl::Span enforcement_literals, + absl::Span vars, + absl::Span coefficients, int64_t upper_bound, Model* model) { + // Linear1. + DCHECK_GE(vars.size(), 1); if (vars.size() == 1) { - CHECK_NE(coefficients[0], 0); - if (coefficients[0] > 0) { - return Implication( - enforcement_literals, - IntegerLiteral::LowerOrEqual( - vars[0], FloorRatio(IntegerValue(upper_bound), - IntegerValue(coefficients[0])))); + DCHECK_NE(coefficients[0], 0); + IntegerVariable var = vars[0]; + IntegerValue coeff(coefficients[0]); + if (coeff < 0) { + var = NegationOf(var); + coeff = -coeff; + } + const IntegerValue rhs = FloorRatio(IntegerValue(upper_bound), coeff); + if (enforcement_literals.empty()) { + model->Add(LowerOrEqual(var, rhs.value())); } else { - return Implication( + model->Add(Implication(enforcement_literals, + IntegerLiteral::LowerOrEqual(var, rhs))); + } + return; + } + + // Detect precedences with 2 and 3 terms. + const SatParameters& params = *model->GetOrCreate(); + if (!params.new_linear_propagation()) { + if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) && + (coefficients[1] == 1 || coefficients[1] == -1)) { + AddConditionalSum2LowerOrEqual( enforcement_literals, - IntegerLiteral::GreaterOrEqual( - vars[0], CeilRatio(IntegerValue(-upper_bound), - IntegerValue(-coefficients[0])))); + coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]), + coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound, + model); + return; + } + if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) && + (coefficients[1] == 1 || coefficients[1] == -1) && + (coefficients[2] == 1 || coefficients[2] == -1)) { + AddConditionalSum3LowerOrEqual( + enforcement_literals, + coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]), + coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), + coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound, + model); + return; } } - return [=](Model* model) { - const SatParameters& params = *model->GetOrCreate(); - if (!params.new_linear_propagation()) { - if (vars.size() == 2 && (coefficients[0] == 1 || coefficients[0] == -1) && - (coefficients[1] == 1 || coefficients[1] == -1)) { - return ConditionalSum2LowerOrEqual( - coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]), - coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), upper_bound, - enforcement_literals)(model); - } - if (vars.size() == 3 && (coefficients[0] == 1 || coefficients[0] == -1) && - (coefficients[1] == 1 || coefficients[1] == -1) && - (coefficients[2] == 1 || coefficients[2] == -1)) { - return ConditionalSum3LowerOrEqual( - coefficients[0] == 1 ? vars[0] : NegationOf(vars[0]), - coefficients[1] == 1 ? vars[1] : NegationOf(vars[1]), - coefficients[2] == 1 ? vars[2] : NegationOf(vars[2]), upper_bound, - enforcement_literals)(model); - } - } - - // If value == min(expression), then we can avoid creating the sum. + // If value == min(expression), then we can avoid creating the sum. + // + // TODO(user): Deal with the case with no enforcement literal, in case the + // presolve was turned off? + if (!enforcement_literals.empty()) { IntegerValue expression_min(0); auto* integer_trail = model->GetOrCreate(); for (int i = 0; i < vars.size(); ++i) { @@ -581,69 +533,63 @@ inline std::function ConditionalWeightedSumLowerOrEqual( } model->Add(ClauseConstraint(clause)); } - } else { - if (params.new_linear_propagation()) { - const bool ok = model->GetOrCreate()->AddConstraint( - enforcement_literals, vars, - std::vector(coefficients.begin(), coefficients.end()), - IntegerValue(upper_bound)); - if (!ok) { - auto* sat_solver = model->GetOrCreate(); - if (sat_solver->CurrentDecisionLevel() == 0) { - sat_solver->NotifyThatModelIsUnsat(); - } else { - LOG(FATAL) << "We currently do not support adding conflicting " - "constraint at positive level."; - } - } + return; + } + } + + if (params.new_linear_propagation()) { + const bool ok = model->GetOrCreate()->AddConstraint( + enforcement_literals, vars, + std::vector(coefficients.begin(), coefficients.end()), + IntegerValue(upper_bound)); + if (!ok) { + auto* sat_solver = model->GetOrCreate(); + if (sat_solver->CurrentDecisionLevel() == 0) { + sat_solver->NotifyThatModelIsUnsat(); } else { - IntegerSumLE* constraint = new IntegerSumLE( - enforcement_literals, vars, - std::vector(coefficients.begin(), coefficients.end()), - IntegerValue(upper_bound), model); - constraint->RegisterWith(model->GetOrCreate()); - model->TakeOwnership(constraint); + LOG(FATAL) << "We currently do not support adding conflicting " + "constraint at positive level."; } } - }; + } else { + IntegerSumLE* constraint = new IntegerSumLE( + enforcement_literals, vars, + std::vector(coefficients.begin(), coefficients.end()), + IntegerValue(upper_bound), model); + constraint->RegisterWith(model->GetOrCreate()); + model->TakeOwnership(constraint); + } } // enforcement_literals => sum >= lower_bound -template -inline std::function ConditionalWeightedSumGreaterOrEqual( - const std::vector& enforcement_literals, - const std::vector& vars, const VectorInt& coefficients, - int64_t lower_bound) { +inline void AddWeightedSumGreaterOrEqual( + absl::Span enforcement_literals, + absl::Span vars, + absl::Span coefficients, int64_t lower_bound, Model* model) { // We just negate everything and use an <= constraint. std::vector negated_coeffs(coefficients.begin(), coefficients.end()); for (int64_t& ref : negated_coeffs) ref = -ref; - return ConditionalWeightedSumLowerOrEqual(enforcement_literals, vars, - negated_coeffs, -lower_bound); + AddWeightedSumLowerOrEqual(enforcement_literals, vars, negated_coeffs, + -lower_bound, model); } -// Weighted sum <= constant reified. -template -inline std::function WeightedSumLowerOrEqualReif( - Literal is_le, const std::vector& vars, - const VectorInt& coefficients, int64_t upper_bound) { +// TODO(user): Delete once Telamon use new function. +inline std::function ConditionalWeightedSumLowerOrEqual( + const std::vector& enforcement_literals, + const std::vector& vars, + const std::vector& coefficients, int64_t upper_bound) { return [=](Model* model) { - model->Add(ConditionalWeightedSumLowerOrEqual({is_le}, vars, coefficients, - upper_bound)); - model->Add(ConditionalWeightedSumGreaterOrEqual( - {is_le.Negated()}, vars, coefficients, upper_bound + 1)); + AddWeightedSumLowerOrEqual(enforcement_literals, vars, coefficients, + upper_bound, model); }; } - -// Weighted sum >= constant reified. -template -inline std::function WeightedSumGreaterOrEqualReif( - Literal is_ge, const std::vector& vars, - const VectorInt& coefficients, int64_t lower_bound) { +inline std::function ConditionalWeightedSumGreaterOrEqual( + const std::vector& enforcement_literals, + const std::vector& vars, + const std::vector& coefficients, int64_t upper_bound) { return [=](Model* model) { - model->Add(ConditionalWeightedSumGreaterOrEqual({is_ge}, vars, coefficients, - lower_bound)); - model->Add(ConditionalWeightedSumLowerOrEqual( - {is_ge.Negated()}, vars, coefficients, lower_bound - 1)); + AddWeightedSumGreaterOrEqual(enforcement_literals, vars, coefficients, + upper_bound, model); }; } @@ -702,12 +648,12 @@ inline void LoadConditionalLinearConstraint( } if (cst.ub < kMaxIntegerValue) { - model->Add(ConditionalWeightedSumLowerOrEqual( - converted_literals, vars, converted_coeffs, cst.ub.value())); + AddWeightedSumLowerOrEqual(converted_literals, vars, converted_coeffs, + cst.ub.value(), model); } if (cst.lb > kMinIntegerValue) { - model->Add(ConditionalWeightedSumGreaterOrEqual( - converted_literals, vars, converted_coeffs, cst.lb.value())); + AddWeightedSumGreaterOrEqual(converted_literals, vars, converted_coeffs, + cst.lb.value(), model); } } @@ -720,40 +666,6 @@ inline void AddConditionalAffinePrecedence( LoadConditionalLinearConstraint(enforcement_literals, builder.Build(), model); } -// Weighted sum == constant reified. -// TODO(user): Simplify if the constant is at the edge of the possible values. -template -inline std::function FixedWeightedSumReif( - Literal is_eq, const std::vector& vars, - const VectorInt& coefficients, int64_t value) { - return [=](Model* model) { - // We creates two extra Boolean variables in this case. The alternative is - // to code a custom propagator for the direction equality => reified. - const Literal is_le = Literal(model->Add(NewBooleanVariable()), true); - const Literal is_ge = Literal(model->Add(NewBooleanVariable()), true); - model->Add(ReifiedBoolAnd({is_le, is_ge}, is_eq)); - model->Add(WeightedSumLowerOrEqualReif(is_le, vars, coefficients, value)); - model->Add(WeightedSumGreaterOrEqualReif(is_ge, vars, coefficients, value)); - }; -} - -// Weighted sum != constant. -// TODO(user): Simplify if the constant is at the edge of the possible values. -template -inline std::function WeightedSumNotEqual( - const std::vector& vars, const VectorInt& coefficients, - int64_t value) { - return [=](Model* model) { - // Exactly one of these alternative must be true. - const Literal is_lt = Literal(model->Add(NewBooleanVariable()), true); - const Literal is_gt = is_lt.Negated(); - model->Add(ConditionalWeightedSumLowerOrEqual(is_lt, vars, coefficients, - value - 1)); - model->Add(ConditionalWeightedSumGreaterOrEqual(is_gt, vars, coefficients, - value + 1)); - }; -} - // Model-based function to create an IntegerVariable that corresponds to the // given weighted sum of other IntegerVariables. // diff --git a/ortools/sat/precedences.h b/ortools/sat/precedences.h index 41245d5395..b021d55154 100644 --- a/ortools/sat/precedences.h +++ b/ortools/sat/precedences.h @@ -554,44 +554,22 @@ inline std::function AffineCoeffOneLowerOrEqualWithOffset( }; } -// a + b <= ub. -inline std::function Sum2LowerOrEqual(IntegerVariable a, - IntegerVariable b, - int64_t ub) { - return LowerOrEqualWithOffset(a, NegationOf(b), -ub); -} - // l => (a + b <= ub). -inline std::function ConditionalSum2LowerOrEqual( - IntegerVariable a, IntegerVariable b, int64_t ub, - const std::vector& enforcement_literals) { - return [=](Model* model) { - PrecedencesPropagator* p = model->GetOrCreate(); - p->AddPrecedenceWithAllOptions(a, NegationOf(b), IntegerValue(-ub), - kNoIntegerVariable, enforcement_literals); - }; -} - -// a + b + c <= ub. -inline std::function Sum3LowerOrEqual(IntegerVariable a, - IntegerVariable b, - IntegerVariable c, - int64_t ub) { - return [=](Model* model) { - PrecedencesPropagator* p = model->GetOrCreate(); - p->AddPrecedenceWithAllOptions(a, NegationOf(c), IntegerValue(-ub), b, {}); - }; +inline void AddConditionalSum2LowerOrEqual( + absl::Span enforcement_literals, IntegerVariable a, + IntegerVariable b, int64_t ub, Model* model) { + PrecedencesPropagator* p = model->GetOrCreate(); + p->AddPrecedenceWithAllOptions(a, NegationOf(b), IntegerValue(-ub), + kNoIntegerVariable, enforcement_literals); } // l => (a + b + c <= ub). -inline std::function ConditionalSum3LowerOrEqual( - IntegerVariable a, IntegerVariable b, IntegerVariable c, int64_t ub, - const std::vector& enforcement_literals) { - return [=](Model* model) { - PrecedencesPropagator* p = model->GetOrCreate(); - p->AddPrecedenceWithAllOptions(a, NegationOf(c), IntegerValue(-ub), b, - enforcement_literals); - }; +inline void AddConditionalSum3LowerOrEqual( + absl::Span enforcement_literals, IntegerVariable a, + IntegerVariable b, IntegerVariable c, int64_t ub, Model* model) { + PrecedencesPropagator* p = model->GetOrCreate(); + p->AddPrecedenceWithAllOptions(a, NegationOf(c), IntegerValue(-ub), b, + enforcement_literals); } // a >= b.