Helper class to express a product as a linear constraint. More...

#include <implied_bounds.h>

Public Member Functions
	ProductDecomposer (Model *model)

std::vector< LiteralValueValue >	TryToDecompose (const AffineExpression &left, const AffineExpression &right)

bool	TryToLinearize (const AffineExpression &left, const AffineExpression &right, LinearConstraintBuilder *builder)

Detailed Description

Helper class to express a product as a linear constraint.

Definition at line 210 of file implied_bounds.h.

Constructor & Destructor Documentation

◆ ProductDecomposer()

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

inlineexplicit

Definition at line 212 of file implied_bounds.h.

Member Function Documentation

◆ TryToDecompose()

std::vector< LiteralValueValue > operations_research::sat::ProductDecomposer::TryToDecompose	(	const AffineExpression &	left,
		const AffineExpression &	right )

Tries to decompose a product left * right in a list of constant alternative left_value * right_value controlled by literals in an exactly one relationship. We construct this by using literals from the full encoding or element encodings of the variables of the two affine expressions. If it fails, it returns an empty vector.

Fill in the encodings for the left variable.

Fill in the encodings for the right variable.

Select the compatible encoding with the minimum index.

By construction, encodings follow the order of literals in the exactly_one constraint.

Build decomposition of the product.

Definition at line 347 of file implied_bounds.cc.

◆ TryToLinearize()

bool operations_research::sat::ProductDecomposer::TryToLinearize	(	const AffineExpression &	left,
		const AffineExpression &	right,
		LinearConstraintBuilder *	builder )

Looks at value encodings and detects if the product of two variables can be linearized.

On true, the builder will be cleared to contain the linearization. On false, it might be in an undefined state.

In the returned encoding, note that all the literals will be unique and in exactly one relation, and that the values can be duplicated. This is what we call an "element" encoding. The expressions will also be canonical.

Todo: (user): Experiment with x * x where constants = 0, x is fully encoded, and the domain is small.

Linearization is possible if both left and right have the same Boolean variable.

Definition at line 430 of file implied_bounds.cc.

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