diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index a08299e8d9..14c92e4ae0 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -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 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::min(); - if (max_sum <= ub) ub = std::numeric_limits::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::min()) { - m->Add(ConditionalWeightedSumGreaterOrEqual({subdomain_literal}, vars, - coeffs, lb)); - } - if (ub != std::numeric_limits::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 clause; + std::vector for_enumeration; + auto* encoding = m->GetOrCreate(); + 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 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 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 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 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)); } } diff --git a/ortools/sat/cp_model_postsolve.cc b/ortools/sat/cp_model_postsolve.cc index a8428670f0..3e82437a0a 100644 --- a/ortools/sat/cp_model_postsolve.cc +++ b/ortools/sat/cp_model_postsolve.cc @@ -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* domains) { int64_t max_value = std::numeric_limits::min(); for (const LinearExpressionProto& expr : ct.lin_max().exprs()) { @@ -218,10 +218,15 @@ void PostsolveLinMax(const ConstraintProto& ct, std::vector* 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. diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 7ea16efce7..e54104f56b 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -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::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 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(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. diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index 61861313da..6b5538035c 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -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); diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 1e03ad5f9d..31ba1ca2b7 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -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)); diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 10876cfc56..4cebda89e0 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -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> constraint_to_intervals_; std::vector interval_usage_; - // Contains abs relation (key = abs(saved_variable)). - absl::flat_hash_map abs_relations_; - // Used by GetTrueLiteral()/GetFalseLiteral(). bool true_literal_is_defined_ = false; int true_literal_;