#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 (const absl::flat_hash_map< IntegerVariable, glop::ColIndex > &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

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 247 of file implied_bounds.h.

Constructor & Destructor Documentation

◆ ProductDetector()

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

explicit

Definition at line 488 of file implied_bounds.cc.

◆ ~ProductDetector()

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

Definition at line 501 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 307 of file implied_bounds.h.

◆ GetProduct() [1/2]

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

Definition at line 691 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 640 of file implied_bounds.cc.

◆ InitializeBooleanRLTCuts()

void operations_research::sat::ProductDetector::InitializeBooleanRLTCuts	(	const absl::flat_hash_map< IntegerVariable, glop::ColIndex > &	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.

Definition at line 799 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 315 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 578 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 710 of file implied_bounds.cc.

◆ ProcessConditionalZero()

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

Definition at line 744 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 610 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 521 of file implied_bounds.cc.

◆ ProcessTernaryExactlyOne()

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

Definition at line 560 of file implied_bounds.cc.

◆ ProcessTrailAtLevelOne()

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

Definition at line 622 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 665 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

Public Member Functions