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

[CP-SAT] fix #3643

Browse Source
This commit is contained in:
Laurent Perron
2023-01-25 18:36:12 +01:00
parent 46f3f1bd79
commit 49a72a8d67
4 changed files with 72 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

21
ortools/sat/cp_model_presolve.cc
View File

@@ -3720,8 +3720,18 @@ void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint(
// TODO(user): If 2 * min_coeff_magnitude >= bound, then the constraint can
// be completely rewriten to 2 * (enforcement_part) + sum var >= 2 which is
// what happen eventually when bound is even, but not if it is odd currently.
const int64_t second_threshold = std::max(CeilOfRatio(threshold, int64_t{2}),
threshold - min_coeff_magnitude);
int64_t second_threshold = std::max(CeilOfRatio(threshold, int64_t{2}),
threshold - min_coeff_magnitude);
// Tricky: The second threshold only work if the domain is simple. If the
// domain has holes, changing the coefficient might change whether the
// variable can be at one or not by herself.
//
// TODO(user): We could still reduce it to the smaller value with same
// feasibility.
if (rhs_domain.NumIntervals() > 1) {
second_threshold = threshold; // Disable.
}
// Do we only extract Booleans?
//
@@ -9179,9 +9189,14 @@ void CpModelPresolver::ProcessVariableInTwoAtMostOrExactlyOne(int var) {
// We can always sum the two constraints.
// If var appear in one and not(var) in the other, the two term cancel out to
// one, so we still have an <= 1 (or eventually a ==1 (see below).
//
// Note that if the constraint are of size one, they can just be preprocessed
// individually and just be removed. So we abort here as the code below
// is incorrect if new_ct is an empty constraint.
context_->tmp_literals.clear();
int c1_ref = std::numeric_limits<int>::min();
const ConstraintProto& ct1 = context_->working_model->constraints(c1);
if (AtMostOneOrExactlyOneLiterals(ct1).size() <= 1) return;
for (const int lit : AtMostOneOrExactlyOneLiterals(ct1)) {
if (PositiveRef(lit) == var) {
c1_ref = lit;
@@ -9191,6 +9206,7 @@ void CpModelPresolver::ProcessVariableInTwoAtMostOrExactlyOne(int var) {
}
int c2_ref = std::numeric_limits<int>::min();
const ConstraintProto& ct2 = context_->working_model->constraints(c2);
if (AtMostOneOrExactlyOneLiterals(ct2).size() <= 1) return;
for (const int lit : AtMostOneOrExactlyOneLiterals(ct2)) {
if (PositiveRef(lit) == var) {
c2_ref = lit;
@@ -9261,6 +9277,7 @@ void CpModelPresolver::ProcessVariableInTwoAtMostOrExactlyOne(int var) {
// TODO(user): If the merged list contains duplicates or literal that are
// negation of other, we need to deal with that right away. For some reason
// something is not robust to that it seems. Investigate & fix!
DCHECK_NE(new_ct->constraint_case(), ConstraintProto::CONSTRAINT_NOT_SET);
if (PresolveAtMostOrExactlyOne(new_ct)) {
context_->UpdateConstraintVariableUsage(new_ct_index);
}

44
ortools/sat/cuts.cc
View File

@@ -939,12 +939,30 @@ CoverCutHelper::~CoverCutHelper() {
// Try a simple cover heuristic.
// Look for violated CUT of the form: sum (UB - X) or (X - LB) >= 1.
int CoverCutHelper::GetCoverSize(int relevant_size, IntegerValue* rhs) {
relevant_size =
std::partition(
base_ct_.terms.begin(), base_ct_.terms.begin() + relevant_size,
[](const CutTerm& t) { return t.LpDistToMaxValue() < 0.9999; }) -
base_ct_.terms.begin();
std::sort(base_ct_.terms.begin(), base_ct_.terms.begin() + relevant_size,
if (relevant_size == 0) return 0;
// Sorting can be slow, so we start by splitting the vector in 3 parts
// [can always be in cover, candidates, can never be in cover].
int part1 = 0;
const double threshold = 1.0 / static_cast<double>(relevant_size);
for (int i = 0; i < relevant_size;) {
const double dist = base_ct_.terms[i].LpDistToMaxValue();
if (dist < threshold) {
// Move to part 1.
std::swap(base_ct_.terms[i], base_ct_.terms[part1]);
++i;
++part1;
} else if (dist < 0.9999) {
// Keep in part 2.
++i;
} else {
// Exclude entirely (part 3).
--relevant_size;
std::swap(base_ct_.terms[i], base_ct_.terms[relevant_size]);
}
}
std::sort(base_ct_.terms.begin() + part1,
base_ct_.terms.begin() + relevant_size,
[](const CutTerm& a, const CutTerm& b) {
const double dist_a = a.LpDistToMaxValue();
const double dist_b = b.LpDistToMaxValue();
@@ -978,7 +996,7 @@ int CoverCutHelper::GetCoverSize(int relevant_size, IntegerValue* rhs) {
// Abort early if we run into overflow.
// In that case, rhs must be negative, and we can try this cover still.
cover_size = i;
CHECK_LT(*rhs, 0);
DCHECK_LT(*rhs, 0);
break;
}
}
@@ -1010,26 +1028,26 @@ int CoverCutHelper::GetCoverSize(int relevant_size, IntegerValue* rhs) {
*rhs += t.bound_diff * t.coeff;
std::swap(base_ct_.terms[i], base_ct_.terms[--cover_size]);
}
CHECK_GT(cover_size, 0);
DCHECK_GT(cover_size, 0);
return cover_size;
}
bool CoverCutHelper::MakeAllTermsPositive() {
bool CoverCutHelper::MakeAllTermsPositive(CutData* cut) {
// Make sure each coeff is positive.
//
// TODO(user): maybe we should do it all at once to avoid some overflow
// condition.
for (CutTerm& term : base_ct_.terms) {
for (CutTerm& term : cut->terms) {
if (term.coeff >= 0) continue;
if (!term.Complement(&base_ct_.rhs)) {
if (!term.Complement(&cut->rhs)) {
++total_num_overflow_abort_;
return false;
}
}
// We should have aborted early if the base constraint was already infeasible.
CHECK_GE(base_ct_.rhs, 0);
CHECK_GE(cut->rhs, 0);
return true;
}
@@ -1037,7 +1055,6 @@ bool CoverCutHelper::TrySimpleKnapsack(const CutData& input,
ImpliedBoundsProcessor* ib_processor) {
cut_.Clear();
base_ct_ = input;
if (!MakeAllTermsPositive()) return false;
if (ib_processor != nullptr) {
cut_builder_.RegisterAllBooleansTerms(base_ct_);
@@ -1147,7 +1164,6 @@ bool CoverCutHelper::TryWithLetchfordSouliLifting(
const CutData& input, ImpliedBoundsProcessor* ib_processor) {
cut_.Clear();
base_ct_ = input;
if (!MakeAllTermsPositive()) return false;
// Perform IB expansion with no restriction, all coeff should still be
// positive.

11
ortools/sat/cuts.h
View File

@@ -442,6 +442,14 @@ class CoverCutHelper {
public:
~CoverCutHelper();
// Complements term to make sure all coeff are positive, returns false on
// overflow.
//
// Important: This must be called on the input of both Try*() functions. It
// is separated as an optimization to share the loop rather than do it in
// both functions.
bool MakeAllTermsPositive(CutData* cut);
// Try to find a cut with a knapsack heuristic.
// If this returns true, you can get the cut via cut().
bool TrySimpleKnapsack(const CutData& input,
@@ -484,9 +492,6 @@ class CoverCutHelper {
void SetSharedStatistics(SharedStatistics* stats) { shared_stats_ = stats; }
private:
// This changes base_ct_, returns false on overflow.
bool MakeAllTermsPositive();
// This looks at base_ct_ and reoder the terms so that the first ones are in
// the cover. return zero if no interesting cover was found.
int GetCoverSize(int relevant_size, IntegerValue* rhs);

28
ortools/sat/linear_programming_constraint.cc
View File

@@ -912,19 +912,6 @@ bool LinearProgrammingConstraint::AddCutFromConstraints(
tmp_slack_rows_.push_back(row);
}
// Try cover approach to find cut.
// TODO(user): Optimize by merging common steps (sort mainly).
if (cover_cut_helper_.TrySimpleKnapsack(base_ct_, ib_processor)) {
at_least_one_added |= PostprocessAndAddCut(
absl::StrCat(name, "_KB"), cover_cut_helper_.Info(), first_slack,
cover_cut_helper_.cut());
}
if (cover_cut_helper_.TryWithLetchfordSouliLifting(base_ct_, ib_processor)) {
at_least_one_added |= PostprocessAndAddCut(
absl::StrCat(name, "_KL"), cover_cut_helper_.Info(), first_slack,
cover_cut_helper_.cut());
}
// Try integer rounding heuristic to find cut.
RoundingOptions options;
options.max_scaling = parameters_.max_integer_rounding_scaling();
@@ -955,6 +942,21 @@ bool LinearProgrammingConstraint::AddCutFromConstraints(
first_slack, integer_rounding_cut_helper_.cut());
}
// Try cover approach to find cut.
if (cover_cut_helper_.MakeAllTermsPositive(&base_ct_)) {
if (cover_cut_helper_.TrySimpleKnapsack(base_ct_, ib_processor)) {
at_least_one_added |= PostprocessAndAddCut(
absl::StrCat(name, "_KB"), cover_cut_helper_.Info(), first_slack,
cover_cut_helper_.cut());
}
if (cover_cut_helper_.TryWithLetchfordSouliLifting(base_ct_,
ib_processor)) {
at_least_one_added |= PostprocessAndAddCut(
absl::StrCat(name, "_KL"), cover_cut_helper_.Info(), first_slack,
cover_cut_helper_.cut());
}
}
return at_least_one_added;
}