Detailed Description

Class used to detect and hold all the information about a variable beeing the product of two others. This class is meant to be used by LP relaxation and cuts.

Definition at line 246 of file implied_bounds.h.

#include <implied_bounds.h>

Public Member Functions
	ProductDetector (Model *model)
	~ProductDetector ()
void	ProcessTernaryClause (absl::Span< const Literal > ternary_clause)
void	ProcessTernaryExactlyOne (absl::Span< const Literal > ternary_exo)
void	ProcessBinaryClause (absl::Span< const Literal > binary_clause)
void	ProcessImplicationGraph (BinaryImplicationGraph *graph)
	Utility function to process a bunch of implication all at once.
void	ProcessTrailAtLevelOne ()
void	ProcessConditionalEquality (Literal l, IntegerVariable x, IntegerVariable y)
void	ProcessConditionalZero (Literal l, IntegerVariable p)
LiteralIndex	GetProduct (Literal a, Literal b) const
	Query function mainly used for testing.
IntegerVariable	GetProduct (Literal a, IntegerVariable b) const
bool	ProductIsLinearizable (IntegerVariable a, IntegerVariable b) const
LinearExpression	LinearizeProduct (IntegerVariable a, IntegerVariable b)
LinearExpression	ProductLowerBound (IntegerVariable a, IntegerVariable b)
void	InitializeBooleanRLTCuts (absl::Span< const IntegerVariable > lp_vars, const util_intops::StrongVector< IntegerVariable, double > &lp_values)
const absl::flat_hash_map< IntegerVariable, std::vector< IntegerVariable > > &	BoolRLTCandidates () const
IntegerVariable	LiteralProductUpperBound (IntegerVariable a, IntegerVariable b) const

Constructor & Destructor Documentation

◆ ProductDetector()

operations_research::sat::ProductDetector::ProductDetector ( Model * model )

explicit

Definition at line 490 of file implied_bounds.cc.

◆ ~ProductDetector()

operations_research::sat::ProductDetector::~ProductDetector ( )

Definition at line 503 of file implied_bounds.cc.

Member Function Documentation

◆ BoolRLTCandidates()

const absl::flat_hash_map< IntegerVariable, std::vector< IntegerVariable > > & operations_research::sat::ProductDetector::BoolRLTCandidates ( ) const

inline

BoolRLTCandidates()[var] contains the list of factor for which we have a violated upper bound on lit(var) * lit(factor).

Definition at line 306 of file implied_bounds.h.

◆ GetProduct() [1/2]

IntegerVariable operations_research::sat::ProductDetector::GetProduct	(	Literal	a,
		IntegerVariable	b ) const

Definition at line 693 of file implied_bounds.cc.

◆ GetProduct() [2/2]

LiteralIndex operations_research::sat::ProductDetector::GetProduct	(	Literal	a,
		Literal	b ) const

Query function mainly used for testing.

Definition at line 642 of file implied_bounds.cc.

◆ InitializeBooleanRLTCuts()

void operations_research::sat::ProductDetector::InitializeBooleanRLTCuts	(	absl::Span< const IntegerVariable >	lp_vars,
		const util_intops::StrongVector< IntegerVariable, double > &	lp_values )

Experimental. Find violated inequality of the form l1 * l2 <= l3. And set-up data structure to query this efficiently.

Todo: (user): limit work if too many ternary.

Todo: (user): Maybe we shouldn't reconstruct this every time, but it is hard in case of multiple lps to make sure we don't use variables not in the lp otherwise.

If we transform a linear constraint to sum positive_coeff * bool <= rhs. We will list all interesting multiplicative candidate for each variable.

If we have l1 + l2 + l3 >= 1, then for all (i, j) pair we have !li * !lj <= lk. We are looking for violation like this.

Clear.

Todo: (user): Just switch to memclear() when dense.

Definition at line 801 of file implied_bounds.cc.

◆ LinearizeProduct()

LinearExpression operations_research::sat::ProductDetector::LinearizeProduct	(	IntegerVariable	a,
		IntegerVariable	b )

Todo: (user): Implement!

◆ LiteralProductUpperBound()

IntegerVariable operations_research::sat::ProductDetector::LiteralProductUpperBound	(	IntegerVariable	a,
		IntegerVariable	b ) const

inline

Returns if it exists an integer variable u such that lit(a) * lit(b) <= lit(u). All integer variable must be boolean, a positive variable means positive literal, and a negative variable means negative literal. Returns kNoIntegerVariable if there are none.

Definition at line 314 of file implied_bounds.h.

◆ ProcessBinaryClause()

void operations_research::sat::ProductDetector::ProcessBinaryClause ( absl::Span< const Literal > binary_clause )

Todo: (user): As product are discovered, we could remove entries from our hash maps!

Definition at line 580 of file implied_bounds.cc.

◆ ProcessConditionalEquality()

void operations_research::sat::ProductDetector::ProcessConditionalEquality	(	Literal	l,
		IntegerVariable	x,
		IntegerVariable	y )

We also detect product of Boolean with IntegerVariable. After presolve, a product P = l * X should be encoded with: l => P = X not(l) => P = 0

Todo: (user): Generalize to a * X + b = l * (Y + c) since these are also easy to linearize if we see l * Y.

We process both possibilities (product = x or product = y).

Todo: (user): Linear scan can be bad if b => X = many other variables. Hopefully this will not be common.

Definition at line 712 of file implied_bounds.cc.

◆ ProcessConditionalZero()

void operations_research::sat::ProductDetector::ProcessConditionalZero	(	Literal	l,
		IntegerVariable	p )

Definition at line 746 of file implied_bounds.cc.

◆ ProcessImplicationGraph()

void operations_research::sat::ProductDetector::ProcessImplicationGraph ( BinaryImplicationGraph * graph )

Utility function to process a bunch of implication all at once.

Definition at line 612 of file implied_bounds.cc.

◆ ProcessTernaryClause()

void operations_research::sat::ProductDetector::ProcessTernaryClause ( absl::Span< const Literal > ternary_clause )

Internally, a Boolean product is encoded in a linear fashion: p = a * b become: 1/ a and b => p, i.e. a clause (not(a), not(b), p). 2/ p => a and p => b, which is a clause (not(p), a) and (not(p), b).

In particular if we have a+b+c==1 then we have a=b*c, b=a*c, and c=a*b !!

For the detection to work, we must load all ternary clause first, then the implication.

We mark the literal of the ternary clause as seen. Only a => b with a seen need to be looked at.

Definition at line 523 of file implied_bounds.cc.

◆ ProcessTernaryExactlyOne()

void operations_research::sat::ProductDetector::ProcessTernaryExactlyOne ( absl::Span< const Literal > ternary_exo )

Definition at line 562 of file implied_bounds.cc.

◆ ProcessTrailAtLevelOne()

void operations_research::sat::ProductDetector::ProcessTrailAtLevelOne ( )

Definition at line 624 of file implied_bounds.cc.

◆ ProductIsLinearizable()

bool operations_research::sat::ProductDetector::ProductIsLinearizable	(	IntegerVariable	a,
		IntegerVariable	b ) const

Query Functions. LinearizeProduct() should only be called if ProductIsLinearizable() is true.

Otherwise, we need both a and b to be expressible as linear expression involving Booleans whose product is also expressible.

Any product involving la/not(la) * lb/not(lb) can be used.

Definition at line 667 of file implied_bounds.cc.

◆ ProductLowerBound()

LinearExpression operations_research::sat::ProductDetector::ProductLowerBound	(	IntegerVariable	a,
		IntegerVariable	b )

Returns an expression that is always lower or equal to the product a * b. This use the exact LinearizeProduct() if ProductIsLinearizable() otherwise it uses the simple McCormick lower bound.

Todo: (user): Implement!

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

ortools/sat/implied_bounds.h
ortools/sat/implied_bounds.cc