#include <cp_model_mapping.h>

Public Member Functions
bool	IsBoolean (int ref) const

bool	IsInteger (int ref) const

sat::Literal	Literal (int ref) const

IntegerVariable	Integer (int ref) const

AffineExpression	Affine (const LinearExpressionProto &exp) const

IntervalVariable	Interval (int i) const

template<typename List >
std::vector< IntegerVariable >	Integers (const List &list) const

template<typename ProtoIndices >
std::vector< sat::Literal >	Literals (const ProtoIndices &indices) const

template<typename List >
std::vector< AffineExpression >	Affines (const List &list) const

template<typename ProtoIndices >
std::vector< IntervalVariable >	Intervals (const ProtoIndices &indices) const

bool	ConstraintIsAlreadyLoaded (const ConstraintProto *ct) const

bool	IsHalfEncodingConstraint (const ConstraintProto *ct) const

int	GetProtoVariableFromBooleanVariable (BooleanVariable var) const

int	GetProtoVariableFromIntegerVariable (IntegerVariable var) const

const std::vector< IntegerVariable > &	GetVariableMapping () const

LinearExpression	GetExprFromProto (const LinearExpressionProto &expr_proto) const

int	NumIntegerVariables () const
	For logging only, these are not super efficient.

int	NumBooleanVariables () const

int	NumProtoVariables () const
	Returns the number of variables in the loaded proto.

Friends
void	LoadVariables (const CpModelProto &model_proto, bool view_all_booleans_as_integers, Model *m)

void	ExtractEncoding (const CpModelProto &model_proto, Model *m)

Detailed Description

Holds the mapping between CpModel proto indices and the sat::model ones.

This also holds some information used when loading a CpModel proto.

Definition at line 71 of file cp_model_mapping.h.

Member Function Documentation

◆ Affine()

AffineExpression operations_research::sat::CpModelMapping::Affine ( const LinearExpressionProto & exp ) const

inline

Todo: (user): We could "easily" create an intermediate variable for more complex linear expression. We could also identify duplicate expressions to not create two identical integer variable.

Definition at line 100 of file cp_model_mapping.h.

◆ Affines()

template<typename List >

std::vector< AffineExpression > operations_research::sat::CpModelMapping::Affines ( const List & list ) const

inline

Definition at line 133 of file cp_model_mapping.h.

◆ ConstraintIsAlreadyLoaded()

bool operations_research::sat::CpModelMapping::ConstraintIsAlreadyLoaded ( const ConstraintProto * ct ) const

inline

Depending on the option, we will load constraints in stages. This is used to detect constraints that are already loaded. For instance the interval constraints and the linear constraint of size 1 (encodings) are usually loaded first.

Definition at line 152 of file cp_model_mapping.h.

◆ GetExprFromProto()

LinearExpression operations_research::sat::CpModelMapping::GetExprFromProto ( const LinearExpressionProto & expr_proto ) const

inline

Definition at line 179 of file cp_model_mapping.h.

◆ GetProtoVariableFromBooleanVariable()

int operations_research::sat::CpModelMapping::GetProtoVariableFromBooleanVariable ( BooleanVariable var ) const

inline

Note: both these functions returns positive reference or -1.

Definition at line 166 of file cp_model_mapping.h.

◆ GetProtoVariableFromIntegerVariable()

int operations_research::sat::CpModelMapping::GetProtoVariableFromIntegerVariable ( IntegerVariable var ) const

inline

Definition at line 170 of file cp_model_mapping.h.

◆ GetVariableMapping()

const std::vector< IntegerVariable > & operations_research::sat::CpModelMapping::GetVariableMapping ( ) const

inline

Definition at line 175 of file cp_model_mapping.h.

◆ Integer()

IntegerVariable operations_research::sat::CpModelMapping::Integer ( int ref ) const

inline

Definition at line 91 of file cp_model_mapping.h.

◆ Integers()

template<typename List >

std::vector< IntegerVariable > operations_research::sat::CpModelMapping::Integers ( const List & list ) const

inline

Definition at line 117 of file cp_model_mapping.h.

◆ Interval()

IntervalVariable operations_research::sat::CpModelMapping::Interval ( int i ) const

inline

Definition at line 109 of file cp_model_mapping.h.

◆ Intervals()

template<typename ProtoIndices >

std::vector< IntervalVariable > operations_research::sat::CpModelMapping::Intervals ( const ProtoIndices & indices ) const

inline

Definition at line 141 of file cp_model_mapping.h.

◆ IsBoolean()

bool operations_research::sat::CpModelMapping::IsBoolean ( int ref ) const

inline

Returns true if the given CpModelProto variable reference refers to a Boolean variable. Such variable will always have an associated Literal(), but not always an associated Integer().

Definition at line 76 of file cp_model_mapping.h.

◆ IsHalfEncodingConstraint()

bool operations_research::sat::CpModelMapping::IsHalfEncodingConstraint ( const ConstraintProto * ct ) const

inline

Returns true if the given constraint is a "half-encoding" constraint. That is, if it is of the form (b => size 1 linear) but there is no (<=) side in the model. Such constraint are detected while we extract integer encoding and are cached here so that we can deal properly with them during the linear relaxation.

Definition at line 161 of file cp_model_mapping.h.

◆ IsInteger()

bool operations_research::sat::CpModelMapping::IsInteger ( int ref ) const

inline

Definition at line 81 of file cp_model_mapping.h.

◆ Literal()

sat::Literal operations_research::sat::CpModelMapping::Literal ( int ref ) const

inline

Definition at line 86 of file cp_model_mapping.h.

◆ Literals()

template<typename ProtoIndices >

std::vector< sat::Literal > operations_research::sat::CpModelMapping::Literals ( const ProtoIndices & indices ) const

inline

Definition at line 125 of file cp_model_mapping.h.

◆ NumBooleanVariables()

int operations_research::sat::CpModelMapping::NumBooleanVariables ( ) const

inline

Definition at line 198 of file cp_model_mapping.h.

◆ NumIntegerVariables()

int operations_research::sat::CpModelMapping::NumIntegerVariables ( ) const

inline

For logging only, these are not super efficient.

Definition at line 191 of file cp_model_mapping.h.

◆ NumProtoVariables()

int operations_research::sat::CpModelMapping::NumProtoVariables ( ) const

inline

Returns the number of variables in the loaded proto.

Definition at line 207 of file cp_model_mapping.h.

Friends And Related Symbol Documentation

◆ ExtractEncoding

void ExtractEncoding	(	const CpModelProto &	model_proto,
		Model *	m )

friend

The logic assumes that the linear constraints have been presolved, so that equality with a domain bound have been converted to <= or >= and so that we never have any trivial inequalities.

Todo: (user): Regroup/presolve two encoding like b => x > 2 and the same Boolean b => x > 5. These shouldn't happen if we merge linear constraints.

Extract the encodings (IntegerVariable <-> Booleans) present in the model. This effectively load some linear constraints of size 1 that will be marked as already loaded.

Todo: (user): Debug what makes it unsat at this point.

Detection of literal equivalent to (i_var == value). We collect all the half-reified constraint lit => equality or lit => inequality for a given variable, and we will later sort them to detect equivalence.

Todo: (user): We will re-add the same implied bounds during probing, so it might not be necessary to do that here. Also, it might be too early if some of the literal view used in the LP are created later, but that should be fixable via calls to implied_bounds->NotifyNewIntegerView().

Detection of literal equivalent to (i_var >= bound). We also collect all the half-refied part and we will sort the vector for detection of the equivalence.

Loop over all constraints and fill var_to_equalities and inequalities.

ct is a linear constraint with one term and one enforcement literal.

Detect enforcement_literal => (var >= value or var <= value).

Detect implied bounds. The test is less strict than the above test.

Detect enforcement_literal => (var == value or var != value).

Note: for domain with 2 values like [0, 1], we will detect both == 0 and != 1. Similarly, for a domain in [min, max], we should both detect (== min) and (<= min), and both detect (== max) and (>= max).

Detect Literal <=> X >= value

Todo: (user): In these cases, we could fix the enforcement literal right away or ignore the constraint. Note that it will be done later anyway though.

Encode the half-inequalities.

Detect Literal <=> X == value and associate them in the IntegerEncoder.

Todo: (user): Fully encode variable that are almost fully encoded?

Todo: (user): Try to remove it. Normally we caught UNSAT above, but tests are very flaky (it only happens in parallel). Keeping it there for the time being.

Encode the half-equalities.

Todo: (user): delay this after PropagateEncodingFromEquivalenceRelations()? Otherwise we might create new Boolean variables for no reason. Note however, that in the presolve, we should only use the "representative" in linear constraints, so we should be fine.

If we have just an half-equality, lets not create the <=> literal but just add two implications. If we don't create hole, we don't really need the reverse literal. This way it is also possible for the ExtractElementEncoding() to detect later that actually this literal is <=> to var == value, and this way we create one less Boolean for the same result.

Todo: (user): It is not 100% clear what is the best encoding and if we should create equivalent literal or rely on propagator instead to push bounds.

Update stats.

Definition at line 396 of file cp_model_loader.cc.

◆ LoadVariables

void LoadVariables	(	const CpModelProto &	model_proto,
		bool	view_all_booleans_as_integers,
		Model *	m )

friend

Extracts all the used variables in the CpModelProto and creates a sat::Model representation for them. More precisely

All Boolean variables will be mapped.
All Interval variables will be mapped.
All non-Boolean variable will have a corresponding IntegerVariable, and depending on the view_all_booleans_as_integers, some or all of the BooleanVariable will also have an IntegerVariable corresponding to its "integer view".

Note(user): We could create IntegerVariable on the fly as they are needed, but that loose the original variable order which might be useful in heuristics later.

All [0, 1] variables always have a corresponding Boolean, even if it is fixed to 0 (domain == [0,0]) or fixed to 1 (domain == [1,1]).

Compute the list of positive variable reference for which we need to create an IntegerVariable.

Compute the integer variable references used by the model.

We always add a linear relaxation for circuit/route except for linearization level zero.

Add the objectives variables that needs to be referenceable as integer even if they are only used as Booleans.

Make sure any unused variable, that is not already a Boolean is considered "used".

We want the variable in the problem order.

It is important for memory usage to reserve tight vector has we have many indexed by IntegerVariable. Unfortunately, we create intermediate IntegerVariable while loading large linear constraint, or when we have disjoint LP component. So this is a best effort at a tight upper bound.

Link any variable that has both views.

Associate with corresponding integer variable.

Create the interval variables.

Todo: (user): Fix the constant variable situation. An optional interval with constant start/end or size cannot share the same constant variable if it is used in non-optional situation.

Definition at line 126 of file cp_model_loader.cc.

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

ortools/sat/cp_model_mapping.h

Public Member Functions

Friends

Detailed Description

Member Function Documentation

◆ Affine()

◆ Affines()

◆ ConstraintIsAlreadyLoaded()

◆ GetExprFromProto()

◆ GetProtoVariableFromBooleanVariable()

◆ GetProtoVariableFromIntegerVariable()

◆ GetVariableMapping()

◆ Integer()

◆ Integers()

◆ Interval()

◆ Intervals()

◆ IsBoolean()

◆ IsHalfEncodingConstraint()

◆ IsInteger()

◆ Literal()

◆ Literals()

◆ NumBooleanVariables()

◆ NumIntegerVariables()

◆ NumProtoVariables()

Friends And Related Symbol Documentation

◆ ExtractEncoding

◆ LoadVariables