#include <integer.h>

Public Member Functions
	IntegerEncoder (Model *model)

	IntegerEncoder (const IntegerEncoder &)=delete
	This type is neither copyable nor movable.

IntegerEncoder &	operator= (const IntegerEncoder &)=delete

	~IntegerEncoder ()

void	ReserveSpaceForNumVariables (int num_vars)
	Memory optimization: you can call this before encoding variables.

void	FullyEncodeVariable (IntegerVariable var)

bool	VariableIsFullyEncoded (IntegerVariable var) const

const std::vector< ValueLiteralPair > &	FullDomainEncoding (IntegerVariable var) const

const std::vector< ValueLiteralPair > &	PartialDomainEncoding (IntegerVariable var) const

std::pair< IntegerLiteral, IntegerLiteral >	Canonicalize (IntegerLiteral i_lit) const

Literal	GetOrCreateAssociatedLiteral (IntegerLiteral i_lit)

Literal	GetOrCreateLiteralAssociatedToEquality (IntegerVariable var, IntegerValue value)

void	AssociateToIntegerLiteral (Literal literal, IntegerLiteral i_lit)

void	AssociateToIntegerEqualValue (Literal literal, IntegerVariable var, IntegerValue value)

bool	IsFixedOrHasAssociatedLiteral (IntegerLiteral i_lit) const

LiteralIndex	GetAssociatedLiteral (IntegerLiteral i_lit) const

LiteralIndex	GetAssociatedEqualityLiteral (IntegerVariable var, IntegerValue value) const

void	DisableImplicationBetweenLiteral ()

void	AddAllImplicationsBetweenAssociatedLiterals ()

const InlinedIntegerLiteralVector &	GetIntegerLiterals (Literal lit) const
	Returns the IntegerLiterals that were associated with the given Literal.

const InlinedIntegerValueVector &	GetEqualityLiterals (Literal lit) const

const std::vector< IntegerVariable > &	GetAllAssociatedVariables (Literal lit) const

IntegerVariable	GetLiteralView (Literal lit) const

ABSL_MUST_USE_RESULT bool	LiteralOrNegationHasView (Literal lit, IntegerVariable view=nullptr, bool view_is_direct=nullptr) const

LiteralIndex	SearchForLiteralAtOrBefore (IntegerLiteral i_lit, IntegerValue *bound) const

Literal	GetTrueLiteral ()
	Gets the literal always set to true, make it if it does not exist.

Literal	GetFalseLiteral ()

std::vector< ValueLiteralPair >	PartialGreaterThanEncoding (IntegerVariable var) const

bool	UpdateEncodingOnInitialDomainChange (IntegerVariable var, Domain domain)

Detailed Description

Each integer variable x will be associated with a set of literals encoding (x >= v) for some values of v. This class maintains the relationship between the integer variables and such literals which can be created by a call to CreateAssociatedLiteral().

The advantage of creating such Boolean variables is that the SatSolver which is driving the search can then take this variable as a decision and maintain these variables activity and so on. These variables can also be propagated directly by the learned clauses.

This class also support a non-lazy full domain encoding which will create one literal per possible value in the domain. See FullyEncodeVariable(). This is meant to be called by constraints that directly work on the variable values like a table constraint or an all-diff constraint.

Todo: (user): We could also lazily create precedences Booleans between two arbitrary IntegerVariable. This is better done in the PrecedencesPropagator though.

Definition at line 471 of file integer.h.

Constructor & Destructor Documentation

◆ IntegerEncoder() [1/2]

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

inlineexplicit

Definition at line 473 of file integer.h.

◆ IntegerEncoder() [2/2]

operations_research::sat::IntegerEncoder::IntegerEncoder ( const IntegerEncoder & )

delete

This type is neither copyable nor movable.

◆ ~IntegerEncoder()

operations_research::sat::IntegerEncoder::~IntegerEncoder ( )

inline

Definition at line 484 of file integer.h.

Member Function Documentation

◆ AddAllImplicationsBetweenAssociatedLiterals()

void operations_research::sat::IntegerEncoder::AddAllImplicationsBetweenAssociatedLiterals ( )

This is tricky: AddBinaryClause() might trigger propagation that causes the encoding to be filtered. So we make a copy...

literal => previous.

Definition at line 226 of file integer.cc.

◆ AssociateToIntegerEqualValue()

void operations_research::sat::IntegerEncoder::AssociateToIntegerEqualValue	(	Literal	literal,
		IntegerVariable	var,
		IntegerValue	value )

The function is symmetric and we only deal with positive variable.

Detect literal view. Note that the same literal can be associated to more than one variable, and thus already have a view. We don't change it in this case.

We use the "do not insert if present" behavior of .insert() to do just one lookup.

If this key is already associated, make the two literals equal.

Fix literal for value outside the domain.

Update equality_by_var. Note that due to the equality_to_associated_literal_ hash table, there should never be any duplicate values for a given variable.

Fix literal for constant domain.

Special case for the first and last value.

Note: this will recursively call AssociateToIntegerEqualValue() but since equality_to_associated_literal_[] is now set, the recursion will stop there. When a domain has just 2 values, this allows to call just once AssociateToIntegerEqualValue() and also associate the other value to the negation of the given literal.

(var == value) <=> (var >= value) and (var <= value).

Update reverse encoding.

Definition at line 434 of file integer.cc.

◆ AssociateToIntegerLiteral()

void operations_research::sat::IntegerEncoder::AssociateToIntegerLiteral	(	Literal	literal,
		IntegerLiteral	i_lit )

Associates the Boolean literal to (X >= bound) or (X == value). If a literal was already associated to this fact, this will add an equality constraints between both literals. If the fact is trivially true or false, this will fix the given literal.

Always transform to positive variable.

We just insert the part corresponding to the literal with positive variable.

Corner case if adding implication cause this to be fixed.

Resize reverse encoding.

Detect the case >= max or <= min and properly register them. Note that both cases will happen at the same time if there is just two possible value in the domain.

Definition at line 364 of file integer.cc.

◆ Canonicalize()

std::pair< IntegerLiteral, IntegerLiteral > operations_research::sat::IntegerEncoder::Canonicalize ( IntegerLiteral i_lit ) const

Returns the "canonical" (i_lit, negation of i_lit) pair. This mainly deal with domain with initial hole like [1,2][5,6] so that if one ask for x <= 3, this get canonicalized in the pair (x <= 2, x >= 5).

Note: it is an error to call this with a literal that is trivially true or trivially false according to the initial variable domain. This is CHECKed to make sure we don't create wasteful literal.

Todo: (user): This is linear in the domain "complexity", we can do better if needed.

Definition at line 246 of file integer.cc.

◆ DisableImplicationBetweenLiteral()

void operations_research::sat::IntegerEncoder::DisableImplicationBetweenLiteral ( )

inline

Advanced usage. It is more efficient to create the associated literals in order, but it might be anoying to do so. Instead, you can first call DisableImplicationBetweenLiteral() and when you are done creating all the associated literals, you can call (only at level zero) AddAllImplicationsBetweenAssociatedLiterals() which will also turn back on the implications between literals for the one that will be added afterwards.

Definition at line 580 of file integer.h.

◆ FullDomainEncoding()

const std::vector< ValueLiteralPair > & operations_research::sat::IntegerEncoder::FullDomainEncoding ( IntegerVariable var ) const

Returns the list of literal <=> var == value currently associated to the given variable. The result is sorted by value. We filter literal at false, and if a literal is true, then you will get a singleton. To be sure to get the full set of encoded value, then you should call this at level zero.

The FullDomainEncoding() just check VariableIsFullyEncoded() and returns the same result.

Warning: The reference returned is only valid until the next call to one of these functions.

Definition at line 145 of file integer.cc.

◆ FullyEncodeVariable()

void operations_research::sat::IntegerEncoder::FullyEncodeVariable ( IntegerVariable var )

Fully encode a variable using its current initial domain. If the variable is already fully encoded, this does nothing.

This creates new Booleans variables as needed: 1) num_values for the literals X == value. Except when there is just two value in which case only one variable is created. 2) num_values - 3 for the literals X >= value or X <= value (using their negation). The -3 comes from the fact that we can reuse the equality literals for the two extreme points.

The encoding for NegationOf(var) is automatically created too. It reuses the same Boolean variable as the encoding of var.

Todo: (user): It is currently only possible to call that at the decision level zero because we cannot add ternary clause in the middle of the search (for now). This is Checked.

Todo: (user): Maybe we can optimize the literal creation order and their polarity as our default SAT heuristics initially depends on this.

Todo: (user): Currently, in some corner cases, GetOrCreateLiteralAssociatedToEquality() might trigger some propagation that update the domain of var, so we need to cache the values to not read garbage. Note that it is okay to call the function on values no longer reachable, as this will just do nothing.

Mark var and Negation(var) as fully encoded.

Definition at line 79 of file integer.cc.

◆ GetAllAssociatedVariables()

const std::vector< IntegerVariable > & operations_research::sat::IntegerEncoder::GetAllAssociatedVariables ( Literal lit ) const

inline

Returns all the variables for which this literal is associated to either var >= value or var == value.

Definition at line 602 of file integer.h.

◆ GetAssociatedEqualityLiteral()

LiteralIndex operations_research::sat::IntegerEncoder::GetAssociatedEqualityLiteral	(	IntegerVariable	var,
		IntegerValue	value ) const

Definition at line 317 of file integer.cc.

◆ GetAssociatedLiteral()

LiteralIndex operations_research::sat::IntegerEncoder::GetAssociatedLiteral ( IntegerLiteral i_lit ) const

Todo: (user): Canonicalization might be slow.

Definition at line 540 of file integer.cc.

◆ GetEqualityLiterals()

const InlinedIntegerValueVector & operations_research::sat::IntegerEncoder::GetEqualityLiterals ( Literal lit ) const

inline

Returns the variable == value pairs that were associated with the given Literal. Note that only positive IntegerVariable appears here.

Definition at line 593 of file integer.h.

◆ GetFalseLiteral()

Literal operations_research::sat::IntegerEncoder::GetFalseLiteral ( )

inline

Definition at line 654 of file integer.h.

◆ GetIntegerLiterals()

const InlinedIntegerLiteralVector & operations_research::sat::IntegerEncoder::GetIntegerLiterals ( Literal lit ) const

inline

Returns the IntegerLiterals that were associated with the given Literal.

Definition at line 584 of file integer.h.

◆ GetLiteralView()

IntegerVariable operations_research::sat::IntegerEncoder::GetLiteralView ( Literal lit ) const

inline

If it exists, returns a [0,1] integer variable which is equal to 1 iff the given literal is true. Returns kNoIntegerVariable if such variable does not exist. Note that one can create one by creating a new IntegerVariable and calling AssociateToIntegerEqualValue().

Definition at line 618 of file integer.h.

◆ GetOrCreateAssociatedLiteral()

Literal operations_research::sat::IntegerEncoder::GetOrCreateAssociatedLiteral ( IntegerLiteral i_lit )

Returns, after creating it if needed, a Boolean literal such that:

if true, then the IntegerLiteral is true.
if false, then the negated IntegerLiteral is true.

Note: this "canonicalize" the given literal first.

This add the proper implications with the two "neighbor" literals of this one if they exist. This is the "list encoding" in: Thibaut Feydy, Peter J. Stuckey, "Lazy Clause Generation Reengineered", CP 2009.

Remove trivial literal.

Canonicalize and see if we have an equivalent literal already.

Todo: (user): on some problem this happens. We should probably make sure that we don't create extra fixed Boolean variable for no reason.

Definition at line 273 of file integer.cc.

◆ GetOrCreateLiteralAssociatedToEquality()

Literal operations_research::sat::IntegerEncoder::GetOrCreateLiteralAssociatedToEquality	(	IntegerVariable	var,
		IntegerValue	value )

Check for trivial true/false literal to avoid creating variable for no reasons.

Todo: (user): this happens on some problem. We should probably make sure that we don't create extra fixed Boolean variable for no reason.

Note: here we could detect the case before creating the literal. The initial domain didn't contain it, but maybe the one of (>= value) or (<= value) is false?

Definition at line 327 of file integer.cc.

◆ GetTrueLiteral()

Literal operations_research::sat::IntegerEncoder::GetTrueLiteral ( )

inline

Gets the literal always set to true, make it if it does not exist.

This might return false if we are already UNSAT.

Todo: (user): Make sure we abort right away on unsat!

Definition at line 641 of file integer.h.

◆ IsFixedOrHasAssociatedLiteral()

bool operations_research::sat::IntegerEncoder::IsFixedOrHasAssociatedLiteral ( IntegerLiteral i_lit ) const

Returns kNoLiteralIndex if there is no associated or the associated literal otherwise.

Tricky: for domain with hole, like [0,1][5,6], we assume some equivalence classes, like >=2, >=3, >=4 are all the same as >= 5.

Definition at line 531 of file integer.cc.

◆ LiteralOrNegationHasView()

ABSL_MUST_USE_RESULT bool operations_research::sat::IntegerEncoder::LiteralOrNegationHasView	(	Literal	lit,
		IntegerVariable *	view = nullptr,
		bool *	view_is_direct = nullptr ) const

If this is true, then a literal can be linearized with an affine expression involving an integer variable.

If a literal has both views, we want to always keep the same representative: the smallest IntegerVariable.

Definition at line 582 of file integer.cc.

◆ operator=()

IntegerEncoder & operations_research::sat::IntegerEncoder::operator= ( const IntegerEncoder & )

delete

◆ PartialDomainEncoding()

const std::vector< ValueLiteralPair > & operations_research::sat::IntegerEncoder::PartialDomainEncoding ( IntegerVariable var ) const

We can cleanup the current encoding in this case.

Definition at line 151 of file integer.cc.

◆ PartialGreaterThanEncoding()

std::vector< ValueLiteralPair > operations_research::sat::IntegerEncoder::PartialGreaterThanEncoding ( IntegerVariable var ) const

Returns the set of Literal associated to IntegerLiteral of the form var >= value. We make a copy, because this can be easily invalidated when calling any function of this class. So it is less efficient but safer.

Tricky: we need to account for holes.

Definition at line 602 of file integer.cc.

◆ ReserveSpaceForNumVariables()

void operations_research::sat::IntegerEncoder::ReserveSpaceForNumVariables ( int num_vars )

Memory optimization: you can call this before encoding variables.

Todo: (user): Reserve vector index by literals? It is trickier, as we might not know beforehand how many we will need. Consider alternatives to not waste space like using dequeue.

Definition at line 73 of file integer.cc.

◆ SearchForLiteralAtOrBefore()

LiteralIndex operations_research::sat::IntegerEncoder::SearchForLiteralAtOrBefore	(	IntegerLiteral	i_lit,
		IntegerValue *	bound ) const

Returns a Boolean literal associated with a bound lower than or equal to the one of the given IntegerLiteral. If the given IntegerLiteral is true, then the returned literal should be true too. Returns kNoLiteralIndex if no such literal was created.

Ex: if 'i' is (x >= 4) and we already created a literal associated to (x >= 2) but not to (x >= 3), we will return the literal associated with (x >= 2).

Note: we assume the input literal is canonicalized and do not fall into a hole. Otherwise, this work but will likely return a literal before and not one equivalent to it (which can be after!).

We need the entry at or before. We take the element before the upper_bound() which is either the encoding of i if it already exists, or the encoding just before it.

We ask for who is implied by -var >= -bound, so we look for the var >= value with value > bound and take its negation.

Compute tight bound if there are holes, we have X <= candidate.

Definition at line 554 of file integer.cc.

◆ UpdateEncodingOnInitialDomainChange()

bool operations_research::sat::IntegerEncoder::UpdateEncodingOnInitialDomainChange	(	IntegerVariable	var,
		Domain	domain )

Makes sure all element in the >= encoding are non-trivial and canonical. The input variable must be positive.

Fix >= literal that can be fixed. We filter and canonicalize the encoding.

We are past the end, so always false.

We are at or before the beginning, so always true.

Note: we canonicalize the literal if it fall into a hole.

Same for equality encoding. This will be lazily cleaned on the next PartialDomainEncoding() call.

Definition at line 638 of file integer.cc.

◆ VariableIsFullyEncoded()

bool operations_research::sat::IntegerEncoder::VariableIsFullyEncoded ( IntegerVariable var ) const

Returns true if we know that PartialDomainEncoding(var) span the full domain of var. This is always true if FullyEncodeVariable(var) has been called.

Once fully encoded, the status never changes.

Todo: (user): Cache result as long as equality_by_var_[index] is unchanged? It might not be needed since if the variable is not fully encoded, then PartialDomainEncoding() will filter unreachable values, and so the size check will be false until further value have been encoded.

This cleans equality_by_var_[index] as a side effect and in particular, sorts it by values.

Todo: (user): Comparing the size might be enough, but we want to be always valid even if either (*domains_[var]) or PartialDomainEncoding(var) are not properly synced because the propagation is not finished.

Definition at line 110 of file integer.cc.

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

ortools/sat/integer.h
ortools/sat/integer.cc

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ IntegerEncoder() [1/2]

◆ IntegerEncoder() [2/2]

◆ ~IntegerEncoder()

Member Function Documentation

◆ AddAllImplicationsBetweenAssociatedLiterals()

◆ AssociateToIntegerEqualValue()

◆ AssociateToIntegerLiteral()

◆ Canonicalize()

◆ DisableImplicationBetweenLiteral()

◆ FullDomainEncoding()

◆ FullyEncodeVariable()

◆ GetAllAssociatedVariables()

◆ GetAssociatedEqualityLiteral()

◆ GetAssociatedLiteral()

◆ GetEqualityLiterals()

◆ GetFalseLiteral()

◆ GetIntegerLiterals()

◆ GetLiteralView()

◆ GetOrCreateAssociatedLiteral()

◆ GetOrCreateLiteralAssociatedToEquality()

◆ GetTrueLiteral()

◆ IsFixedOrHasAssociatedLiteral()

◆ LiteralOrNegationHasView()

◆ operator=()

◆ PartialDomainEncoding()

◆ PartialGreaterThanEncoding()

◆ ReserveSpaceForNumVariables()

◆ SearchForLiteralAtOrBefore()

◆ UpdateEncodingOnInitialDomainChange()

◆ VariableIsFullyEncoded()