Our cut are always of the form linear_expression <= rhs. More...

Detailed Description

Our cut are always of the form linear_expression <= rhs.

Definition at line 116 of file cuts.h.

#include <cuts.h>

Public Member Functions
bool	FillFromLinearConstraint (const LinearConstraint &base_ct, const util_intops::StrongVector< IntegerVariable, double > &lp_values, IntegerTrail *integer_trail)
bool	FillFromParallelVectors (IntegerValue ub, absl::Span< const IntegerVariable > vars, absl::Span< const IntegerValue > coeffs, absl::Span< const double > lp_values, absl::Span< const IntegerValue > lower_bounds, absl::Span< const IntegerValue > upper_bounds)
bool	AppendOneTerm (IntegerVariable var, IntegerValue coeff, double lp_value, IntegerValue lb, IntegerValue ub)
bool	AllCoefficientsArePositive () const
	These functions transform the cut by complementation.
void	ComplementForPositiveCoefficients ()
void	ComplementForSmallerLpValues ()
double	ComputeViolation () const
	Computes and returns the cut violation.
double	ComputeEfficacy () const
void	SortRelevantEntries ()
std::string	DebugString () const

Public Attributes
absl::int128	rhs
std::vector< CutTerm >	terms
IntegerValue	max_magnitude
	Only filled after SortRelevantEntries().
int	num_relevant_entries

Member Function Documentation

◆ AllCoefficientsArePositive()

bool operations_research::sat::CutData::AllCoefficientsArePositive ( ) const

These functions transform the cut by complementation.

Definition at line 232 of file cuts.cc.

◆ AppendOneTerm()

bool operations_research::sat::CutData::AppendOneTerm	(	IntegerVariable	var,
		IntegerValue	coeff,
		double	lp_value,
		IntegerValue	lb,
		IntegerValue	ub )

To try to minimize the risk of overflow, we switch to the bound closer to the lp_value. Since most of our base constraint for cut are tight, hopefully this is not too bad.

Complement the variable so that it is has a positive coefficient.

See formula below, the constant term is either coeff * lb or coeff * ub.

Deal with fixed variable, no need to shift back in this case, we can just remove the term.

X = -(UB - X) + UB

C = (X - LB) + LB

Definition at line 137 of file cuts.cc.

◆ ComplementForPositiveCoefficients()

void operations_research::sat::CutData::ComplementForPositiveCoefficients ( )

Definition at line 218 of file cuts.cc.

◆ ComplementForSmallerLpValues()

void operations_research::sat::CutData::ComplementForSmallerLpValues ( )

Definition at line 225 of file cuts.cc.

◆ ComputeEfficacy()

double operations_research::sat::CutData::ComputeEfficacy ( ) const

Definition at line 265 of file cuts.cc.

◆ ComputeViolation()

double operations_research::sat::CutData::ComputeViolation ( ) const

Computes and returns the cut violation.

Definition at line 257 of file cuts.cc.

◆ DebugString()

std::string operations_research::sat::CutData::DebugString ( ) const

Definition at line 76 of file cuts.cc.

◆ FillFromLinearConstraint()

bool operations_research::sat::CutData::FillFromLinearConstraint	(	const LinearConstraint &	base_ct,
		const util_intops::StrongVector< IntegerVariable, double > &	lp_values,
		IntegerTrail *	integer_trail )

We need level zero bounds and LP relaxation values to fill a CutData. Returns false if we encounter any integer overflow.

Definition at line 174 of file cuts.cc.

◆ FillFromParallelVectors()

bool operations_research::sat::CutData::FillFromParallelVectors	(	IntegerValue	ub,
		absl::Span< const IntegerVariable >	vars,
		absl::Span< const IntegerValue >	coeffs,
		absl::Span< const double >	lp_values,
		absl::Span< const IntegerValue >	lower_bounds,
		absl::Span< const IntegerValue >	upper_bounds )

Definition at line 192 of file cuts.cc.

◆ SortRelevantEntries()

void operations_research::sat::CutData::SortRelevantEntries ( )

This sorts terms by decreasing lp values and fills both num_relevant_entries and max_magnitude.

Sort by larger lp_value first.

Definition at line 239 of file cuts.cc.

Member Data Documentation

◆ max_magnitude

IntegerValue operations_research::sat::CutData::max_magnitude

Only filled after SortRelevantEntries().

Definition at line 155 of file cuts.h.

◆ num_relevant_entries

int operations_research::sat::CutData::num_relevant_entries

Definition at line 156 of file cuts.h.

◆ rhs

absl::int128 operations_research::sat::CutData::rhs

Note: we use a 128 bit rhs so we can freely complement variable without running into overflow.

Definition at line 151 of file cuts.h.

◆ terms

std::vector<CutTerm> operations_research::sat::CutData::terms

Definition at line 152 of file cuts.h.

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

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