operations_research::sat::CutTerm Struct Reference

Detailed Description

To simplify cut generation code, we use a more complex data structure than just a LinearConstraint to represent a cut with shifted/complemented variable and implied bound substitution.

Definition at line 65 of file cuts.h.

#include <cuts.h>

Public Member Functions
bool	IsBoolean () const
bool	IsSimple () const
bool	HasRelevantLpValue () const
bool	IsFractional () const
double	LpDistToMaxValue () const
std::string	DebugString () const
void	Complement (absl::int128 *rhs)
void	ReplaceExpressionByLiteral (IntegerVariable var)
IntegerVariable	GetUnderlyingLiteralOrNone () const

Public Attributes
double	lp_value = 0.0
IntegerValue	coeff = IntegerValue(0)
IntegerValue	bound_diff = IntegerValue(0)
IntegerValue	expr_offset = IntegerValue(0)
std::array< IntegerVariable, 2 >	expr_vars
std::array< IntegerValue, 2 >	expr_coeffs
int	cached_implied_lb = -1
	Refer to cached_data_ in ImpliedBoundsProcessor.
int	cached_implied_ub = -1

Member Function Documentation

Complement()

void operations_research::sat::CutTerm::Complement

(

absl::int128 *

rhs

)

Do the subtitution X -> (1 - X') and update the rhs.

Our precondition on the sum of variable domains fitting an int64_t should ensure that this can never overflow.

We replace coeff * X by coeff * (X - bound_diff + bound_diff) which gives -coeff * complement(X) + coeff * bound_diff;

We keep the same expression variable.

Note

this is not involutive because of floating point error. Fix?

Swap the implied bound info.

Definition at line 84 of file cuts.cc.

DebugString()

std::string operations_research::sat::CutTerm::DebugString

(

)

const

Definition at line 68 of file cuts.cc.

GetUnderlyingLiteralOrNone()

IntegerVariable operations_research::sat::CutTerm::GetUnderlyingLiteralOrNone

(

)

const

If the term correspond to literal_view or (1 - literal_view) return the integer variable representation of that literal. Returns kNoIntegerVariable if this is not the case.

Definition at line 117 of file cuts.cc.

HasRelevantLpValue()

bool operations_research::sat::CutTerm::HasRelevantLpValue ( ) const

inline

Definition at line 68 of file cuts.h.

IsBoolean()

bool operations_research::sat::CutTerm::IsBoolean ( ) const

inline

Definition at line 66 of file cuts.h.

IsFractional()

bool operations_research::sat::CutTerm::IsFractional ( ) const

inline

Definition at line 69 of file cuts.h.

IsSimple()

bool operations_research::sat::CutTerm::IsSimple ( ) const

inline

Definition at line 67 of file cuts.h.

LpDistToMaxValue()

double operations_research::sat::CutTerm::LpDistToMaxValue ( ) const

inline

Definition at line 72 of file cuts.h.

ReplaceExpressionByLiteral()

void operations_research::sat::CutTerm::ReplaceExpressionByLiteral

(

IntegerVariable

var

)

This assumes bound_diff == 1. It replaces the inner expression by either var or 1 - var depending on the positiveness of var.

Definition at line 103 of file cuts.cc.

Member Data Documentation

bound_diff

IntegerValue operations_research::sat::CutTerm::bound_diff = IntegerValue(0)

Definition at line 97 of file cuts.h.

cached_implied_lb

int operations_research::sat::CutTerm::cached_implied_lb = -1

Refer to cached_data_ in ImpliedBoundsProcessor.

Definition at line 111 of file cuts.h.

cached_implied_ub

int operations_research::sat::CutTerm::cached_implied_ub = -1

Definition at line 112 of file cuts.h.

coeff

IntegerValue operations_research::sat::CutTerm::coeff = IntegerValue(0)

Definition at line 96 of file cuts.h.

expr_coeffs

std::array<IntegerValue, 2> operations_research::sat::CutTerm::expr_coeffs

Definition at line 108 of file cuts.h.

expr_offset

IntegerValue operations_research::sat::CutTerm::expr_offset = IntegerValue(0)

X = the given LinearExpression. We only support size 1 or 2 here which allow to inline the memory. When a coefficient is zero, we don't care about the variable.

Todo

(user): We might want to store that elsewhere, as sorting CutTerm is a bit slow and we don't need to look at that in most places. Same for the cached_implied_lb/ub below.

Definition at line 106 of file cuts.h.

expr_vars

std::array<IntegerVariable, 2> operations_research::sat::CutTerm::expr_vars

Definition at line 107 of file cuts.h.

lp_value

double operations_research::sat::CutTerm::lp_value = 0.0

Each term is of the form coeff * X where X is a variable with given lp_value and with a domain in [0, bound_diff]. Note X is always >= 0.

Definition at line 95 of file cuts.h.

---

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

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