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

[CP-SAT] detect implied no_overlap

Browse Source
This commit is contained in:
Laurent Perron
2024-04-24 14:33:38 +02:00
committed by Corentin Le Molgat
parent 2d9fc6bbbc
commit 40fb68305e
4 changed files with 151 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files

150
ortools/sat/cp_model_presolve.cc
View File

@@ -2063,6 +2063,9 @@ bool CpModelPresolver::CanonicalizeLinear(ConstraintProto* ct) {
changed |= DivideLinearByGcd(ct);
// For duplicate detection, we always make the first coeff positive.
//
// TODO(user): Move that to context_->CanonicalizeLinearConstraint(), and do
// the same for LinearExpressionProto.
if (!ct->linear().coeffs().empty() && ct->linear().coeffs(0) < 0) {
for (int64_t& ref_coeff : *ct->mutable_linear()->mutable_coeffs()) {
ref_coeff = -ref_coeff;
@@ -8825,6 +8828,33 @@ void CpModelPresolver::DetectDifferentVariables() {
if (context_->ModelIsUnsat()) return;
PresolveTimer timer(__FUNCTION__, logger_, time_limit_);
// List the variable that are pairwise different, also store in offset[x, y]
// the offsets such that x >= y + offset.second OR y >= x + offset.first.
std::vector<std::pair<int, int>> different_vars;
absl::flat_hash_map<std::pair<int, int>, std::pair<int64_t, int64_t>> offsets;
// Process the fact "v1 - v2 \in Domain".
const auto process_difference = [&different_vars, &offsets](int v1, int v2,
Domain d) {
Domain exclusion = d.Complement().PartAroundZero();
if (exclusion.IsEmpty()) return;
if (v1 == v2) return;
std::pair<int, int> key = {v1, v2};
if (v1 > v2) {
std::swap(key.first, key.second);
exclusion = exclusion.Negation();
}
// We have x - y not in exclusion,
// so x - y > exclusion.Max() --> x > y + exclusion.Max();
// OR x - y < exclusion.Min() --> y > x - exclusion.Min();
different_vars.push_back(key);
offsets[key] = {exclusion.Min() == std::numeric_limits<int64_t>::min()
? std::numeric_limits<int64_t>::max()
: CapAdd(-exclusion.Min(), 1),
CapAdd(exclusion.Max(), 1)};
};
// Try to find identical linear constraint with incompatible domains.
// This works really well on neos16.mps.gz where we have
// a <=> x <= y
@@ -8844,8 +8874,8 @@ void CpModelPresolver::DetectDifferentVariables() {
// different. If we can detect that, then we close the problem quickly instead
// of not closing it.
bool has_all_diff = false;
bool has_no_overlap = false;
std::vector<std::pair<uint64_t, int>> hashes;
std::vector<std::pair<int, int>> different_vars;
const int num_constraints = context_->working_model->constraints_size();
for (int c = 0; c < num_constraints; ++c) {
const ConstraintProto& ct = context_->working_model->constraints(c);
@@ -8853,15 +8883,25 @@ void CpModelPresolver::DetectDifferentVariables() {
has_all_diff = true;
continue;
}
if (ct.constraint_case() == ConstraintProto::kNoOverlap) {
has_no_overlap = true;
continue;
}
if (ct.constraint_case() != ConstraintProto::kLinear) continue;
if (ct.linear().vars().size() == 1) continue;
// Detect direct encoding of x != y. Note that we also see that from x > y
// and related.
if (ct.linear().vars().size() == 2 && ct.enforcement_literal().empty() &&
ct.linear().coeffs(0) == -ct.linear().coeffs(1) &&
!ReadDomainFromProto(ct.linear()).Contains(0)) {
different_vars.push_back({ct.linear().vars(0), ct.linear().vars(1)});
ct.linear().coeffs(0) == -ct.linear().coeffs(1)) {
// We assume the constraint was already divided by its gcd.
if (ct.linear().coeffs(0) == 1) {
process_difference(ct.linear().vars(0), ct.linear().vars(1),
ReadDomainFromProto(ct.linear()));
} else if (ct.linear().coeffs(0) == -1) {
process_difference(ct.linear().vars(1), ct.linear().vars(0),
ReadDomainFromProto(ct.linear()).Negation());
}
}
// TODO(user): Handle this case?
@@ -8931,12 +8971,21 @@ void CpModelPresolver::DetectDifferentVariables() {
// Detect x != y via lit => x > y && not(lit) => x < y.
if (ct1.linear().vars().size() == 2 &&
ct1.linear().coeffs(0) == -ct1.linear().coeffs(1) &&
!ReadDomainFromProto(ct1.linear()).Contains(0) &&
!ReadDomainFromProto(ct2.linear()).Contains(0) &&
ct1.enforcement_literal(0) ==
NegatedRef(ct2.enforcement_literal(0))) {
different_vars.push_back(
{ct1.linear().vars(0), ct1.linear().vars(1)});
// We have x - y in domain1 or in domain2, so it must be in the union.
Domain union_of_domain =
ReadDomainFromProto(ct1.linear())
.UnionWith(ReadDomainFromProto(ct2.linear()));
// We assume the constraint was already divided by its gcd.
if (ct1.linear().coeffs(0) == 1) {
process_difference(ct1.linear().vars(0), ct1.linear().vars(1),
std::move(union_of_domain));
} else if (ct1.linear().coeffs(0) == -1) {
process_difference(ct1.linear().vars(1), ct1.linear().vars(0),
union_of_domain.Negation());
}
}
context_->UpdateRuleStats("incompatible linear: add implication");
@@ -8962,7 +9011,7 @@ void CpModelPresolver::DetectDifferentVariables() {
// TODO(user): Only add them at the end of the presolve! it hurt our presolve
// (like probing is slower) and only serve for linear relaxation.
if (context_->params().infer_all_diffs() && !has_all_diff &&
different_vars.size() > 2) {
!has_no_overlap && different_vars.size() > 2) {
WallTimer local_time;
local_time.Start();
@@ -9001,18 +9050,85 @@ void CpModelPresolver::DetectDifferentVariables() {
int num_cliques = 0;
int64_t cumulative_size = 0;
for (const std::vector<Literal>& clique : cliques) {
for (std::vector<Literal>& clique : cliques) {
if (clique.size() <= 2) continue;
++num_cliques;
cumulative_size += clique.size();
context_->UpdateRuleStats("all_diff: inferred from x != y constraints");
auto* new_ct =
context_->working_model->add_constraints()->mutable_all_diff();
for (const Literal l : clique) {
auto* expr = new_ct->add_exprs();
expr->add_vars(l.Variable().value());
expr->add_coeffs(1);
std::sort(clique.begin(), clique.end());
// We have an all-diff, but inspect the offsets to see if we have a
// disjunctive ! Note that this is quadratic, but no more complex than the
// scan of the model we just did above, since we had one linear constraint
// per entry.
const int num_terms = clique.size();
std::vector<int64_t> sizes(num_terms,
std::numeric_limits<int64_t>::max());
for (int i = 0; i < num_terms; ++i) {
const int v1 = clique[i].Variable().value();
for (int j = i + 1; j < num_terms; ++j) {
const int v2 = clique[j].Variable().value();
const auto [o1, o2] = offsets.at({v1, v2});
sizes[i] = std::min(sizes[i], o1);
sizes[j] = std::min(sizes[j], o2);
}
}
int num_greater_than_one = 0;
int64_t issue = 0;
for (int i = 0; i < num_terms; ++i) {
CHECK_GE(sizes[i], 1);
if (sizes[i] > 1) ++num_greater_than_one;
// When this happens, it means this interval can never be before
// any other. We should probably handle this case better, but for now we
// abort.
issue = CapAdd(issue, sizes[i]);
if (issue == std::numeric_limits<int64_t>::max()) {
context_->UpdateRuleStats("TODO no_overlap: with task always last");
num_greater_than_one = 0;
break;
}
}
if (num_greater_than_one > 0) {
// We have one size greater than 1, lets add a no_overlap!
//
// TODO(user): try to remove all the quadratic boolean and their
// corresponding linear2 ? Any Boolean not used elsewhere could be
// removed.
context_->UpdateRuleStats(
"no_overlap: inferred from x != y constraints");
std::vector<int> intervals;
for (int i = 0; i < num_terms; ++i) {
intervals.push_back(context_->working_model->constraints().size());
auto* new_interval =
context_->working_model->add_constraints()->mutable_interval();
new_interval->mutable_start()->set_offset(0);
new_interval->mutable_start()->add_coeffs(1);
new_interval->mutable_start()->add_vars(clique[i].Variable().value());
new_interval->mutable_size()->set_offset(sizes[i]);
new_interval->mutable_end()->set_offset(sizes[i]);
new_interval->mutable_end()->add_coeffs(1);
new_interval->mutable_end()->add_vars(clique[i].Variable().value());
}
auto* new_ct =
context_->working_model->add_constraints()->mutable_no_overlap();
for (const int interval : intervals) {
new_ct->add_intervals(interval);
}
} else {
context_->UpdateRuleStats("all_diff: inferred from x != y constraints");
auto* new_ct =
context_->working_model->add_constraints()->mutable_all_diff();
for (const Literal l : clique) {
auto* expr = new_ct->add_exprs();
expr->add_vars(l.Variable().value());
expr->add_coeffs(1);
}
}
}

3
ortools/sat/sat_parameters.proto
View File

@@ -519,6 +519,9 @@ message SatParameters {
// for instance. Note that we only run this code if there is no all_diff
// already in the model so that if a user want to add some all_diff, we assume
// it is well done and do not try to add more.
//
// This will also detect and add no_overlap constraints, if all the relations
// x != y have "offsets" between them. I.e. x > y + offset.
optional bool infer_all_diffs = 233 [default = true];
// Try to find large "rectangle" in the linear constraint matrix with

9
ortools/util/sorted_interval_list.cc
View File

@@ -239,6 +239,15 @@ int64_t Domain::SmallestValue() const {
return result;
}
Domain Domain::PartAroundZero() const {
for (const ClosedInterval interval : intervals_) {
if (interval.start <= 0 && interval.end >= 0) {
return Domain(interval.start, interval.end);
}
}
return Domain();
}
// TODO(user): Use std::upper_bound() like in ValueAtOrBefore() ?
int64_t Domain::ClosestValue(int64_t wanted) const {
DCHECK(!IsEmpty());

6
ortools/util/sorted_interval_list.h
View File

@@ -277,6 +277,12 @@ class Domain {
int64_t ValueAtOrBefore(int64_t input) const;
int64_t ValueAtOrAfter(int64_t input) const;
/**
* If the domain contains zero, this return the simple interval around it.
* Otherwise, this returns an empty domain.
*/
Domain PartAroundZero() const;
/**
* Returns true iff the domain is reduced to a single value.
* The domain must not be empty.