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

#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

std::string	DebugString () const

void	Canonicalize ()
	This sorts terms and fill both num_relevant_entries and max_magnitude.

Public Attributes
absl::int128	rhs

std::vector< CutTerm >	terms

IntegerValue	max_magnitude

int	num_relevant_entries

Detailed Description

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

Definition at line 110 of file cuts.h.

Member Function Documentation

◆ AllCoefficientsArePositive()

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

These functions transform the cut by complementation.

Definition at line 228 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 133 of file cuts.cc.

◆ Canonicalize()

void operations_research::sat::CutData::Canonicalize ( )

This sorts terms and fill both num_relevant_entries and max_magnitude.

Sort by larger lp_value first.

Definition at line 235 of file cuts.cc.

◆ ComplementForPositiveCoefficients()

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

Definition at line 214 of file cuts.cc.

◆ ComplementForSmallerLpValues()

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

Definition at line 221 of file cuts.cc.

◆ ComputeEfficacy()

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

Definition at line 262 of file cuts.cc.

◆ ComputeViolation()

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

Computes and returns the cut violation.

Definition at line 254 of file cuts.cc.

◆ DebugString()

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

Definition at line 72 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 170 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 188 of file cuts.cc.

Member Data Documentation

◆ max_magnitude

IntegerValue operations_research::sat::CutData::max_magnitude

Definition at line 146 of file cuts.h.

◆ num_relevant_entries

int operations_research::sat::CutData::num_relevant_entries

Definition at line 147 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 141 of file cuts.h.

◆ terms

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

Definition at line 142 of file cuts.h.

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

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

Public Member Functions

Public Attributes