operations_research::sat::CoverCutHelper Class Reference

Helper to find knapsack cover cuts. More...

#include <cuts.h>

Public Member Functions
	~CoverCutHelper ()
bool	TrySimpleKnapsack (const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
bool	TryWithLetchfordSouliLifting (const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
bool	TrySingleNodeFlow (const CutData &input_ct, ImpliedBoundsProcessor *ib_processor=nullptr)
const CutData &	cut () const
	If successful, info about the last generated cut.
std::string	Info () const
	Single line of text that we append to the cut log line.
void	SetSharedStatistics (SharedStatistics *stats)
void	ClearCache ()

Detailed Description

Helper to find knapsack cover cuts.

Definition at line 457 of file cuts.h.

Constructor & Destructor Documentation

~CoverCutHelper()

operations_research::sat::CoverCutHelper::~CoverCutHelper

(

)

Definition at line 1055 of file cuts.cc.

Member Function Documentation

ClearCache()

void operations_research::sat::CoverCutHelper::ClearCache ( )

inline

Definition at line 514 of file cuts.h.

cut()

const CutData & operations_research::sat::CoverCutHelper::cut ( ) const

inline

If successful, info about the last generated cut.

Definition at line 507 of file cuts.h.

Info()

std::string operations_research::sat::CoverCutHelper::Info ( ) const

inline

Single line of text that we append to the cut log line.

Definition at line 510 of file cuts.h.

SetSharedStatistics()

void operations_research::sat::CoverCutHelper::SetSharedStatistics ( SharedStatistics * stats )

inline

Definition at line 512 of file cuts.h.

TrySimpleKnapsack()

bool operations_research::sat::CoverCutHelper::TrySimpleKnapsack	(	const CutData &	input_ct,
		ImpliedBoundsProcessor *	ib_processor = nullptr )

Try to find a cut with a knapsack heuristic. This assumes an input with all coefficients positive. If this returns true, you can get the cut via cut().

This uses a lifting procedure similar to what is described in "Lifting the Knapsack Cover Inequalities for the Knapsack Polytope", Adam N. Letchfod, Georgia Souli. In particular the section "Lifting via mixed-integer rounding".

Tricky: This only work because the cut absl128 rhs is not changed by these operations.

We only look at non-Boolean with an lp value not close to the upper bound.

If some implied bound substitution are possible, we do not cache anything currently because the logic is currently sighlty different betweent the two code. Fix?

The cut is just obtained by complementing the variable in the cover and applying the MIR super additive function.

Note

since all coeff in the cover will now be negative. If we do no scaling, and if we use max_coeff_in_cover to construct f(), they will be mapped by f() to -1 and we get the classical cover inequality. With scaling we can get a strictly dominating cut though.

Todo

(user): we don't have to pick max_coeff_in_cover and could use the coefficient of the most fractional variable. Or like in the MIR code try a few of them. Currently, the cut in the test is worse if we don't take the max_coeff_in_cover though, so we need more understanding.

Todo

(user): It seems we could use a more advanced lifting function described later in the paper. Investigate.

Todo

(user): Experiment without this line that basically disable scoring.

Todo

(user): experiment with different value of scaling and param t.

Update counters.

Definition at line 1293 of file cuts.cc.

TrySingleNodeFlow()

bool operations_research::sat::CoverCutHelper::TrySingleNodeFlow	(	const CutData &	input_ct,
		ImpliedBoundsProcessor *	ib_processor = nullptr )

It turns out that what FlowCoverCutHelper is doing is really just finding a cover and generating a cut via coefficient strenghtening instead of MIR rounding. This more generic version should just always outperform our old code.

Todo

(user): Change the heuristic to depends on the lp_value of the implied bounds. This way we can exactly match what happen in the old FlowCoverCutHelper.

After complementing the term in the cover, we have sum -ci.X + other_terms <= -slack;

We do not support complex terms, but we shouldn't get any.

The algorithm goes as follow:

• Compute heuristically a minimal cover.
• We have sum_cover ci.Xi >= slack where Xi is distance to upper bound.
• Apply coefficient strenghtening if ci > slack.

Using implied bound we have two cases (all coeffs positive): 1/ ci.Xi = ci.fi.Bi + ci.Si : always good. 2/ ci.Xi = ci.di.Bi - ci.Si <= di.Bi: good if Si lp_value is zero.

Note

if everything is Boolean, we just get a normal cover and coeff strengthening just result in all coeff at 1, so worse than our cover heuristic.

Todo

(user): Shouldn't we just use rounding f() with maximum coeff to allows lift of all other terms? but then except for the heuristic the cut is really similar to the cover cut.

Lifting.

Compute good period. We don't want to extend it in the simpler case where f(x)=-1 if x < 0.

Todo

(user): If the Mir*() function is used, we don't need to extend that much the period. Fix.

Todo

(user): do exact binary search to find highest x in [-max_neg_magnitude, 0] such that f(x) == f(-max_neg_magnitude) ? not really needed though since we know that we have this equality:

Generate the cut.

Definition at line 1408 of file cuts.cc.

TryWithLetchfordSouliLifting()

bool operations_research::sat::CoverCutHelper::TryWithLetchfordSouliLifting	(	const CutData &	input_ct,
		ImpliedBoundsProcessor *	ib_processor = nullptr )

Applies the lifting procedure described in "On Lifted Cover Inequalities: A New Lifting Procedure with Unusual Properties", Adam N. Letchford, Georgia Souli. This assumes an input with all coefficients positive.

The algo is pretty simple, given a cover C for a given rhs. We compute a rational weight p/q so that sum_C min(w_i, p/q) = rhs. Note that q is pretty small (lower or equal to the size of C). The generated cut is then of the form sum X_i in C for which w_i <= p / q

• sum gamma_i X_i for the other variable <= C - 1.

gamma_i being the smallest k such that w_i <= sum of the k + 1 largest min(w_i, p/q) for i in C. In particular, it is zero if w_i <= p/q.

Note

this accept a general constraint that has been canonicalized to sum coeff_i * X_i <= base_rhs. Each coeff_i >= 0 and each X_i >= 0.

Todo

(user): Generalize to non-Boolean, or use a different cover heuristic for this:

• We want a Boolean only cover currently.
• We can always use implied bound for this, since there is more chance for a Bool only cover.
• Also, f() should be super additive on the value <= rhs, i.e. f(a + b) >= f(a) + f(b), so it is always good to use implied bounds of the form X = bound * B + Slack.

We already called GetCoverSizeForBooleans() and ib_processor was nullptr, so reuse that info.

Perform IB expansion with no restriction, all coeff should still be positive.

Todo

(user): Merge Boolean terms that are complement of each other.

Todo

(user): we currently only deal with Boolean in the cover. Fix.

We don't support big rhs here. Note however than since this only deal with Booleans, it is less likely.

Collect the weight in the cover.

Compute the correct threshold so that if we round down larger weights to p/q. We have sum of the weight in cover == base_rhs.

Compute thresholds. For the first q values, thresholds[i] is the smallest integer such that q * threshold[i] > p * (i + 1).

Todo

(user): compute this in an overflow-safe way.

For the other values, we just add the weights.

Generate the cut.

Our algo is quadratic in worst case, but large coefficients should be rare, and in practice we don't really see this.

Note

this work for non-Boolean since we can just "theorically" split them as a sum of Booleans :) Probably a cleaner proof exist by just using the super-additivity of the lifting function on [0, rhs].

Find the largest index <= coeff.

Todo

(user): For exact multiple of p/q we can increase the coeff by 1/2. See section in the paper on getting maximal super additive function.

Definition at line 1512 of file cuts.cc.

---

The documentation for this class was generated from the following files:

• ortools/sat/cuts.h
• ortools/sat/cuts.cc