705 lines
28 KiB
C++
705 lines
28 KiB
C++
// Copyright 2010-2025 Google LLC
|
|
// Licensed under the Apache License, Version 2.0 (the "License");
|
|
// you may not use this file except in compliance with the License.
|
|
// You may obtain a copy of the License at
|
|
//
|
|
// http://www.apache.org/licenses/LICENSE-2.0
|
|
//
|
|
// Unless required by applicable law or agreed to in writing, software
|
|
// distributed under the License is distributed on an "AS IS" BASIS,
|
|
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
// See the License for the specific language governing permissions and
|
|
// limitations under the License.
|
|
|
|
#include "ortools/sat/presolve_encoding.h"
|
|
|
|
#include <cstdint>
|
|
#include <cstdlib>
|
|
#include <functional>
|
|
#include <limits>
|
|
#include <optional>
|
|
#include <utility>
|
|
#include <vector>
|
|
|
|
#include "absl/algorithm/container.h"
|
|
#include "absl/container/flat_hash_map.h"
|
|
#include "absl/container/flat_hash_set.h"
|
|
#include "absl/container/inlined_vector.h"
|
|
#include "absl/log/check.h"
|
|
#include "absl/log/log.h"
|
|
#include "google/protobuf/repeated_field.h"
|
|
#include "ortools/base/stl_util.h"
|
|
#include "ortools/sat/cp_model_utils.h"
|
|
#include "ortools/sat/presolve_context.h"
|
|
#include "ortools/util/bitset.h"
|
|
#include "ortools/util/sorted_interval_list.h"
|
|
|
|
namespace operations_research {
|
|
namespace sat {
|
|
|
|
namespace {
|
|
bool ConstraintIsEncodingBound(const ConstraintProto& ct) {
|
|
if (ct.constraint_case() != ConstraintProto::kLinear) return false;
|
|
if (ct.linear().vars_size() != 1) return false;
|
|
if (ct.linear().coeffs(0) != 1) return false;
|
|
if (ct.enforcement_literal_size() != 1) return false;
|
|
if (PositiveRef(ct.enforcement_literal(0)) == ct.linear().vars(0)) {
|
|
return false;
|
|
}
|
|
return true;
|
|
}
|
|
} // namespace
|
|
|
|
std::vector<VariableEncodingLocalModel> CreateVariableEncodingLocalModels(
|
|
PresolveContext* context) {
|
|
// In this function we want to make sure we don't waste too much time on
|
|
// problems that do not have many linear1. Thus, the first thing we do is to
|
|
// filter out as soon and cheaply as possible the bare minimum of constraints
|
|
// that could be relevant to the final output.
|
|
|
|
// Constraints taking a list of literals that can, under some conditions,
|
|
// accept the following substitution:
|
|
// constraint(a, b, ...) => constraint(a | b, ...)
|
|
// one obvious case is bool_or. But if we can know that a and b cannot be
|
|
// both true, we can also apply this to at_most_one and exactly_one.
|
|
//
|
|
// Note that in the implementation we might for simplicity refer to the
|
|
// constraints we are interested in as "bool_or" but this is just to avoid
|
|
// mentioning all the three types over and over.
|
|
// TODO(user): this should also work for linear constraints with the two
|
|
// booleans having the same coefficient?
|
|
std::vector<int> constraint_encoding_or; // bool_or, exactly_one, at_most_one
|
|
|
|
// Do a pass to gather all linear1 constraints.
|
|
absl::flat_hash_map<int, absl::InlinedVector<int, 1>> var_to_linear1;
|
|
for (int i = 0; i < context->working_model->constraints_size(); ++i) {
|
|
const ConstraintProto& ct = context->working_model->constraints(i);
|
|
if (ct.constraint_case() == ConstraintProto::kBoolOr ||
|
|
ct.constraint_case() == ConstraintProto::kAtMostOne ||
|
|
ct.constraint_case() == ConstraintProto::kExactlyOne) {
|
|
constraint_encoding_or.push_back(i);
|
|
continue;
|
|
}
|
|
if (!ConstraintIsEncodingBound(ct)) {
|
|
continue;
|
|
}
|
|
var_to_linear1[ct.linear().vars(0)].push_back(i);
|
|
}
|
|
|
|
// Filter out the variables that do not have an interesting encoding.
|
|
absl::erase_if(var_to_linear1, [context](const auto& p) {
|
|
if (p.second.size() > 1) return false;
|
|
return context->VarToConstraints(p.first).size() > 2;
|
|
});
|
|
|
|
if (var_to_linear1.empty()) return {};
|
|
|
|
absl::flat_hash_map<int, absl::InlinedVector<int, 2>> bool_to_var_encodings;
|
|
|
|
// Now we use the linear1 we found to see which bool_or/amo/exactly_one are
|
|
// linking two encodings of the same variable. But first, since some models
|
|
// have a lot of bool_or, we use a simple heuristic to filter out all that are
|
|
// not related to the encodings. We use a bitset to keep track of all boolean
|
|
// potentially encoding a domain for any variable and we filter out all
|
|
// bool_or that are not linked to at least two of these booleans.
|
|
Bitset64<int> booleans_potentially_encoding_domain(
|
|
context->working_model->variables_size());
|
|
|
|
for (const auto& [var, linear1_cts] : var_to_linear1) {
|
|
for (const int c : linear1_cts) {
|
|
const ConstraintProto& ct = context->working_model->constraints(c);
|
|
const int bool_var = PositiveRef(ct.enforcement_literal(0));
|
|
booleans_potentially_encoding_domain.Set(bool_var);
|
|
bool_to_var_encodings[bool_var].push_back(var);
|
|
}
|
|
}
|
|
for (auto& [bool_var, var_encodings] : bool_to_var_encodings) {
|
|
// Remove the potential duplicate for the negation.
|
|
gtl::STLSortAndRemoveDuplicates(&var_encodings);
|
|
}
|
|
int new_encoding_or_count = 0;
|
|
for (int i = 0; i < constraint_encoding_or.size(); ++i) {
|
|
const int c = constraint_encoding_or[i];
|
|
const ConstraintProto& ct = context->working_model->constraints(c);
|
|
const BoolArgumentProto& bool_ct =
|
|
ct.constraint_case() == ConstraintProto::kAtMostOne
|
|
? ct.at_most_one()
|
|
: (ct.constraint_case() == ConstraintProto::kExactlyOne
|
|
? ct.exactly_one()
|
|
: ct.bool_or());
|
|
if (absl::c_count_if(
|
|
bool_ct.literals(),
|
|
[booleans_potentially_encoding_domain](int ref) {
|
|
return booleans_potentially_encoding_domain[PositiveRef(ref)];
|
|
}) < 2) {
|
|
continue;
|
|
}
|
|
constraint_encoding_or[new_encoding_or_count++] = c;
|
|
}
|
|
constraint_encoding_or.resize(new_encoding_or_count);
|
|
|
|
// Track the number of times a given boolean appears in the local model for a
|
|
// given variable.
|
|
struct VariableAndBoolInfo {
|
|
// Can only be 1 or 2 (for negation) if properly presolved.
|
|
int linear1_count = 0;
|
|
// Number of times the boolean will appear in
|
|
// `constraints_linking_two_encoding_booleans`.
|
|
int bool_or_count = 0;
|
|
};
|
|
absl::flat_hash_map<std::pair<int, int>, VariableAndBoolInfo> var_bool_counts;
|
|
|
|
// Now that we have a potentially smaller set of bool_or, we actually check
|
|
// which of them are linking two encodings of the same variable.
|
|
absl::flat_hash_map<int, std::vector<int>> var_to_constraints_encoding_or;
|
|
|
|
// Map from variable to the bools that appear in a given bool_or.
|
|
absl::flat_hash_map<int, std::vector<int>> var_to_bools;
|
|
|
|
for (const int c : constraint_encoding_or) {
|
|
var_to_bools.clear();
|
|
const ConstraintProto& ct = context->working_model->constraints(c);
|
|
const BoolArgumentProto& bool_ct =
|
|
ct.constraint_case() == ConstraintProto::kAtMostOne
|
|
? ct.at_most_one()
|
|
: (ct.constraint_case() == ConstraintProto::kExactlyOne
|
|
? ct.exactly_one()
|
|
: ct.bool_or());
|
|
for (const int ref : bool_ct.literals()) {
|
|
const int bool_var = PositiveRef(ref);
|
|
if (!booleans_potentially_encoding_domain[bool_var]) continue;
|
|
for (const int var : bool_to_var_encodings[bool_var]) {
|
|
var_to_bools[var].push_back(bool_var);
|
|
}
|
|
}
|
|
for (const auto& [var, bools] : var_to_bools) {
|
|
if (bools.size() >= 2) {
|
|
// We have two encodings of `var` in the same constraint `c`. Thus `c`
|
|
// should be part of the local model for `var`.
|
|
var_to_constraints_encoding_or[var].push_back(c);
|
|
for (const int bool_var : bools) {
|
|
var_bool_counts[{var, bool_var}].bool_or_count++;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
std::vector<VariableEncodingLocalModel> local_models;
|
|
// Now that we have all the information, we can create the local models.
|
|
for (const auto& [var, linear1_cts] : var_to_linear1) {
|
|
VariableEncodingLocalModel& encoding_model = local_models.emplace_back();
|
|
encoding_model.var = var;
|
|
encoding_model.linear1_constraints.assign(linear1_cts.begin(),
|
|
linear1_cts.end());
|
|
encoding_model.constraints_linking_two_encoding_booleans =
|
|
var_to_constraints_encoding_or[var];
|
|
absl::c_sort(encoding_model.constraints_linking_two_encoding_booleans);
|
|
encoding_model.var_in_more_than_one_constraint_outside_the_local_model =
|
|
(context->VarToConstraints(var).size() - linear1_cts.size() > 1);
|
|
for (const int ct : linear1_cts) {
|
|
const int bool_var = PositiveRef(
|
|
context->working_model->constraints(ct).enforcement_literal(0));
|
|
encoding_model.bools_only_used_inside_the_local_model.insert(bool_var);
|
|
var_bool_counts[{var, bool_var}].linear1_count++;
|
|
}
|
|
absl::erase_if(encoding_model.bools_only_used_inside_the_local_model,
|
|
[context, v = var, &var_bool_counts](int bool_var) {
|
|
const auto& counts = var_bool_counts[{v, bool_var}];
|
|
return context->VarToConstraints(bool_var).size() !=
|
|
counts.linear1_count + counts.bool_or_count;
|
|
});
|
|
auto it = context->ObjectiveMap().find(var);
|
|
if (it != context->ObjectiveMap().end()) {
|
|
encoding_model.variable_coeff_in_objective = it->second;
|
|
}
|
|
}
|
|
absl::c_sort(local_models, [](const VariableEncodingLocalModel& a,
|
|
const VariableEncodingLocalModel& b) {
|
|
return a.var < b.var;
|
|
});
|
|
return local_models;
|
|
}
|
|
|
|
bool BasicPresolveAndGetFullyEncodedDomains(
|
|
PresolveContext* context, VariableEncodingLocalModel& local_model,
|
|
absl::flat_hash_map<int, Domain>* result, bool* changed) {
|
|
*changed = false;
|
|
absl::flat_hash_map<int, int> ref_to_linear1;
|
|
|
|
// Fill ref_to_linear1 and do some basic presolving.
|
|
const Domain var_domain = context->DomainOf(local_model.var);
|
|
for (const int ct : local_model.linear1_constraints) {
|
|
ConstraintProto* ct_proto = context->working_model->mutable_constraints(ct);
|
|
DCHECK(ConstraintIsEncodingBound(*ct_proto));
|
|
const int ref = ct_proto->enforcement_literal(0);
|
|
Domain domain = ReadDomainFromProto(ct_proto->linear());
|
|
if (!domain.IsIncludedIn(var_domain)) {
|
|
*changed = true;
|
|
domain = domain.IntersectionWith(context->DomainOf(local_model.var));
|
|
if (domain.IsEmpty()) {
|
|
context->UpdateRuleStats(
|
|
"variables: linear1 with domain not included in variable domain");
|
|
if (!context->SetLiteralToFalse(ref)) {
|
|
return false;
|
|
}
|
|
ct_proto->Clear();
|
|
context->UpdateConstraintVariableUsage(ct);
|
|
continue;
|
|
}
|
|
FillDomainInProto(domain, ct_proto->mutable_linear());
|
|
}
|
|
auto [it, inserted] = ref_to_linear1.insert({ref, ct});
|
|
if (!inserted) {
|
|
*changed = true;
|
|
ConstraintProto* old_ct_proto =
|
|
context->working_model->mutable_constraints(it->second);
|
|
const Domain old_ct_domain = ReadDomainFromProto(old_ct_proto->linear());
|
|
const Domain new_domain = domain.IntersectionWith(old_ct_domain);
|
|
ct_proto->Clear();
|
|
context->UpdateConstraintVariableUsage(ct);
|
|
if (new_domain.IsEmpty()) {
|
|
context->UpdateRuleStats(
|
|
"variables: linear1 with same variable and enforcement and "
|
|
"non-overlapping domain, setting enforcement to false");
|
|
if (!context->SetLiteralToFalse(ref)) {
|
|
return false;
|
|
}
|
|
old_ct_proto->Clear();
|
|
context->UpdateConstraintVariableUsage(it->second);
|
|
ref_to_linear1.erase(ref);
|
|
} else {
|
|
FillDomainInProto(new_domain, old_ct_proto->mutable_linear());
|
|
context->UpdateRuleStats(
|
|
"variables: merged two linear1 with same variable and enforcement");
|
|
}
|
|
}
|
|
}
|
|
|
|
// Remove from the local model anything that was removed in the loop above.
|
|
int new_linear1_size = 0;
|
|
for (int i = 0; i < local_model.linear1_constraints.size(); ++i) {
|
|
const int ct = local_model.linear1_constraints[i];
|
|
const ConstraintProto& ct_proto = context->working_model->constraints(ct);
|
|
if (ct_proto.constraint_case() != ConstraintProto::kLinear) continue;
|
|
if (context->IsFixed(ct_proto.enforcement_literal(0))) {
|
|
continue;
|
|
}
|
|
DCHECK(ConstraintIsEncodingBound(ct_proto));
|
|
local_model.linear1_constraints[new_linear1_size++] = ct;
|
|
}
|
|
if (new_linear1_size != local_model.linear1_constraints.size()) {
|
|
*changed = true;
|
|
local_model.linear1_constraints.resize(new_linear1_size);
|
|
// Rerun the presolve loop to recompute ref_to_linear1.
|
|
return true;
|
|
}
|
|
|
|
for (const auto& [ref, ct] : ref_to_linear1) {
|
|
auto it = ref_to_linear1.find(NegatedRef(ref));
|
|
if (it == ref_to_linear1.end()) continue;
|
|
const ConstraintProto& positive_ct =
|
|
context->working_model->constraints(ct);
|
|
const ConstraintProto& negative_ct =
|
|
context->working_model->constraints(it->second);
|
|
const Domain positive_domain = ReadDomainFromProto(positive_ct.linear());
|
|
const Domain negative_domain = ReadDomainFromProto(negative_ct.linear());
|
|
if (!positive_domain.IntersectionWith(negative_domain).IsEmpty()) {
|
|
// This is not a fully encoded domain. For example, it could be
|
|
// l => x in {-inf,inf}
|
|
// ~l => x in {-inf,inf}
|
|
// which actually means that `l` doesn't really encode anything.
|
|
continue;
|
|
}
|
|
bool domain_modified = false;
|
|
if (!context->IntersectDomainWith(
|
|
local_model.var, positive_domain.UnionWith(negative_domain),
|
|
&domain_modified)) {
|
|
return false;
|
|
}
|
|
*changed = *changed || domain_modified;
|
|
result->insert({ref, positive_domain});
|
|
result->insert({NegatedRef(ref), negative_domain});
|
|
}
|
|
|
|
// Now detect a different way of fully encoding a domain:
|
|
// l1 => x in D1
|
|
// l2 => x in D2
|
|
// l3 => x in D3
|
|
// ...
|
|
// l_n => x in D_n
|
|
// bool_or(l1, l2, l3, ..., l_n)
|
|
//
|
|
// where D1, D2, ..., D_n are non overlapping. This works too for exactly_one.
|
|
for (const int ct : local_model.constraints_linking_two_encoding_booleans) {
|
|
const ConstraintProto& ct_proto = context->working_model->constraints(ct);
|
|
if (ct_proto.constraint_case() != ConstraintProto::kBoolOr &&
|
|
ct_proto.constraint_case() != ConstraintProto::kExactlyOne) {
|
|
continue;
|
|
}
|
|
if (!ct_proto.enforcement_literal().empty()) continue;
|
|
const BoolArgumentProto& bool_or =
|
|
ct_proto.constraint_case() == ConstraintProto::kExactlyOne
|
|
? ct_proto.exactly_one()
|
|
: ct_proto.bool_or();
|
|
if (bool_or.literals().size() < 2) continue;
|
|
bool encoding_detected = true;
|
|
Domain non_overlapping_domain;
|
|
std::vector<std::pair<int, Domain>> ref_and_domains;
|
|
for (const int ref : bool_or.literals()) {
|
|
auto it = ref_to_linear1.find(ref);
|
|
if (it == ref_to_linear1.end()) {
|
|
encoding_detected = false;
|
|
break;
|
|
}
|
|
const Domain domain = ReadDomainFromProto(
|
|
context->working_model->constraints(it->second).linear());
|
|
ref_and_domains.push_back({ref, domain});
|
|
if (!non_overlapping_domain.IntersectionWith(domain).IsEmpty()) {
|
|
encoding_detected = false;
|
|
break;
|
|
}
|
|
non_overlapping_domain = non_overlapping_domain.UnionWith(domain);
|
|
}
|
|
if (encoding_detected) {
|
|
context->UpdateRuleStats("variables: detected fully encoded domain");
|
|
bool domain_modified = false;
|
|
if (!context->IntersectDomainWith(local_model.var, non_overlapping_domain,
|
|
&domain_modified)) {
|
|
return false;
|
|
}
|
|
if (domain_modified) {
|
|
context->UpdateRuleStats(
|
|
"variables: restricted domain to fully encoded domain");
|
|
}
|
|
*changed = *changed || domain_modified;
|
|
for (const auto& [ref, domain] : ref_and_domains) {
|
|
result->insert({ref, domain});
|
|
result->insert({NegatedRef(ref),
|
|
var_domain.IntersectionWith(domain.Complement())});
|
|
}
|
|
// Promote a bool_or to an exactly_one.
|
|
if (ct_proto.constraint_case() == ConstraintProto::kBoolOr) {
|
|
context->UpdateRuleStats(
|
|
"variables: promoted bool_or to exactly_one for fully encoded "
|
|
"domain");
|
|
std::vector<int> new_enforcement_literals(bool_or.literals().begin(),
|
|
bool_or.literals().end());
|
|
context->working_model->mutable_constraints(ct)->clear_bool_or();
|
|
context->working_model->mutable_constraints(ct)
|
|
->mutable_exactly_one()
|
|
->mutable_literals()
|
|
->Add(new_enforcement_literals.begin(),
|
|
new_enforcement_literals.end());
|
|
*changed = true;
|
|
}
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
// Return false on unsat
|
|
bool DetectEncodedComplexDomain(
|
|
PresolveContext* context, int ct_index,
|
|
VariableEncodingLocalModel& local_model,
|
|
absl::flat_hash_map<int, Domain>* fully_encoded_domains, bool* changed) {
|
|
ConstraintProto* ct = context->working_model->mutable_constraints(ct_index);
|
|
*changed = false;
|
|
|
|
if (context->ModelIsUnsat()) return false;
|
|
DCHECK(ct->constraint_case() == ConstraintProto::kAtMostOne ||
|
|
ct->constraint_case() == ConstraintProto::kExactlyOne ||
|
|
ct->constraint_case() == ConstraintProto::kBoolOr);
|
|
|
|
// Handling exaclty_one, at_most_one and bool_or is pretty similar. If we have
|
|
// l1 <=> v \in D1
|
|
// l2 <=> v \in D2
|
|
//
|
|
// We built
|
|
// l <=> v \in (D1 U D2).
|
|
//
|
|
// Moreover, if we have exactly_one(l1, l2, ...) or at_most_one(l1, l2, ...),
|
|
// we know that v cannot be in the intersection of D1 and D2. Thus, we first
|
|
// unconditionally remove (D1 ∩ D2) from the domain of v, making
|
|
// (l1=true and l2=true) impossible and allowing us to write our clauses as
|
|
// exactly_one(l1 or l2, ...) or at_most_one(l1 or l2, ...).
|
|
//
|
|
// Thus, other than the domain reduction that should not be done for the
|
|
// bool_or, all we need is to create a variable
|
|
// (l1 or l2) == l <=> (v \in (D1 U D2)).
|
|
google::protobuf::RepeatedField<int32_t>& literals =
|
|
ct->constraint_case() == ConstraintProto::kAtMostOne
|
|
? *ct->mutable_at_most_one()->mutable_literals()
|
|
: (ct->constraint_case() == ConstraintProto::kExactlyOne
|
|
? *ct->mutable_exactly_one()->mutable_literals()
|
|
: *ct->mutable_bool_or()->mutable_literals());
|
|
if (literals.size() <= 1) return true;
|
|
|
|
if (!ct->enforcement_literal().empty()) {
|
|
// TODO(user): support this case if it any problem needs it.
|
|
return true;
|
|
}
|
|
|
|
// When we have
|
|
// lit => var in D1
|
|
// ~lit => var in D2
|
|
// we can represent this on a line:
|
|
//
|
|
// ----------------D1----------------
|
|
// ----------------D2---------------
|
|
// |+++++++++++|*********************|++++++++++|
|
|
// lit=false lit unconstrained lit=true
|
|
//
|
|
// Handling the case where the variable is unconstrained by the lit is a
|
|
// bit of a pain: we want to replace two literals in a exactly_one by a
|
|
// single one, and if they are both unconstrained we might be forced to pick
|
|
// one arbitrarily to set to true. In any case, this is not a proper
|
|
// encoding of a complex domain, so we just ignore it.
|
|
// TODO(user): This can be implemented if it turns out to be common.
|
|
|
|
std::optional<int> maybe_lit1;
|
|
Domain domain_lit1;
|
|
std::optional<int> maybe_lit2;
|
|
Domain domain_lit2;
|
|
for (const int lit_var : literals) {
|
|
if (!local_model.bools_only_used_inside_the_local_model.contains(
|
|
PositiveRef(lit_var))) {
|
|
continue;
|
|
}
|
|
auto it = fully_encoded_domains->find(lit_var);
|
|
if (it == fully_encoded_domains->end()) {
|
|
continue;
|
|
}
|
|
|
|
if (!maybe_lit1) {
|
|
maybe_lit1 = lit_var;
|
|
domain_lit1 = it->second;
|
|
} else {
|
|
maybe_lit2 = lit_var;
|
|
domain_lit2 = it->second;
|
|
break;
|
|
}
|
|
}
|
|
|
|
if (!maybe_lit2.has_value()) return true;
|
|
DCHECK(maybe_lit1.has_value());
|
|
const int lit1 = *maybe_lit1;
|
|
const int lit2 = *maybe_lit2;
|
|
|
|
// We found two literals that each fully encodes an interval and are both only
|
|
// used in the encoding and in the bool_or/exactly_one/at_most_one. We can
|
|
// thus replace the two literals by their OR. Since this code is already
|
|
// rather complex, so we will just simplify a pair of literals at a time, and
|
|
// leave for the presolve fixpoint to do the rest.
|
|
*changed = true;
|
|
|
|
context->UpdateRuleStats(
|
|
"variables: detected encoding of a complex domain with multiple "
|
|
"linear1");
|
|
|
|
if (ct->constraint_case() != ConstraintProto::kBoolOr) {
|
|
// In virtue of the AMO, var must not be in the intersection of the two
|
|
// domains where both literals are true.
|
|
if (!context->IntersectDomainWith(
|
|
local_model.var,
|
|
domain_lit2.IntersectionWith(domain_lit1).Complement())) {
|
|
return false;
|
|
}
|
|
}
|
|
const Domain var_domain = context->DomainOf(local_model.var);
|
|
const Domain domain_new_var_false = var_domain.IntersectionWith(
|
|
domain_lit1.Complement().IntersectionWith(domain_lit2.Complement()));
|
|
const Domain domain_new_var_true =
|
|
var_domain.IntersectionWith(domain_new_var_false.Complement());
|
|
|
|
// Now we want to build a lit3 = (lit1 or lit2) to use in the AMO/bool_or.
|
|
const int new_var = context->NewBoolVarWithClause({lit1, lit2});
|
|
|
|
if (domain_new_var_true.IsEmpty()) {
|
|
CHECK(context->SetLiteralToFalse(new_var));
|
|
} else if (domain_new_var_false.IsEmpty()) {
|
|
CHECK(context->SetLiteralToTrue(new_var));
|
|
} else {
|
|
local_model.linear1_constraints.push_back(
|
|
context->working_model->constraints_size());
|
|
ConstraintProto* new_ct = context->working_model->add_constraints();
|
|
new_ct->add_enforcement_literal(new_var);
|
|
new_ct->mutable_linear()->add_vars(local_model.var);
|
|
new_ct->mutable_linear()->add_coeffs(1);
|
|
FillDomainInProto(domain_new_var_true, new_ct->mutable_linear());
|
|
local_model.linear1_constraints.push_back(
|
|
context->working_model->constraints_size());
|
|
new_ct = context->working_model->add_constraints();
|
|
new_ct->add_enforcement_literal(NegatedRef(new_var));
|
|
new_ct->mutable_linear()->add_vars(local_model.var);
|
|
new_ct->mutable_linear()->add_coeffs(1);
|
|
FillDomainInProto(domain_new_var_false, new_ct->mutable_linear());
|
|
context->UpdateNewConstraintsVariableUsage();
|
|
}
|
|
|
|
// Remove the two literals from the AMO.
|
|
int new_size = 0;
|
|
for (int i = 0; i < literals.size(); ++i) {
|
|
if (literals.Get(i) != lit1 && literals.Get(i) != lit2) {
|
|
literals.Set(new_size++, literals.Get(i));
|
|
}
|
|
}
|
|
literals.Truncate(new_size);
|
|
literals.Add(new_var);
|
|
context->UpdateConstraintVariableUsage(ct_index);
|
|
|
|
// Finally, move the four linear1 to the mapping model.
|
|
fully_encoded_domains->insert({new_var, domain_new_var_true});
|
|
fully_encoded_domains->insert({NegatedRef(new_var), domain_new_var_false});
|
|
fully_encoded_domains->erase(lit1);
|
|
fully_encoded_domains->erase(lit2);
|
|
fully_encoded_domains->erase(NegatedRef(lit1));
|
|
fully_encoded_domains->erase(NegatedRef(lit2));
|
|
context->MarkVariableAsRemoved(PositiveRef(lit1));
|
|
context->MarkVariableAsRemoved(PositiveRef(lit2));
|
|
int new_linear1_size = 0;
|
|
for (int i = 0; i < local_model.linear1_constraints.size(); ++i) {
|
|
const int ct = local_model.linear1_constraints[i];
|
|
ConstraintProto* ct_proto = context->working_model->mutable_constraints(ct);
|
|
if (PositiveRef(ct_proto->enforcement_literal(0)) == PositiveRef(lit1) ||
|
|
PositiveRef(ct_proto->enforcement_literal(0)) == PositiveRef(lit2)) {
|
|
context->NewMappingConstraint(*ct_proto, __FILE__, __LINE__);
|
|
ct_proto->Clear();
|
|
context->UpdateConstraintVariableUsage(ct);
|
|
continue;
|
|
}
|
|
local_model.linear1_constraints[new_linear1_size++] = ct;
|
|
}
|
|
local_model.linear1_constraints.resize(new_linear1_size);
|
|
|
|
return true;
|
|
}
|
|
|
|
bool DetectAllEncodedComplexDomain(PresolveContext* context,
|
|
VariableEncodingLocalModel& local_model) {
|
|
absl::flat_hash_map<int, Domain> fully_encoded_domains;
|
|
bool changed_on_basic_presolve = false;
|
|
if (!BasicPresolveAndGetFullyEncodedDomains(context, local_model,
|
|
&fully_encoded_domains,
|
|
&changed_on_basic_presolve)) {
|
|
return false;
|
|
}
|
|
if (local_model.constraints_linking_two_encoding_booleans.size() != 1) {
|
|
return true;
|
|
}
|
|
const int ct = local_model.constraints_linking_two_encoding_booleans[0];
|
|
bool changed = true;
|
|
while (changed) {
|
|
if (!DetectEncodedComplexDomain(context, ct, local_model,
|
|
&fully_encoded_domains, &changed)) {
|
|
return false;
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool MaybeTransferLinear1ToAnotherVariable(
|
|
VariableEncodingLocalModel& local_model, PresolveContext* context) {
|
|
if (local_model.var == -1) return true;
|
|
if (local_model.variable_coeff_in_objective != 0) return true;
|
|
if (local_model.single_constraint_using_the_var_outside_the_local_model ==
|
|
-1) {
|
|
return true;
|
|
}
|
|
const int other_c =
|
|
local_model.single_constraint_using_the_var_outside_the_local_model;
|
|
|
|
const std::vector<int>& to_rewrite = local_model.linear1_constraints;
|
|
|
|
// 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 true;
|
|
}
|
|
|
|
// 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;
|
|
|
|
const int var = local_model.var;
|
|
// 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 = target, expr = expr](const Domain& implied) {
|
|
Domain target_domain =
|
|
implied.ContinuousMultiplicationBy(target.coeffs(0))
|
|
.AdditionWith(Domain(target.offset()));
|
|
target_domain = target_domain.IntersectionWith(
|
|
Domain(0, std::numeric_limits<int64_t>::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 true;
|
|
}
|
|
|
|
// Applies transfer_f to all linear1.
|
|
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 true;
|
|
}
|
|
|
|
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 (!context->MarkConstraintAsFalse(ct, "linear1: unsat transfer")) {
|
|
return false;
|
|
}
|
|
} else if (new_domain == current) {
|
|
// Note that we don't need to remove this constraint from
|
|
// local_model.linear1_constraints since we will set
|
|
// local_model.var = -1 below.
|
|
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->NewMappingConstraint(other_ct, __FILE__, __LINE__);
|
|
context->working_model->mutable_constraints(other_c)->Clear();
|
|
context->UpdateConstraintVariableUsage(other_c);
|
|
context->MarkVariableAsRemoved(var);
|
|
local_model.var = -1;
|
|
return true;
|
|
}
|
|
} // namespace sat
|
|
} // namespace operations_research
|