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

[CP-SAT] more presolve around int_abs

Browse Source
This commit is contained in:
Laurent Perron
2023-11-09 13:46:44 +01:00
parent cdd5de3e60
commit 41bdec18d5
6 changed files with 234 additions and 159 deletions
Download Patch File Download Diff File Expand all files Collapse all files

116
ortools/sat/cp_model_loader.cc
View File

@@ -1401,64 +1401,88 @@ void LoadLinearConstraint(const ConstraintProto& ct, Model* m) {
coeffs, ub));
}
}
} else {
// In this case, we can create just one Boolean instead of two since one
// is the negation of the other.
const bool special_case =
ct.enforcement_literal().empty() && ct.linear().domain_size() == 4;
return;
}
std::vector<Literal> clause;
for (int i = 0; i < ct.linear().domain_size(); i += 2) {
int64_t lb = ct.linear().domain(i);
int64_t ub = ct.linear().domain(i + 1);
if (min_sum >= lb) lb = std::numeric_limits<int64_t>::min();
if (max_sum <= ub) ub = std::numeric_limits<int64_t>::max();
// We have a linear with a complex Domain, we need to create extra Booleans.
const Literal subdomain_literal(
special_case && i > 0 ? clause.back().Negated()
: Literal(m->Add(NewBooleanVariable()), true));
clause.push_back(subdomain_literal);
// In this case, we can create just one Boolean instead of two since one
// is the negation of the other.
const bool special_case =
ct.enforcement_literal().empty() && ct.linear().domain_size() == 4;
if (lb != std::numeric_limits<int64_t>::min()) {
m->Add(ConditionalWeightedSumGreaterOrEqual({subdomain_literal}, vars,
coeffs, lb));
}
if (ub != std::numeric_limits<int64_t>::max()) {
m->Add(ConditionalWeightedSumLowerOrEqual({subdomain_literal}, vars,
coeffs, ub));
// For enforcement => var \in domain, we can potentially reuse the encoding
// literal directly rather than creating new ones.
const bool is_linear1 = !special_case && vars.size() == 1 && coeffs[0] == 1;
std::vector<Literal> clause;
std::vector<Literal> for_enumeration;
auto* encoding = m->GetOrCreate<IntegerEncoder>();
for (int i = 0; i < ct.linear().domain_size(); i += 2) {
const int64_t lb = ct.linear().domain(i);
const int64_t ub = ct.linear().domain(i + 1);
if (is_linear1) {
if (lb == ub) {
clause.push_back(
encoding->GetOrCreateLiteralAssociatedToEquality(vars[0], lb));
continue;
} else if (min_sum >= lb) {
clause.push_back(encoding->GetOrCreateAssociatedLiteral(
IntegerLiteral::LowerOrEqual(vars[0], ub)));
continue;
} else if (max_sum <= ub) {
clause.push_back(encoding->GetOrCreateAssociatedLiteral(
IntegerLiteral::GreaterOrEqual(vars[0], lb)));
continue;
}
}
const std::vector<Literal> enforcement_literals =
mapping->Literals(ct.enforcement_literal());
const Literal subdomain_literal(
special_case && i > 0 ? clause.back().Negated()
: Literal(m->Add(NewBooleanVariable()), true));
clause.push_back(subdomain_literal);
for_enumeration.push_back(subdomain_literal);
// Make sure all booleans are tights when enumerating all solutions.
if (params.enumerate_all_solutions() && !enforcement_literals.empty()) {
Literal linear_is_enforced;
if (enforcement_literals.size() == 1) {
linear_is_enforced = enforcement_literals[0];
} else {
linear_is_enforced = Literal(m->Add(NewBooleanVariable()), true);
std::vector<Literal> maintain_linear_is_enforced;
for (const Literal e_lit : enforcement_literals) {
m->Add(Implication(e_lit.Negated(), linear_is_enforced.Negated()));
maintain_linear_is_enforced.push_back(e_lit.Negated());
}
maintain_linear_is_enforced.push_back(linear_is_enforced);
m->Add(ClauseConstraint(maintain_linear_is_enforced));
}
for (const Literal lit : clause) {
m->Add(Implication(linear_is_enforced.Negated(), lit.Negated()));
if (special_case) break; // For the unique Boolean var to be false.
}
if (min_sum < lb) {
m->Add(ConditionalWeightedSumGreaterOrEqual({subdomain_literal}, vars,
coeffs, lb));
}
if (max_sum > ub) {
m->Add(ConditionalWeightedSumLowerOrEqual({subdomain_literal}, vars,
coeffs, ub));
}
}
if (!special_case) {
const std::vector<Literal> enforcement_literals =
mapping->Literals(ct.enforcement_literal());
// Make sure all booleans are tights when enumerating all solutions.
if (params.enumerate_all_solutions() && !enforcement_literals.empty()) {
Literal linear_is_enforced;
if (enforcement_literals.size() == 1) {
linear_is_enforced = enforcement_literals[0];
} else {
linear_is_enforced = Literal(m->Add(NewBooleanVariable()), true);
std::vector<Literal> maintain_linear_is_enforced;
for (const Literal e_lit : enforcement_literals) {
clause.push_back(e_lit.Negated());
m->Add(Implication(e_lit.Negated(), linear_is_enforced.Negated()));
maintain_linear_is_enforced.push_back(e_lit.Negated());
}
m->Add(ClauseConstraint(clause));
maintain_linear_is_enforced.push_back(linear_is_enforced);
m->Add(ClauseConstraint(maintain_linear_is_enforced));
}
for (const Literal lit : for_enumeration) {
m->Add(Implication(linear_is_enforced.Negated(), lit.Negated()));
if (special_case) break; // For the unique Boolean var to be false.
}
}
if (!special_case) {
for (const Literal e_lit : enforcement_literals) {
clause.push_back(e_lit.Negated());
}
m->Add(ClauseConstraint(clause));
}
}

19
ortools/sat/cp_model_postsolve.cc
View File

@@ -208,9 +208,9 @@ int64_t EvaluateLinearExpression(const LinearExpressionProto& expr,
} // namespace
// Compute the max of each expression, and assign it to the target expr (which
// must be of the form +ref or -ref); We only support post-solving the case
// where whatever the value of all expression, there will be a valid target.
// Compute the max of each expression, and assign it to the target expr. We only
// support post-solving the case where whatever the value of all expression,
// there will be a valid target.
void PostsolveLinMax(const ConstraintProto& ct, std::vector<Domain>* domains) {
int64_t max_value = std::numeric_limits<int64_t>::min();
for (const LinearExpressionProto& expr : ct.lin_max().exprs()) {
@@ -218,10 +218,15 @@ void PostsolveLinMax(const ConstraintProto& ct, std::vector<Domain>* domains) {
// one of the expression refer to the target itself !
max_value = std::max(max_value, EvaluateLinearExpression(expr, *domains));
}
const int target_ref = GetSingleRefFromExpression(ct.lin_max().target());
const int target_var = PositiveRef(target_ref);
(*domains)[target_var] =
Domain(RefIsPositive(target_ref) ? max_value : -max_value);
const LinearExpressionProto& target = ct.lin_max().target();
CHECK_EQ(target.vars().size(), 1);
CHECK(RefIsPositive(target.vars(0)));
max_value -= target.offset();
CHECK_EQ(max_value % target.coeffs(0), 0);
max_value /= target.coeffs(0);
(*domains)[target.vars(0)] = Domain(max_value);
}
// We only support 3 cases in the presolve currently.

186
ortools/sat/cp_model_presolve.cc
View File

@@ -762,7 +762,6 @@ bool CpModelPresolver::DivideLinMaxByGcd(int c, ConstraintProto* ct) {
bool CpModelPresolver::PresolveLinMax(ConstraintProto* ct) {
if (context_->ModelIsUnsat()) return false;
if (HasEnforcementLiteral(*ct)) return false;
const LinearExpressionProto& target = ct->lin_max().target();
// x = max(x, xi...) => forall i, x >= xi.
@@ -1189,21 +1188,6 @@ bool CpModelPresolver::PresolveIntAbs(ConstraintProto* ct) {
return RemoveConstraint(ct);
}
// Store the x == abs(y) relation if expr and target_expr can be cast into a
// ref.
// TODO(user): Support general affine expression in for expr in the Store
// method call.
{
if (ExpressionContainsSingleRef(target_expr) &&
ExpressionContainsSingleRef(expr)) {
const int target_ref = GetSingleRefFromExpression(target_expr);
const int expr_ref = GetSingleRefFromExpression(expr);
if (context_->StoreAbsRelation(target_ref, expr_ref)) {
context_->UpdateRuleStats("int_abs: store abs(x) == y");
}
}
}
return false;
}
@@ -2408,37 +2392,6 @@ bool CpModelPresolver::PresolveLinearOfSizeOne(ConstraintProto* ct) {
}
}
// If the constraint is literal => x in domain and x = abs(abs_arg), we can
// replace x by abs_arg and hopefully remove the variable x later.
//
// Tricky: Note that we do not do that for "encoding" constraints as this
// can be problematic if it is referenced by HasVarValueEncoding().
int abs_arg;
if (context_->GetAbsRelation(var, &abs_arg) && var != abs_arg) {
DCHECK(RefIsPositive(abs_arg));
context_->UpdateRuleStats("linear1: remove abs from abs(x) in domain");
const Domain implied_abs_target_domain =
rhs.IntersectionWith({0, std::numeric_limits<int64_t>::max()});
if (implied_abs_target_domain.IsEmpty()) {
return MarkConstraintAsFalse(ct);
}
const Domain new_abs_var_domain =
implied_abs_target_domain
.UnionWith(implied_abs_target_domain.Negation())
.IntersectionWith(context_->DomainOf(abs_arg));
if (new_abs_var_domain.IsEmpty()) {
return MarkConstraintAsFalse(ct);
}
// Modify the constraint in-place.
ct->clear_linear();
ct->mutable_linear()->add_vars(abs_arg);
ct->mutable_linear()->add_coeffs(1);
FillDomainInProto(new_abs_var_domain, ct->mutable_linear());
return true;
}
return false;
}
@@ -7695,16 +7648,15 @@ void CpModelPresolver::TransformIntoMaxCliques() {
namespace {
bool IsAffineIntAbs(ConstraintProto* ct) {
if (ct->constraint_case() != ConstraintProto::kLinMax ||
ct->lin_max().exprs_size() != 2 ||
ct->lin_max().target().vars_size() > 1 ||
ct->lin_max().exprs(0).vars_size() != 1 ||
ct->lin_max().exprs(1).vars_size() != 1) {
bool IsAffineIntAbs(const ConstraintProto& ct) {
if (ct.constraint_case() != ConstraintProto::kLinMax ||
ct.lin_max().exprs_size() != 2 || ct.lin_max().target().vars_size() > 1 ||
ct.lin_max().exprs(0).vars_size() != 1 ||
ct.lin_max().exprs(1).vars_size() != 1) {
return false;
}
const LinearArgumentProto& lin_max = ct->lin_max();
const LinearArgumentProto& lin_max = ct.lin_max();
if (lin_max.exprs(0).offset() != -lin_max.exprs(1).offset()) return false;
if (PositiveRef(lin_max.exprs(0).vars(0)) !=
PositiveRef(lin_max.exprs(1).vars(0))) {
@@ -7753,7 +7705,7 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
context_->UpdateConstraintVariableUsage(c);
}
if (!DivideLinMaxByGcd(c, ct)) return false;
if (IsAffineIntAbs(ct)) {
if (IsAffineIntAbs(*ct)) {
return PresolveIntAbs(ct);
} else {
return PresolveLinMax(ct);
@@ -10042,6 +9994,121 @@ void CpModelPresolver::ProcessVariableInTwoAtMostOrExactlyOne(int var) {
}
}
// If we have a bunch of constraint of the form literal => Y \in domain and
// another constraint Y = f(X), we can remove Y, that constraint, and transform
// all linear1 from constraining Y to constraining X.
//
// We can for instance do it for Y = abs(X) or Y = X^2 easily. More complex
// function might be trickier.
//
// Note that we can't always do it in the reverse direction though!
// If we have l => X = -1, we can't transfer that to abs(X) for instance, since
// X=1 will also map to abs(-1). We can only do it if for all implied domain D
// we have f^-1(f(D)) = D, which is not easy to check.
void CpModelPresolver::MaybeTransferLinear1ToAnotherVariable(int var) {
// Find the extra constraint and do basic CHECKs.
int other_c;
int num_others = 0;
std::vector<int> to_rewrite;
for (const int c : context_->VarToConstraints(var)) {
if (c >= 0) {
const ConstraintProto& ct = context_->working_model->constraints(c);
if (ct.constraint_case() == ConstraintProto::kLinear &&
ct.linear().vars().size() == 1) {
to_rewrite.push_back(c);
continue;
}
}
++num_others;
other_c = c;
}
if (num_others != 1) return;
if (other_c < 0) return;
// In general constraint with more than two variable can't be removed.
// Similarly for linear2 with non-fixed rhs as we would need to check the form
// of all implied domain.
const auto& other_ct = context_->working_model->constraints(other_c);
if (context_->ConstraintToVars(other_c).size() != 2 ||
!other_ct.enforcement_literal().empty() ||
other_ct.constraint_case() == ConstraintProto::kLinear) {
return;
}
// This will be the rewriting function. It takes the implied domain of var
// from linear1, and return a pair {new_var, new_var_implied_domain}.
std::function<std::pair<int, Domain>(const Domain& implied)> transfer_f =
nullptr;
// We only support a few cases.
//
// TODO(user): implement more! Note that the linear2 case was tempting, but if
// we don't have an equality, we can't transfer, and if we do, we actually
// have affine equivalence already.
if (other_ct.constraint_case() == ConstraintProto::kLinMax &&
other_ct.lin_max().target().vars().size() == 1 &&
other_ct.lin_max().target().vars(0) == var &&
std::abs(other_ct.lin_max().target().coeffs(0)) == 1 &&
IsAffineIntAbs(other_ct)) {
context_->UpdateRuleStats("linear1: transferred from abs(X) to X");
const LinearExpressionProto& target = other_ct.lin_max().target();
const LinearExpressionProto& expr = other_ct.lin_max().exprs(0);
transfer_f = [target, expr](const Domain& implied) {
Domain target_domain =
implied.ContinuousMultiplicationBy(target.coeffs(0))
.AdditionWith(Domain(target.offset()));
target_domain =
target_domain.IntersectionWith(Domain(0, target_domain.Max()));
// We have target = abs(expr).
const Domain expr_domain =
target_domain.UnionWith(target_domain.Negation());
const Domain new_domain = expr_domain.AdditionWith(Domain(-expr.offset()))
.InverseMultiplicationBy(expr.coeffs(0));
return std::make_pair(expr.vars(0), new_domain);
};
}
if (transfer_f == nullptr) {
context_->UpdateRuleStats(
"TODO linear1: appear in only one extra 2-var constraint");
return;
}
// Applies transfer_f to all linear1.
std::sort(to_rewrite.begin(), to_rewrite.end());
const Domain var_domain = context_->DomainOf(var);
for (const int c : to_rewrite) {
ConstraintProto* ct = context_->working_model->mutable_constraints(c);
if (ct->linear().vars(0) != var || ct->linear().coeffs(0) != 1) {
// This shouldn't happen.
LOG(INFO) << "Aborted in MaybeTransferLinear1ToAnotherVariable()";
return;
}
const Domain implied =
var_domain.IntersectionWith(ReadDomainFromProto(ct->linear()));
auto [new_var, new_domain] = transfer_f(implied);
const Domain current = context_->DomainOf(new_var);
new_domain = new_domain.IntersectionWith(current);
if (new_domain.IsEmpty()) {
if (!MarkConstraintAsFalse(ct)) return;
} else if (new_domain == current) {
ct->Clear();
} else {
ct->mutable_linear()->set_vars(0, new_var);
FillDomainInProto(new_domain, ct->mutable_linear());
}
context_->UpdateConstraintVariableUsage(c);
}
// Copy other_ct to the mapping model and delete var!
*context_->mapping_model->add_constraints() = other_ct;
context_->working_model->mutable_constraints(other_c)->Clear();
context_->UpdateConstraintVariableUsage(other_c);
context_->MarkVariableAsRemoved(var);
}
// TODO(user): We can still remove the variable even if we want to keep
// all feasible solutions for the cases when we have a full encoding.
//
@@ -10056,11 +10123,18 @@ void CpModelPresolver::ProcessVariableOnlyUsedInEncoding(int var) {
if (context_->IsFixed(var)) return;
if (context_->VariableWasRemoved(var)) return;
if (context_->CanBeUsedAsLiteral(var)) return;
if (!context_->VariableIsOnlyUsedInEncodingAndMaybeInObjective(var)) return;
if (context_->params().search_branching() == SatParameters::FIXED_SEARCH) {
return;
}
if (!context_->VariableIsOnlyUsedInEncodingAndMaybeInObjective(var)) {
if (context_->VariableIsOnlyUsedInLinear1AndOneExtraConstraint(var)) {
MaybeTransferLinear1ToAnotherVariable(var);
return;
}
return;
}
// If a variable var only appear in enf => var \in domain and in the
// objective, we can remove its costs and the variable/constraint by
// transferring part of the cost to the enforcement.

1
ortools/sat/cp_model_presolve.h
View File

@@ -251,6 +251,7 @@ class CpModelPresolver {
// merge this with what ExpandObjective() is doing.
void ShiftObjectiveWithExactlyOnes();
void MaybeTransferLinear1ToAnotherVariable(int var);
void ProcessVariableOnlyUsedInEncoding(int var);
void TryToSimplifyDomain(int var);

52
ortools/sat/presolve_context.cc
View File

@@ -379,14 +379,23 @@ bool PresolveContext::VariableWasRemoved(int ref) const {
}
bool PresolveContext::VariableIsOnlyUsedInEncodingAndMaybeInObjective(
int ref) const {
int var) const {
CHECK(RefIsPositive(var));
if (!ConstraintVariableGraphIsUpToDate()) return false;
const int var = PositiveRef(ref);
if (var_to_num_linear1_[var] == 0) return false;
return var_to_num_linear1_[var] == var_to_constraints_[var].size() ||
(var_to_constraints_[var].contains(kObjectiveConstraint) &&
var_to_num_linear1_[var] + 1 == var_to_constraints_[var].size());
}
bool PresolveContext::VariableIsOnlyUsedInLinear1AndOneExtraConstraint(
int var) const {
if (!ConstraintVariableGraphIsUpToDate()) return false;
if (var_to_num_linear1_[var] == 0) return false;
CHECK(RefIsPositive(var));
return var_to_num_linear1_[var] + 1 == var_to_constraints_[var].size();
}
Domain PresolveContext::DomainOf(int ref) const {
Domain result;
if (RefIsPositive(ref)) {
@@ -1075,45 +1084,6 @@ bool PresolveContext::StoreBooleanEqualityRelation(int ref_a, int ref_b) {
return StoreAffineRelation(var_a, var_b, /*coeff=*/-1, /*offset=*/1);
}
bool PresolveContext::StoreAbsRelation(int target_ref, int ref) {
const auto insert_status = abs_relations_.insert(
std::make_pair(target_ref, SavedVariable(PositiveRef(ref))));
if (!insert_status.second) {
// Tricky: overwrite if the old value refer to a now unused variable.
const int candidate = insert_status.first->second.Get();
if (removed_variables_.contains(candidate) ||
GetAffineRelation(candidate).representative != candidate) {
insert_status.first->second = SavedVariable(PositiveRef(ref));
return true;
}
return false;
}
return true;
}
bool PresolveContext::GetAbsRelation(int target_ref, int* ref) {
// This is currently only called with representative and positive ref.
// It is important to keep it like this.
CHECK(RefIsPositive(target_ref));
CHECK_EQ(GetAffineRelation(target_ref).representative, target_ref);
auto it = abs_relations_.find(target_ref);
if (it == abs_relations_.end()) return false;
// Tricky: In some rare case the stored relation can refer to a deleted
// variable, so we need to ignore it. We also ignore any relation involving
// a variable that has a different affine representatitive.
const int candidate = PositiveRef(it->second.Get());
if (removed_variables_.contains(candidate) ||
GetAffineRelation(candidate).representative != candidate) {
abs_relations_.erase(it);
return false;
}
CHECK(!VariableWasRemoved(candidate));
*ref = candidate;
return true;
}
int PresolveContext::GetLiteralRepresentative(int ref) const {
const AffineRelation::Relation r = GetAffineRelation(PositiveRef(ref));

19
ortools/sat/presolve_context.h
View File

@@ -218,7 +218,16 @@ class PresolveContext {
// constraints of the form lit => var in domain. When this is the case, then
// we can usually remove this variable and replace these constraints with
// the proper constraints on the enforcement literals.
bool VariableIsOnlyUsedInEncodingAndMaybeInObjective(int ref) const;
bool VariableIsOnlyUsedInEncodingAndMaybeInObjective(int var) const;
// Similar to VariableIsOnlyUsedInEncodingAndMaybeInObjective() for the case
// where we have one extra constraint instead of the objective. Sometimes it
// is possible to transfer the linear1 domain restrictions to another
// variable. for instance if the other constraint is of the form Y = abs(X) or
// Y = X^2, then a domain restriction on Y can be transferred to X. We can
// then move the extra constraint to the mapping model and remove one
// variable. This happens on the flatzinc celar problems for instance.
bool VariableIsOnlyUsedInLinear1AndOneExtraConstraint(int var) const;
// Returns false if the new domain is empty. Sets 'domain_modified' (if
// provided) to true iff the domain is modified otherwise does not change it.
@@ -313,11 +322,6 @@ class PresolveContext {
// Returns false if this makes the problem infeasible.
bool StoreBooleanEqualityRelation(int ref_a, int ref_b);
// Stores/Get the relation target_ref = abs(ref); The first function returns
// false if it already exist and the second false if it is not present.
bool StoreAbsRelation(int target_ref, int ref);
bool GetAbsRelation(int target_ref, int* ref);
// Returns the representative of a literal.
int GetLiteralRepresentative(int ref) const;
@@ -660,9 +664,6 @@ class PresolveContext {
std::vector<std::vector<int>> constraint_to_intervals_;
std::vector<int> interval_usage_;
// Contains abs relation (key = abs(saved_variable)).
absl::flat_hash_map<int, SavedVariable> abs_relations_;
// Used by GetTrueLiteral()/GetFalseLiteral().
bool true_literal_is_defined_ = false;
int true_literal_;