operations_research::sat::CutDataBuilder Class Reference

Stores temporaries used to build or manipulate a CutData. More...

#include <cuts.h>

Public Member Functions
bool	ConvertToLinearConstraint (const CutData &cut, LinearConstraint *output)
	Returns false if we encounter an integer overflow.
int	AddOrMergeBooleanTerms (absl::Span< CutTerm > terms, IntegerValue t, CutData *cut)

Detailed Description

Stores temporaries used to build or manipulate a CutData.

Definition at line 160 of file cuts.h.

Member Function Documentation

AddOrMergeBooleanTerms()

int operations_research::sat::CutDataBuilder::AddOrMergeBooleanTerms	(	absl::Span< CutTerm >	new_terms,
		IntegerValue	t,
		CutData *	cut )

These function allow to merges entries corresponding to the same variable and complementation. That is (X - lb) and (ub - X) are NOT merged and kept as separate terms. Note that we currently only merge Booleans since this is the only case we need.

Return num_merges.

We only deal with coeff * Bool or coeff * (1 - Bool)

Todo

(user): Because of merges, we might have entry with a coefficient of zero than are not useful. Remove them?

Fill the maps.

Loop over the cut now. Note that we loop with indices as we might add new terms in the middle of the loop.

We found a match, try to merge the map entry into the cut.

Note

we don't waste time erasing this entry from the map since we should have no duplicates in the original cut.

Finally add the terms we couldn't merge.

Definition at line 298 of file cuts.cc.

ConvertToLinearConstraint()

bool operations_research::sat::CutDataBuilder::ConvertToLinearConstraint	(	const CutData &	cut,
		LinearConstraint *	output )

Returns false if we encounter an integer overflow.

Todo

(user): Divide by gcd first to avoid possible overflow in the conversion? it is however unlikely given that our coeffs should be small.

Definition at line 351 of file cuts.cc.

---

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

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