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

[CP-SAT] improve diffn and linear loading

Browse Source
This commit is contained in:
Laurent Perron
2024-03-26 12:35:12 +01:00
committed by Corentin Le Molgat
parent f2187ed41c
commit f3f9bc44a2
5 changed files with 130 additions and 254 deletions
Download Patch File Download Diff File Expand all files Collapse all files

54
ortools/sat/cp_model_loader.cc
View File

@@ -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<int64_t>::min();
if (max_sum <= ub) ub = std::numeric_limits<int64_t>::max();
if (!HasEnforcementLiteral(ct)) {
if (all_booleans) {
// TODO(user): we should probably also implement an
// half-reified version of this constraint.
std::vector<LiteralWithCoeff> 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<int64_t>::min()) {
m->Add(WeightedSumGreaterOrEqual(vars, coeffs, lb));
}
if (ub != std::numeric_limits<int64_t>::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<Literal> 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<LiteralWithCoeff> 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<SatSolver>()->AddLinearConstraint(
/*use_lower_bound=*/(min_sum < lb), lb,
/*use_upper_bound=*/(max_sum > ub), ub, &cst);
} else {
const std::vector<Literal> enforcement_literals =
mapping->Literals(ct.enforcement_literal());
if (lb != std::numeric_limits<int64_t>::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<int64_t>::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);
}
}

2
ortools/sat/diffn.cc
View File

@@ -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() !=

2
ortools/sat/integer.h
View File

@@ -1912,7 +1912,7 @@ inline std::function<void(Model*)> Equality(IntegerVariable v, int64_t value) {
// is the same as using different underlying variable for an integer literal and
// its negation.
inline std::function<void(Model*)> Implication(
const std::vector<Literal>& enforcement_literals, IntegerLiteral i) {
absl::Span<const Literal> enforcement_literals, IntegerLiteral i) {
return [=](Model* model) {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
if (i.bound <= integer_trail->LowerBound(i.var)) {

280
ortools/sat/integer_expr.h
View File

@@ -417,65 +417,9 @@ template <typename VectorInt>
inline std::function<void(Model*)> WeightedSumLowerOrEqual(
const std::vector<IntegerVariable>& 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<SatParameters>();
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<LinearPropagator>()->AddConstraint(
{}, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound));
if (!ok) {
auto* sat_solver = model->GetOrCreate<SatSolver>();
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<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
}
return AddWeightedSumLowerOrEqual({}, vars, coefficients, upper_bound,
model);
};
}
@@ -502,52 +446,60 @@ inline std::function<void(Model*)> FixedWeightedSum(
}
// enforcement_literals => sum <= upper_bound
template <typename VectorInt>
inline std::function<void(Model*)> ConditionalWeightedSumLowerOrEqual(
const std::vector<Literal>& enforcement_literals,
const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
int64_t upper_bound) {
// Special cases.
CHECK_GE(vars.size(), 1);
inline void AddWeightedSumLowerOrEqual(
absl::Span<const Literal> enforcement_literals,
absl::Span<const IntegerVariable> vars,
absl::Span<const int64_t> 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<SatParameters>();
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<SatParameters>();
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<IntegerTrail>();
for (int i = 0; i < vars.size(); ++i) {
@@ -581,69 +533,63 @@ inline std::function<void(Model*)> ConditionalWeightedSumLowerOrEqual(
}
model->Add(ClauseConstraint(clause));
}
} else {
if (params.new_linear_propagation()) {
const bool ok = model->GetOrCreate<LinearPropagator>()->AddConstraint(
enforcement_literals, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound));
if (!ok) {
auto* sat_solver = model->GetOrCreate<SatSolver>();
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<LinearPropagator>()->AddConstraint(
enforcement_literals, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound));
if (!ok) {
auto* sat_solver = model->GetOrCreate<SatSolver>();
if (sat_solver->CurrentDecisionLevel() == 0) {
sat_solver->NotifyThatModelIsUnsat();
} else {
IntegerSumLE* constraint = new IntegerSumLE(
enforcement_literals, vars,
std::vector<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
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<IntegerValue>(coefficients.begin(), coefficients.end()),
IntegerValue(upper_bound), model);
constraint->RegisterWith(model->GetOrCreate<GenericLiteralWatcher>());
model->TakeOwnership(constraint);
}
}
// enforcement_literals => sum >= lower_bound
template <typename VectorInt>
inline std::function<void(Model*)> ConditionalWeightedSumGreaterOrEqual(
const std::vector<Literal>& enforcement_literals,
const std::vector<IntegerVariable>& vars, const VectorInt& coefficients,
int64_t lower_bound) {
inline void AddWeightedSumGreaterOrEqual(
absl::Span<const Literal> enforcement_literals,
absl::Span<const IntegerVariable> vars,
absl::Span<const int64_t> coefficients, int64_t lower_bound, Model* model) {
// We just negate everything and use an <= constraint.
std::vector<int64_t> 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 <typename VectorInt>
inline std::function<void(Model*)> WeightedSumLowerOrEqualReif(
Literal is_le, const std::vector<IntegerVariable>& vars,
const VectorInt& coefficients, int64_t upper_bound) {
// TODO(user): Delete once Telamon use new function.
inline std::function<void(Model*)> ConditionalWeightedSumLowerOrEqual(
const std::vector<Literal>& enforcement_literals,
const std::vector<IntegerVariable>& vars,
const std::vector<int64_t>& 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 <typename VectorInt>
inline std::function<void(Model*)> WeightedSumGreaterOrEqualReif(
Literal is_ge, const std::vector<IntegerVariable>& vars,
const VectorInt& coefficients, int64_t lower_bound) {
inline std::function<void(Model*)> ConditionalWeightedSumGreaterOrEqual(
const std::vector<Literal>& enforcement_literals,
const std::vector<IntegerVariable>& vars,
const std::vector<int64_t>& 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 <typename VectorInt>
inline std::function<void(Model*)> FixedWeightedSumReif(
Literal is_eq, const std::vector<IntegerVariable>& 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 <typename VectorInt>
inline std::function<void(Model*)> WeightedSumNotEqual(
const std::vector<IntegerVariable>& 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.
//

46
ortools/sat/precedences.h
View File

@@ -554,44 +554,22 @@ inline std::function<void(Model*)> AffineCoeffOneLowerOrEqualWithOffset(
};
}
// a + b <= ub.
inline std::function<void(Model*)> Sum2LowerOrEqual(IntegerVariable a,
IntegerVariable b,
int64_t ub) {
return LowerOrEqualWithOffset(a, NegationOf(b), -ub);
}
// l => (a + b <= ub).
inline std::function<void(Model*)> ConditionalSum2LowerOrEqual(
IntegerVariable a, IntegerVariable b, int64_t ub,
const std::vector<Literal>& enforcement_literals) {
return [=](Model* model) {
PrecedencesPropagator* p = model->GetOrCreate<PrecedencesPropagator>();
p->AddPrecedenceWithAllOptions(a, NegationOf(b), IntegerValue(-ub),
kNoIntegerVariable, enforcement_literals);
};
}
// a + b + c <= ub.
inline std::function<void(Model*)> Sum3LowerOrEqual(IntegerVariable a,
IntegerVariable b,
IntegerVariable c,
int64_t ub) {
return [=](Model* model) {
PrecedencesPropagator* p = model->GetOrCreate<PrecedencesPropagator>();
p->AddPrecedenceWithAllOptions(a, NegationOf(c), IntegerValue(-ub), b, {});
};
inline void AddConditionalSum2LowerOrEqual(
absl::Span<const Literal> enforcement_literals, IntegerVariable a,
IntegerVariable b, int64_t ub, Model* model) {
PrecedencesPropagator* p = model->GetOrCreate<PrecedencesPropagator>();
p->AddPrecedenceWithAllOptions(a, NegationOf(b), IntegerValue(-ub),
kNoIntegerVariable, enforcement_literals);
}
// l => (a + b + c <= ub).
inline std::function<void(Model*)> ConditionalSum3LowerOrEqual(
IntegerVariable a, IntegerVariable b, IntegerVariable c, int64_t ub,
const std::vector<Literal>& enforcement_literals) {
return [=](Model* model) {
PrecedencesPropagator* p = model->GetOrCreate<PrecedencesPropagator>();
p->AddPrecedenceWithAllOptions(a, NegationOf(c), IntegerValue(-ub), b,
enforcement_literals);
};
inline void AddConditionalSum3LowerOrEqual(
absl::Span<const Literal> enforcement_literals, IntegerVariable a,
IntegerVariable b, IntegerVariable c, int64_t ub, Model* model) {
PrecedencesPropagator* p = model->GetOrCreate<PrecedencesPropagator>();
p->AddPrecedenceWithAllOptions(a, NegationOf(c), IntegerValue(-ub), b,
enforcement_literals);
}
// a >= b.