#include <presolve_context.h>

Public Member Functions
	PresolveContext (Model model, CpModelProto cp_model, CpModelProto *mapping)

int	NewIntVar (const Domain &domain)

int	NewBoolVar ()

int	NewIntVarWithDefinition (const Domain &domain, absl::Span< const std::pair< int, int64_t > > definition)

int	NewBoolVarWithClause (absl::Span< const int > clause)

int	GetTrueLiteral ()

int	GetFalseLiteral ()

void	AddImplication (int a, int b)
	a => b.

void	AddImplyInDomain (int b, int x, const Domain &domain)
	b => x in [lb, ub].

bool	DomainIsEmpty (int ref) const
	Helpers to query the current domain of a variable.

bool	IsFixed (int ref) const

bool	CanBeUsedAsLiteral (int ref) const

bool	LiteralIsTrue (int lit) const

bool	LiteralIsFalse (int lit) const

int64_t	MinOf (int ref) const

int64_t	MaxOf (int ref) const

int64_t	FixedValue (int ref) const

bool	DomainContains (int ref, int64_t value) const

Domain	DomainOf (int ref) const

bool	IntervalIsConstant (int ct_ref) const
	Helper to query the state of an interval.

int64_t	StartMin (int ct_ref) const

int64_t	StartMax (int ct_ref) const

int64_t	SizeMin (int ct_ref) const

int64_t	SizeMax (int ct_ref) const

int64_t	EndMin (int ct_ref) const

int64_t	EndMax (int ct_ref) const

std::string	IntervalDebugString (int ct_ref) const

int64_t	MinOf (const LinearExpressionProto &expr) const

int64_t	MaxOf (const LinearExpressionProto &expr) const

bool	IsFixed (const LinearExpressionProto &expr) const

int64_t	FixedValue (const LinearExpressionProto &expr) const

template<typename ProtoWithVarsAndCoeffs >
std::pair< int64_t, int64_t >	ComputeMinMaxActivity (const ProtoWithVarsAndCoeffs &proto) const

void	CappedUpdateMinMaxActivity (int var, int64_t coeff, int64_t min_activity, int64_t max_activity)
	Utility function.

bool	CanonicalizeLinearConstraint (ConstraintProto *ct)

bool	CanonicalizeLinearExpression (absl::Span< const int > enforcements, LinearExpressionProto *expr)

bool	DomainContains (const LinearExpressionProto &expr, int64_t value) const
	This methods only works for affine expressions (checked).

Domain	DomainSuperSetOf (const LinearExpressionProto &expr) const
	Return a super-set of the domain of the linear expression.

bool	ExpressionIsAffineBoolean (const LinearExpressionProto &expr) const

int	LiteralForExpressionMax (const LinearExpressionProto &expr) const

bool	ExpressionIsSingleVariable (const LinearExpressionProto &expr) const
	Returns true iff the expr is of the form 1 * var + 0.

bool	ExpressionIsALiteral (const LinearExpressionProto &expr, int *literal=nullptr) const
	Returns true iff the expr is a literal (x or not(x)).

bool	DomainOfVarIsIncludedIn (int var, const Domain &domain)
	This function takes a positive variable reference.

bool	VariableIsUnique (int ref) const
	Returns true if this ref only appear in one constraint.

bool	VariableIsUniqueAndRemovable (int ref) const

bool	VariableIsNotUsedAnymore (int ref) const
	Returns true if this ref no longer appears in the model.

void	MarkVariableAsRemoved (int ref)

bool	VariableWasRemoved (int ref) const

bool	VariableWithCostIsUnique (int ref) const

bool	VariableWithCostIsUniqueAndRemovable (int ref) const

bool	VariableIsOnlyUsedInEncodingAndMaybeInObjective (int var) const

bool	VariableIsOnlyUsedInLinear1AndOneExtraConstraint (int var) const

ABSL_MUST_USE_RESULT bool	IntersectDomainWith (int ref, const Domain &domain, bool *domain_modified=nullptr)

ABSL_MUST_USE_RESULT bool	SetLiteralToFalse (int lit)
	Returns false if the 'lit' doesn't have the desired value in the domain.

ABSL_MUST_USE_RESULT bool	SetLiteralToTrue (int lit)

ABSL_MUST_USE_RESULT bool	IntersectDomainWith (const LinearExpressionProto &expr, const Domain &domain, bool *domain_modified=nullptr)

ABSL_MUST_USE_RESULT bool	NotifyThatModelIsUnsat (absl::string_view message="")

bool	ModelIsUnsat () const

void	UpdateRuleStats (const std::string &name, int num_times=1)

void	UpdateConstraintVariableUsage (int c)

bool	ConstraintVariableGraphIsUpToDate () const

void	UpdateNewConstraintsVariableUsage ()
	Calls UpdateConstraintVariableUsage() on all newly created constraints.

bool	ConstraintVariableUsageIsConsistent ()

void	CanonicalizeVariable (int ref)

bool	CanonicalizeAffineVariable (int ref, int64_t coeff, int64_t mod, int64_t rhs)

bool	StoreAffineRelation (int ref_x, int ref_y, int64_t coeff, int64_t offset, bool debug_no_recursion=false)

bool	StoreBooleanEqualityRelation (int ref_a, int ref_b)

int	GetLiteralRepresentative (int ref) const
	Returns the representative of a literal.

int	NumAffineRelations () const
	Used for statistics.

AffineRelation::Relation	GetAffineRelation (int ref) const
	Returns the representative of ref under the affine relations.

std::string	RefDebugString (int ref) const
	To facilitate debugging.

std::string	AffineRelationDebugString (int ref) const

bool	PropagateAffineRelation (int ref)

bool	PropagateAffineRelation (int ref, int rep, int64_t coeff, int64_t offset)

void	InitializeNewDomains ()
	Creates the internal structure for any new variables in working_model.

void	ClearStats ()
	Clears the "rules" statistics.

bool	InsertVarValueEncoding (int literal, int var, int64_t value)

int	GetOrCreateVarValueEncoding (int ref, int64_t value)

int	GetOrCreateAffineValueEncoding (const LinearExpressionProto &expr, int64_t value)

void	CanonicalizeDomainOfSizeTwo (int var)

bool	HasVarValueEncoding (int ref, int64_t value, int *literal=nullptr)

bool	IsFullyEncoded (int ref) const

bool	IsFullyEncoded (const LinearExpressionProto &expr) const

bool	StoreLiteralImpliesVarEqValue (int literal, int var, int64_t value)

bool	StoreLiteralImpliesVarNEqValue (int literal, int var, int64_t value)

void	ReadObjectiveFromProto ()

bool	AddToObjectiveOffset (int64_t delta)

ABSL_MUST_USE_RESULT bool	CanonicalizeOneObjectiveVariable (int var)

ABSL_MUST_USE_RESULT bool	CanonicalizeObjective (bool simplify_domain=true)

void	WriteObjectiveToProto () const

ABSL_MUST_USE_RESULT bool	ScaleFloatingPointObjective ()

bool	RecomputeSingletonObjectiveDomain ()

void	WriteVariableDomainsToProto () const

bool	ExploitExactlyOneInObjective (absl::Span< const int > exactly_one)

bool	ShiftCostInExactlyOne (absl::Span< const int > exactly_one, int64_t shift)

void	RemoveVariableFromObjective (int ref)
	Allows to manipulate the objective coefficients.

void	AddToObjective (int var, int64_t value)

void	AddLiteralToObjective (int ref, int64_t value)

ABSL_MUST_USE_RESULT bool	SubstituteVariableInObjective (int var_in_equality, int64_t coeff_in_equality, const ConstraintProto &equality)

const Domain &	ObjectiveDomain () const
	Objective getters.

const absl::flat_hash_map< int, int64_t > &	ObjectiveMap () const

int64_t	ObjectiveCoeff (int var) const

bool	ObjectiveDomainIsConstraining () const

void	RemoveVariableFromAffineRelation (int var)

void	RemoveAllVariablesFromAffineRelationConstraint ()

absl::Span< const int >	ConstraintToVars (int c) const

const absl::flat_hash_set< int > &	VarToConstraints (int var) const

int	IntervalUsage (int c) const

bool	ConstraintIsInactive (int ct_index) const

bool	ConstraintIsOptional (int ct_ref) const

void	RegisterVariablesUsedInAssumptions ()

bool	ModelIsExpanded () const

void	NotifyThatModelIsExpanded ()

int	GetOrCreateReifiedPrecedenceLiteral (const LinearExpressionProto &time_i, const LinearExpressionProto &time_j, int active_i, int active_j)

std::tuple< int, int64_t, int, int64_t, int64_t, int, int >	GetReifiedPrecedenceKey (const LinearExpressionProto &time_i, const LinearExpressionProto &time_j, int active_i, int active_j)

void	ClearPrecedenceCache ()
	Clear the precedence cache.

void	LogInfo ()
	Logs stats to the logger.

void	LoadSolutionHint ()

bool	VarHasSolutionHint (int var) const
	Solution hint accessor.

int64_t	SolutionHint (int var) const

SolverLogger *	logger () const

const SatParameters &	params () const

TimeLimit *	time_limit ()

ModelRandomGenerator *	random ()

ConstraintProto *	NewMappingConstraint (absl::string_view file, int line)

ConstraintProto *	NewMappingConstraint (const ConstraintProto &base_ct, absl::string_view file, int line)

Public Attributes
CpModelProto *	working_model = nullptr

CpModelProto *	mapping_model = nullptr

bool	keep_all_feasible_solutions = false

int64_t	num_presolve_operations = 0

std::vector< int >	tmp_literals
	Temporary storage.

std::vector< Domain >	tmp_term_domains

std::vector< Domain >	tmp_left_domains

absl::flat_hash_set< int >	tmp_literal_set

SparseBitset< int >	modified_domains
	Each time a domain is modified this is set to true.

SparseBitset< int >	var_with_reduced_small_degree

DomainDeductions	deductions
	Advanced presolve. See this class comment.

Detailed Description

Wrap the CpModelProto we are presolving with extra data structure like the in-memory domain of each variables and the constraint variable graph.

Definition at line 85 of file presolve_context.h.

Constructor & Destructor Documentation

◆ PresolveContext()

operations_research::sat::PresolveContext::PresolveContext	(	Model *	model,
		CpModelProto *	cp_model,
		CpModelProto *	mapping )

inline

Definition at line 87 of file presolve_context.h.

Member Function Documentation

◆ AddImplication()

void operations_research::sat::PresolveContext::AddImplication	(	int	a,
		int	b )

a => b.

Definition at line 148 of file presolve_context.cc.

◆ AddImplyInDomain()

void operations_research::sat::PresolveContext::AddImplyInDomain	(	int	b,
		int	x,
		const Domain &	domain )

b => x in [lb, ub].

Doing it like this seems to use slightly less memory.

Todo: (user): Find the best way to create such small proto.

Definition at line 156 of file presolve_context.cc.

◆ AddLiteralToObjective()

void operations_research::sat::PresolveContext::AddLiteralToObjective	(	int	ref,
		int64_t	value )

Definition at line 1910 of file presolve_context.cc.

◆ AddToObjective()

void operations_research::sat::PresolveContext::AddToObjective	(	int	var,
		int64_t	value )

Definition at line 1898 of file presolve_context.cc.

◆ AddToObjectiveOffset()

bool operations_research::sat::PresolveContext::AddToObjectiveOffset ( int64_t delta )

Tricky: The objective domain is without the offset, so we need to shift it.

Definition at line 1927 of file presolve_context.cc.

◆ AffineRelationDebugString()

std::string operations_research::sat::PresolveContext::AffineRelationDebugString ( int ref ) const

Definition at line 1275 of file presolve_context.cc.

◆ CanBeUsedAsLiteral()

bool operations_research::sat::PresolveContext::CanBeUsedAsLiteral ( int ref ) const

Definition at line 178 of file presolve_context.cc.

◆ CanonicalizeAffineVariable()

bool operations_research::sat::PresolveContext::CanonicalizeAffineVariable	(	int	ref,
		int64_t	coeff,
		int64_t	mod,
		int64_t	rhs )

Given the relation (X * coeff % mod = rhs % mod), this creates a new variable so that X = mod * Y + cte.

This requires mod != 0 and coeff != 0.

Note: the new variable will have a canonical domain (i.e. min == 0). We also do not create anything if this fixes the given variable or the relation simplifies. Returns false if the model is infeasible.

We just abort in this case as there is no point introducing a new variable.

From var * coeff % mod = rhs We have var = mod * X + offset.

Lets create a new integer variable and add the affine relation.

We make sure the new variable has a domain starting at zero to minimize future overflow issues. If it end up Boolean, it is also nice to be able to use it as such.

A potential problem with this is that it messes up the natural variable order chosen by the modeler. We try to correct that when mapping variables at the end of the presolve.

Definition at line 944 of file presolve_context.cc.

◆ CanonicalizeDomainOfSizeTwo()

void operations_research::sat::PresolveContext::CanonicalizeDomainOfSizeTwo ( int var )

If not already done, adds a Boolean to represent any integer variables that take only two values. Make sure all the relevant affine and encoding relations are updated.

Note: this might create a new Boolean variable.

Find encoding for min if present.

Find encoding for max if present.

Insert missing encoding.

Add affine relation.

Definition at line 1325 of file presolve_context.cc.

◆ CanonicalizeLinearConstraint()

bool operations_research::sat::PresolveContext::CanonicalizeLinearConstraint ( ConstraintProto * ct )

Canonicalization of linear constraint. This might also be needed when creating new constraint to make sure there are no duplicate variables. Returns true if the set of variables in the expression changed.

This uses affine relation and regroup duplicate/fixed terms.

Definition at line 2436 of file presolve_context.cc.

◆ CanonicalizeLinearExpression()

bool operations_research::sat::PresolveContext::CanonicalizeLinearExpression	(	absl::Span< const int >	enforcements,
		LinearExpressionProto *	expr )

Definition at line 2449 of file presolve_context.cc.

◆ CanonicalizeObjective()

bool operations_research::sat::PresolveContext::CanonicalizeObjective ( bool simplify_domain = true )

We replace each entry by its affine representative.

Note: the non-deterministic loop is fine, but because we iterate one the map while modifying it, it is safer to do a copy rather than to try to handle that in one pass.

Todo: (user): This is a bit duplicated with the presolve linear code. We also do not propagate back any domain restriction from the objective to the variables if any.

We need to sort the entries to be deterministic.

This is the new domain.

Note: the domain never include the offset.

Depending on the use case, we cannot do that.

Maybe divide by GCD.

We update the offset accordingly.

To avoid overflow in (fixed_value * gcd + before_offset) * factor + after_offset because the objective is constant (and should fit on an int64_t), we can rewrite it as fixed_value + offset.

It is important to update the implied_domain for the "is constraining" test below.

Detect if the objective domain do not limit the "optimal" objective value. If this is true, then we can apply any reduction that reduce the objective value without any issues.

Definition at line 1770 of file presolve_context.cc.

◆ CanonicalizeOneObjectiveVariable()

bool operations_research::sat::PresolveContext::CanonicalizeOneObjectiveVariable ( int var )

If a variable only appear in objective, we can fix it!

Note: we don't care if it was in affine relation, because if none of the relations are left, then we can still fix it.

Do the substitution.

Process new term.

Definition at line 1718 of file presolve_context.cc.

◆ CanonicalizeVariable()

void operations_research::sat::PresolveContext::CanonicalizeVariable ( int ref )

A "canonical domain" always have a MinOf() equal to zero. If needed we introduce a new variable with such canonical domain and add the relation X = Y + offset.

This is useful in some corner case to avoid overflow.

Todo: (user): When we can always get rid of affine relation, it might be good to do a final pass to canonicalize all domains in a model after presolve.

Definition at line 914 of file presolve_context.cc.

◆ CappedUpdateMinMaxActivity()

void operations_research::sat::PresolveContext::CappedUpdateMinMaxActivity	(	int	var,
		int64_t	coeff,
		int64_t *	min_activity,
		int64_t *	max_activity )

inline

Utility function.

Definition at line 177 of file presolve_context.h.

◆ ClearPrecedenceCache()

void operations_research::sat::PresolveContext::ClearPrecedenceCache ( )

Clear the precedence cache.

Definition at line 2259 of file presolve_context.cc.

◆ ClearStats()

void operations_research::sat::PresolveContext::ClearStats ( )

Clears the "rules" statistics.

Definition at line 70 of file presolve_context.cc.

◆ ComputeMinMaxActivity()

template<typename ProtoWithVarsAndCoeffs >

std::pair< int64_t, int64_t > operations_research::sat::PresolveContext::ComputeMinMaxActivity ( const ProtoWithVarsAndCoeffs & proto ) const

inline

Accepts any proto with two parallel vector .vars() and .coeffs(), like LinearConstraintProto or ObjectiveProto or LinearExpressionProto but beware that this ignore any offset.

Definition at line 157 of file presolve_context.h.

◆ ConstraintIsInactive()

bool operations_research::sat::PresolveContext::ConstraintIsInactive ( int ct_index ) const

Checks if a constraint contains an enforcement literal set to false, or if it has been cleared.

Definition at line 572 of file presolve_context.cc.

◆ ConstraintIsOptional()

bool operations_research::sat::PresolveContext::ConstraintIsOptional ( int ct_ref ) const

Checks if a constraint contains an enforcement literal not fixed, and no enforcement literals set to false.

Definition at line 584 of file presolve_context.cc.

◆ ConstraintToVars()

absl::Span< const int > operations_research::sat::PresolveContext::ConstraintToVars ( int c ) const

inline

Variable <-> constraint graph. The vector list is sorted and contains unique elements.

Important: To properly handle the objective, var_to_constraints[objective] contains kObjectiveConstraint (i.e. -1) so that if the objective appear in only one constraint, the constraint cannot be simplified.

Definition at line 515 of file presolve_context.h.

◆ ConstraintVariableGraphIsUpToDate()

bool operations_research::sat::PresolveContext::ConstraintVariableGraphIsUpToDate ( ) const

At the beginning of the presolve, we delay the costly creation of this "graph" until we at least ran some basic presolve. This is because during a LNS neighbhorhood, many constraints will be reduced significantly by this "simple" presolve.

Definition at line 716 of file presolve_context.cc.

◆ ConstraintVariableUsageIsConsistent()

bool operations_research::sat::PresolveContext::ConstraintVariableUsageIsConsistent ( )

Returns true if our current constraints <-> variables graph is ok. This is meant to be used in DEBUG mode only.

Todo: (user): Also test var_to_constraints_ !!

Definition at line 733 of file presolve_context.cc.

◆ DomainContains() [1/2]

bool operations_research::sat::PresolveContext::DomainContains	(	const LinearExpressionProto &	expr,
		int64_t	value ) const

This methods only works for affine expressions (checked).

Definition at line 483 of file presolve_context.cc.

◆ DomainContains() [2/2]

bool operations_research::sat::PresolveContext::DomainContains	(	int	ref,
		int64_t	value ) const

Definition at line 476 of file presolve_context.cc.

◆ DomainIsEmpty()

bool operations_research::sat::PresolveContext::DomainIsEmpty ( int ref ) const

Helpers to query the current domain of a variable.

Definition at line 168 of file presolve_context.cc.

◆ DomainOf()

Domain operations_research::sat::PresolveContext::DomainOf ( int ref ) const

Definition at line 466 of file presolve_context.cc.

◆ DomainOfVarIsIncludedIn()

bool operations_research::sat::PresolveContext::DomainOfVarIsIncludedIn	(	int	var,
		const Domain &	domain )

inline

This function takes a positive variable reference.

Definition at line 216 of file presolve_context.h.

◆ DomainSuperSetOf()

Domain operations_research::sat::PresolveContext::DomainSuperSetOf ( const LinearExpressionProto & expr ) const

Return a super-set of the domain of the linear expression.

Definition at line 262 of file presolve_context.cc.

◆ EndMax()

int64_t operations_research::sat::PresolveContext::EndMax ( int ct_ref ) const

Definition at line 365 of file presolve_context.cc.

◆ EndMin()

int64_t operations_research::sat::PresolveContext::EndMin ( int ct_ref ) const

Definition at line 359 of file presolve_context.cc.

◆ ExploitExactlyOneInObjective()

bool operations_research::sat::PresolveContext::ExploitExactlyOneInObjective ( absl::Span< const int > exactly_one )

Checks if the given exactly_one is included in the objective, and simplify the objective by adding a constant value to all the exactly one terms.

Returns true if a simplification was done.

Objective = coeff * var = coeff * (1 - ref);

Definition at line 2017 of file presolve_context.cc.

◆ ExpressionIsAffineBoolean()

bool operations_research::sat::PresolveContext::ExpressionIsAffineBoolean ( const LinearExpressionProto & expr ) const

Returns true iff the expr is of the form a * literal + b. The other function can be used to get the literal that achieve MaxOf().

Definition at line 272 of file presolve_context.cc.

◆ ExpressionIsALiteral()

bool operations_research::sat::PresolveContext::ExpressionIsALiteral	(	const LinearExpressionProto &	expr,
		int *	literal = nullptr ) const

Returns true iff the expr is a literal (x or not(x)).

Definition at line 289 of file presolve_context.cc.

◆ ExpressionIsSingleVariable()

bool operations_research::sat::PresolveContext::ExpressionIsSingleVariable ( const LinearExpressionProto & expr ) const

Returns true iff the expr is of the form 1 * var + 0.

Definition at line 284 of file presolve_context.cc.

◆ FixedValue() [1/2]

int64_t operations_research::sat::PresolveContext::FixedValue ( const LinearExpressionProto & expr ) const

Definition at line 253 of file presolve_context.cc.

◆ FixedValue() [2/2]

int64_t operations_research::sat::PresolveContext::FixedValue ( int ref ) const

Definition at line 213 of file presolve_context.cc.

◆ GetAffineRelation()

AffineRelation::Relation operations_research::sat::PresolveContext::GetAffineRelation ( int ref ) const

Returns the representative of ref under the affine relations.

This makes sure that the affine relation only uses one of the representative from the var_equiv_relations_.

Definition at line 1261 of file presolve_context.cc.

◆ GetFalseLiteral()

int operations_research::sat::PresolveContext::GetFalseLiteral ( )

Definition at line 145 of file presolve_context.cc.

◆ GetLiteralRepresentative()

int operations_research::sat::PresolveContext::GetLiteralRepresentative ( int ref ) const

Returns the representative of a literal.

Note(user): This can happen is some corner cases where the affine relation where added before the variable became usable as Boolean. When this is the case, the domain will be of the form [x, x + 1] and should be later remapped to a Boolean variable.

We made sure that the affine representative can always be used as a literal. However, if some variable are fixed, we might not have only (coeff=1 offset=0) or (coeff=-1 offset=1) and we might have something like (coeff=8 offset=0) which is only valid for both variable at zero...

What is sure is that depending on the value, only one mapping can be valid because r.coeff can never be zero.

Definition at line 1230 of file presolve_context.cc.

◆ GetOrCreateAffineValueEncoding()

int operations_research::sat::PresolveContext::GetOrCreateAffineValueEncoding	(	const LinearExpressionProto &	expr,
		int64_t	value )

Gets the associated literal if it is already created. Otherwise create it, add the corresponding constraints and returns it.

Important: This does not update the constraint<->variable graph, so ConstraintVariableGraphIsUpToDate() will be false until UpdateNewConstraintsVariableUsage() is called.

Definition at line 1642 of file presolve_context.cc.

◆ GetOrCreateReifiedPrecedenceLiteral()

int operations_research::sat::PresolveContext::GetOrCreateReifiedPrecedenceLiteral	(	const LinearExpressionProto &	time_i,
		const LinearExpressionProto &	time_j,
		int	active_i,
		int	active_j )

The following helper adds the following constraint: result <=> (time_i <= time_j && active_i is true && active_j is true) and returns the (cached) literal result.

Note: this cache should just be used temporarily and then cleared with ClearPrecedenceCache() because there is no mechanism to update the cached literals when literal equivalence are detected.

result => (time_i <= time_j) && active_i && active_j.

Not(result) && active_i && active_j => (time_i > time_j)

This is redundant but should improves performance.

If GetOrCreateReifiedPrecedenceLiteral(time_j, time_i, active_j, active_i) (the reverse precedence) has been called too, then we can link the two precedence literals, and the two active literals together.

Definition at line 2151 of file presolve_context.cc.

◆ GetOrCreateVarValueEncoding()

int operations_research::sat::PresolveContext::GetOrCreateVarValueEncoding	(	int	ref,
		int64_t	value )

Gets the associated literal if it is already created. Otherwise create it, add the corresponding constraints and returns it.

Important: This does not update the constraint<->variable graph, so ConstraintVariableGraphIsUpToDate() will be false until UpdateNewConstraintsVariableUsage() is called.

Positive after CanonicalizeEncoding().

Returns the false literal if the value is not in the domain.

Returns the associated literal if already present.

If the variable was already removed, for now we create a new one. This should be rare hopefully.

Special case for fixed domains.

Special case for domains of size 2.

Checks if the other value is already encoded.

If the variable was already removed, for now we create a new one. This should be rare hopefully.

Update the encoding map. The domain could have been reduced to size two after the creation of the first literal.

Definition at line 1570 of file presolve_context.cc.

◆ GetReifiedPrecedenceKey()

std::tuple< int, int64_t, int, int64_t, int64_t, int, int > operations_research::sat::PresolveContext::GetReifiedPrecedenceKey	(	const LinearExpressionProto &	time_i,
		const LinearExpressionProto &	time_j,
		int	active_i,
		int	active_j )

In all formulas, active_i and active_j are symmetrical, we can sort the active literals.

Definition at line 2240 of file presolve_context.cc.

◆ GetTrueLiteral()

int operations_research::sat::PresolveContext::GetTrueLiteral ( )

Some expansion code use constant literal to be simpler to write. This will create a NewBoolVar() the first time, but later call will just returns it.

Definition at line 137 of file presolve_context.cc.

◆ HasVarValueEncoding()

bool operations_research::sat::PresolveContext::HasVarValueEncoding	(	int	ref,
		int64_t	value,
		int *	literal = nullptr )

Returns true if a literal attached to ref == var exists. It assigns the corresponding to literal if non null.

Definition at line 1540 of file presolve_context.cc.

◆ InitializeNewDomains()

void operations_research::sat::PresolveContext::InitializeNewDomains ( )

Creates the internal structure for any new variables in working_model.

Create the internal structure for any new variables in working_model.

We mark the domain as modified so we will look at these new variable during our presolve loop.

We resize the hint too even if not loaded.

Definition at line 1282 of file presolve_context.cc.

◆ InsertVarValueEncoding()

bool operations_research::sat::PresolveContext::InsertVarValueEncoding	(	int	literal,
		int	var,
		int64_t	value )

Inserts the given literal to encode var == value. If an encoding already exists, it adds the two implications between the previous encoding and the new encoding.

Important: This does not update the constraint<->variable graph, so ConstraintVariableGraphIsUpToDate() will be false until UpdateNewConstraintsVariableUsage() is called.

Returns false if the model become UNSAT.

Todo: (user): This function is not always correct if !context->DomainOf(var).contains(value), we could make it correct but it might be a bit expansive to do so. For now we just have a DCHECK().

Definition at line 1504 of file presolve_context.cc.

◆ IntersectDomainWith() [1/2]

ABSL_MUST_USE_RESULT bool operations_research::sat::PresolveContext::IntersectDomainWith	(	const LinearExpressionProto &	expr,
		const Domain &	domain,
		bool *	domain_modified = nullptr )

Same as IntersectDomainWith() but take a linear expression as input. If this expression if of size > 1, this does nothing for now, so it will only propagates for constant and affine expression.

We don't do anything for longer expression for now.

Definition at line 539 of file presolve_context.cc.

◆ IntersectDomainWith() [2/2]

ABSL_MUST_USE_RESULT bool operations_research::sat::PresolveContext::IntersectDomainWith	(	int	ref,
		const Domain &	domain,
		bool *	domain_modified = nullptr )

Returns false if the new domain is empty. Sets 'domain_modified' (if provided) to true iff the domain is modified otherwise does not change it.

Propagate the domain of the representative right away.

Note: the recursive call should only by one level deep.

Definition at line 493 of file presolve_context.cc.

◆ IntervalDebugString()

std::string operations_research::sat::PresolveContext::IntervalDebugString ( int ct_ref ) const

Definition at line 321 of file presolve_context.cc.

◆ IntervalIsConstant()

bool operations_research::sat::PresolveContext::IntervalIsConstant ( int ct_ref ) const

Helper to query the state of an interval.

Note: we only support converted intervals.

Definition at line 312 of file presolve_context.cc.

◆ IntervalUsage()

int operations_research::sat::PresolveContext::IntervalUsage ( int c ) const

inline

Definition at line 523 of file presolve_context.h.

◆ IsFixed() [1/2]

bool operations_research::sat::PresolveContext::IsFixed ( const LinearExpressionProto & expr ) const

Definition at line 246 of file presolve_context.cc.

◆ IsFixed() [2/2]

bool operations_research::sat::PresolveContext::IsFixed ( int ref ) const

Definition at line 172 of file presolve_context.cc.

◆ IsFullyEncoded() [1/2]

bool operations_research::sat::PresolveContext::IsFullyEncoded ( const LinearExpressionProto & expr ) const

This methods only works for affine expressions (checked). It returns true iff the expression is constant or its one variable is full encoded.

Definition at line 1564 of file presolve_context.cc.

◆ IsFullyEncoded() [2/2]

bool operations_research::sat::PresolveContext::IsFullyEncoded ( int ref ) const

Returns true if we have literal <=> var = value for all values of var.

Todo: (user): If the domain was shrunk, we can have a false positive. Still it means that the number of values removed is greater than the number of values not encoded.

Definition at line 1556 of file presolve_context.cc.

◆ LiteralForExpressionMax()

int operations_research::sat::PresolveContext::LiteralForExpressionMax ( const LinearExpressionProto & expr ) const

Definition at line 278 of file presolve_context.cc.

◆ LiteralIsFalse()

bool operations_research::sat::PresolveContext::LiteralIsFalse ( int lit ) const

Definition at line 192 of file presolve_context.cc.

◆ LiteralIsTrue()

bool operations_research::sat::PresolveContext::LiteralIsTrue ( int lit ) const

Definition at line 183 of file presolve_context.cc.

◆ LoadSolutionHint()

void operations_research::sat::PresolveContext::LoadSolutionHint ( )

This should be called only once after InitializeNewDomains() to load the hint, in order to maintain it as best as possible during presolve.

Definition at line 1308 of file presolve_context.cc.

◆ logger()

SolverLogger * operations_research::sat::PresolveContext::logger ( ) const

inline

Definition at line 581 of file presolve_context.h.

◆ LogInfo()

void operations_research::sat::PresolveContext::LogInfo ( )

Logs stats to the logger.

Definition at line 2263 of file presolve_context.cc.

◆ MarkVariableAsRemoved()

void operations_research::sat::PresolveContext::MarkVariableAsRemoved ( int ref )

Functions to make sure that once we remove a variable, we no longer reuse it.

Definition at line 422 of file presolve_context.cc.

◆ MaxOf() [1/2]

int64_t operations_research::sat::PresolveContext::MaxOf ( const LinearExpressionProto & expr ) const

Definition at line 233 of file presolve_context.cc.

◆ MaxOf() [2/2]

int64_t operations_research::sat::PresolveContext::MaxOf ( int ref ) const

Definition at line 207 of file presolve_context.cc.

◆ MinOf() [1/2]

int64_t operations_research::sat::PresolveContext::MinOf ( const LinearExpressionProto & expr ) const

Helpers to query the current domain of a linear expression. This doesn't check for integer overflow, but our linear expression should be such that this cannot happen (tested at validation).

Definition at line 220 of file presolve_context.cc.

◆ MinOf() [2/2]

int64_t operations_research::sat::PresolveContext::MinOf ( int ref ) const

Definition at line 201 of file presolve_context.cc.

◆ ModelIsExpanded()

bool operations_research::sat::PresolveContext::ModelIsExpanded ( ) const

inline

The "expansion" phase should be done once and allow to transform complex constraints into basic ones (see cp_model_expand.h). Some presolve rules need to know if the expansion was ran before beeing applied.

Definition at line 548 of file presolve_context.h.

◆ ModelIsUnsat()

bool operations_research::sat::PresolveContext::ModelIsUnsat ( ) const

inline

Definition at line 277 of file presolve_context.h.

◆ NewBoolVar()

int operations_research::sat::PresolveContext::NewBoolVar ( )

Definition at line 100 of file presolve_context.cc.

◆ NewBoolVarWithClause()

int operations_research::sat::PresolveContext::NewBoolVarWithClause ( absl::Span< const int > clause )

Create a new bool var. Its hint value will be the same as the value of the given clause.

If there all literal where hinted and at zero, we set the hint of new_var to zero, otherwise we leave it unassigned.

Definition at line 102 of file presolve_context.cc.

◆ NewIntVar()

int operations_research::sat::PresolveContext::NewIntVar ( const Domain & domain )

Helpers to adds new variables to the presolved model.

Todo: (user): We should control more how this is called so we can update a solution hint accordingly.

Definition at line 72 of file presolve_context.cc.

◆ NewIntVarWithDefinition()

int operations_research::sat::PresolveContext::NewIntVarWithDefinition	(	const Domain &	domain,
		absl::Span< const std::pair< int, int64_t > >	definition )

This should replace NewIntVar() eventually in order to be able to crush primal solution or just update the hint.

We only fill the hint of the new variable if all the variable involved in its definition have a value.

Definition at line 79 of file presolve_context.cc.

◆ NewMappingConstraint() [1/2]

ConstraintProto * operations_research::sat::PresolveContext::NewMappingConstraint	(	absl::string_view	file,
		int	line )

Adds a new constraint to the mapping proto. The version with the base constraint will copy that constraint to the new constraint.

If the flag –cp_model_debug_postsolve is set, we will use the caller file/line number to add debug info in the constraint name() field.

Definition at line 2458 of file presolve_context.cc.

◆ NewMappingConstraint() [2/2]

ConstraintProto * operations_research::sat::PresolveContext::NewMappingConstraint	(	const ConstraintProto &	base_ct,
		absl::string_view	file,
		int	line )

Definition at line 2468 of file presolve_context.cc.

◆ NotifyThatModelIsExpanded()

void operations_research::sat::PresolveContext::NotifyThatModelIsExpanded ( )

inline

Definition at line 549 of file presolve_context.h.

◆ NotifyThatModelIsUnsat()

ABSL_MUST_USE_RESULT bool operations_research::sat::PresolveContext::NotifyThatModelIsUnsat ( absl::string_view message = "" )

inline

This function always return false. It is just a way to make a little bit more sure that we abort right away when infeasibility is detected.

Todo: (user): Report any explanation for the client in a nicer way?

Definition at line 270 of file presolve_context.h.

◆ NumAffineRelations()

int operations_research::sat::PresolveContext::NumAffineRelations ( ) const

inline

Used for statistics.

Definition at line 348 of file presolve_context.h.

◆ ObjectiveCoeff()

int64_t operations_research::sat::PresolveContext::ObjectiveCoeff ( int var ) const

inline

Definition at line 495 of file presolve_context.h.

◆ ObjectiveDomain()

const Domain & operations_research::sat::PresolveContext::ObjectiveDomain ( ) const

inline

Objective getters.

Definition at line 491 of file presolve_context.h.

◆ ObjectiveDomainIsConstraining()

bool operations_research::sat::PresolveContext::ObjectiveDomainIsConstraining ( ) const

inline

Definition at line 500 of file presolve_context.h.

◆ ObjectiveMap()

const absl::flat_hash_map< int, int64_t > & operations_research::sat::PresolveContext::ObjectiveMap ( ) const

inline

Definition at line 492 of file presolve_context.h.

◆ params()

const SatParameters & operations_research::sat::PresolveContext::params ( ) const

inline

Definition at line 582 of file presolve_context.h.

◆ PropagateAffineRelation() [1/2]

bool operations_research::sat::PresolveContext::PropagateAffineRelation ( int ref )

Makes sure the domain of ref and of its representative (ref = coeff * rep + offset) are in sync. Returns false on unsat.

Definition at line 840 of file presolve_context.cc.

◆ PropagateAffineRelation() [2/2]

bool operations_research::sat::PresolveContext::PropagateAffineRelation	(	int	ref,
		int	rep,
		int64_t	coeff,
		int64_t	offset )

Propagate domains both ways. var = coeff * rep + offset

Definition at line 847 of file presolve_context.cc.

◆ random()

ModelRandomGenerator * operations_research::sat::PresolveContext::random ( )

inline

Definition at line 584 of file presolve_context.h.

◆ ReadObjectiveFromProto()

void operations_research::sat::PresolveContext::ReadObjectiveFromProto ( )

Objective handling functions. We load it at the beginning so that during presolve we can work on the more efficient hash_map representation.

Note: ReadObjectiveFromProto() makes sure that var_to_constraints of all the variable that appear in the objective contains -1. This is later enforced by all the functions modifying the objective.

Note(user): Because we process affine relation only on CanonicalizeObjective(), it is possible that when processing a canonicalized linear constraint, we don't detect that a variable in affine relation is in the objective. For now this is fine, because when this is the case, we also have an affine linear constraint, so we can't really do anything with that variable since it appear in at least two constraints.

We do some small canonicalization here

We might relax this in CanonicalizeObjective() when we will compute the possible objective domain from the domains of the variables.

This is an upper bound of the higher magnitude that can be reach by summing an objective partial sum. Because of the model validation, this shouldn't overflow, and we make sure it stays this way.

Skipping var fixed to zero allow to avoid some overflow in situation were we can deal with it.

Definition at line 1661 of file presolve_context.cc.

◆ RecomputeSingletonObjectiveDomain()

bool operations_research::sat::PresolveContext::RecomputeSingletonObjectiveDomain ( )

When the objective is singleton, we can always restrict the domain of var so that the current objective domain is non-constraining. Returns false on UNSAT.

Transfer all the info to the domain of var.

Recompute a correct and non-constraining objective domain.

Definition at line 1873 of file presolve_context.cc.

◆ RefDebugString()

std::string operations_research::sat::PresolveContext::RefDebugString ( int ref ) const

To facilitate debugging.

Definition at line 1270 of file presolve_context.cc.

◆ RegisterVariablesUsedInAssumptions()

void operations_research::sat::PresolveContext::RegisterVariablesUsedInAssumptions ( )

inline

Make sure we never delete an "assumption" literal by using a special constraint for that.

Definition at line 539 of file presolve_context.h.

◆ RemoveAllVariablesFromAffineRelationConstraint()

void operations_research::sat::PresolveContext::RemoveAllVariablesFromAffineRelationConstraint ( )

Definition at line 877 of file presolve_context.cc.

◆ RemoveVariableFromAffineRelation()

void operations_research::sat::PresolveContext::RemoveVariableFromAffineRelation ( int var )

Advanced usage. This should be called when a variable can be removed from the problem, so we don't count it as part of an affine relation anymore.

We only call that for a non representative variable that is only used in the kAffineRelationConstraint. Such variable can be ignored and should never be seen again in the presolve.

We shouldn't reuse this variable again!

We do not call EraseFromVarToConstraint() on purpose here since the variable is removed.

If the representative is left alone, we can remove it from the special affine relation constraint too.

Definition at line 886 of file presolve_context.cc.

◆ RemoveVariableFromObjective()

void operations_research::sat::PresolveContext::RemoveVariableFromObjective ( int ref )

Allows to manipulate the objective coefficients.

Definition at line 1891 of file presolve_context.cc.

◆ ScaleFloatingPointObjective()

bool operations_research::sat::PresolveContext::ScaleFloatingPointObjective ( )

We need the domains up to date before scaling.

Definition at line 925 of file presolve_context.cc.

◆ SetLiteralToFalse()

ABSL_MUST_USE_RESULT bool operations_research::sat::PresolveContext::SetLiteralToFalse ( int lit )

Returns false if the 'lit' doesn't have the desired value in the domain.

Definition at line 562 of file presolve_context.cc.

◆ SetLiteralToTrue()

ABSL_MUST_USE_RESULT bool operations_research::sat::PresolveContext::SetLiteralToTrue ( int lit )

Definition at line 568 of file presolve_context.cc.

◆ ShiftCostInExactlyOne()

bool operations_research::sat::PresolveContext::ShiftCostInExactlyOne	(	absl::Span< const int >	exactly_one,
		int64_t	shift )

We can always add a multiple of sum X - 1 == 0 to the objective. However, depending on which multiple we choose, this might break our overflow preconditions on the objective. So we return false and do nothing if this happens.

We have to be careful because shifting cost like this might increase the min/max possible activity of the sum.

Todo: (user): Be more precise with this objective_overflow_detection_ and always keep it up to date on each offset / coeff change.

The value will be zero if it wasn't present.

Term = coeff * (1 - X) = coeff - coeff * X; So -coeff -> -coeff -shift And Term = coeff + shift - shift - (coeff + shift) * X = (coeff + shift) * (1 - X) - shift;

Note: the domain never include the offset, so we need to update it.

When we shift the cost using an exactly one, our objective implied bounds might be more or less precise. If the objective domain is not constraining (and thus just constraining the upper bound), we relax it to make sure its stay "non constraining".

Todo: (user): This is a bit hacky, find a nicer way.

Definition at line 2039 of file presolve_context.cc.

◆ SizeMax()

int64_t operations_research::sat::PresolveContext::SizeMax ( int ct_ref ) const

Definition at line 377 of file presolve_context.cc.

◆ SizeMin()

int64_t operations_research::sat::PresolveContext::SizeMin ( int ct_ref ) const

Definition at line 371 of file presolve_context.cc.

◆ SolutionHint()

int64_t operations_research::sat::PresolveContext::SolutionHint ( int var ) const

inline

Definition at line 579 of file presolve_context.h.

◆ StartMax()

int64_t operations_research::sat::PresolveContext::StartMax ( int ct_ref ) const

Definition at line 353 of file presolve_context.cc.

◆ StartMin()

int64_t operations_research::sat::PresolveContext::StartMin ( int ct_ref ) const

Definition at line 347 of file presolve_context.cc.

◆ StoreAffineRelation()

bool operations_research::sat::PresolveContext::StoreAffineRelation	(	int	ref_x,
		int	ref_y,
		int64_t	coeff,
		int64_t	offset,
		bool	debug_no_recursion = false )

Adds the relation (ref_x = coeff * ref_y + offset) to the repository. Returns false if we detect infeasability because of this.

Once the relation is added, it doesn't need to be enforced by a constraint in the model proto, since we will propagate such relation directly and add them to the proto at the end of the presolve.

Note: this should always add a relation, even though it might need to create a new representative for both ref_x and ref_y in some cases. Like if x = 3z and y = 5t are already added, if we add x = 2y, we have 3z = 10t and can only resolve this by creating a new variable r such that z = 10r and t = 3r.

All involved variables will be marked to appear in the special kAffineRelationConstraint. This will allow to identify when a variable is no longer needed (only appear there and is not a representative).

Todo: (user): Do we implement a rounding to closest instead of routing towards 0.

Todo: (user): I am not 100% sure why, but sometimes the representative is fixed but that is not propagated to ref_x or ref_y and this causes issues.

If both are already in the same class, we need to make sure the relations are compatible.

x = rx.coeff * rep + rx.offset; y = ry.coeff * rep + ry.offset; And x == coeff * ry.coeff * rep + (coeff * ry.offset + offset).

So we get the relation a * rep == b with a and b defined here:

ref_x = coeff * ref_y + offset; rx.coeff * rep_x + rx.offset = coeff * (ry.coeff * rep_y + ry.offset) + offset

We have a * rep_x + b * rep_y == o

In this (rare) case, we need to canonicalize one of the variable that will become the representative for both.

Re-add the relation now that a will resolve to a multiple of b.

Canonicalize from (a * rep_x + b * rep_y = o) to (x = c * y + o).

Lets propagate domains first.

To avoid corner cases where replacing x by y in a linear expression can cause overflow, we might want to canonicalize y first to avoid cases like x = c * [large_value, ...] - large_value.

Todo: (user): we can do better for overflow by not always choosing the min at zero, do the best things if it becomes needed.

Both these function recursively call StoreAffineRelation() but shouldn't be able to cascade (CHECKED).

Todo: (user): can we force the rep and remove GetAffineRelation()?

Lets propagate again the new relation. We might as well do it as early as possible and not all call site do it.

Todo: (user): I am not sure this is needed given the propagation above.

These maps should only contains representative, so only need to remap either x or y.

The domain didn't change, but this notification allows to re-process any constraint containing these variables. Note that we do not need to retrigger a propagation of the constraint containing a variable whose representative didn't change.

Definition at line 1008 of file presolve_context.cc.

◆ StoreBooleanEqualityRelation()

bool operations_research::sat::PresolveContext::StoreBooleanEqualityRelation	(	int	ref_a,
		int	ref_b )

Adds the fact that ref_a == ref_b using StoreAffineRelation() above. Returns false if this makes the problem infeasible.

a = b

a = 1 - b

Definition at line 1207 of file presolve_context.cc.

◆ StoreLiteralImpliesVarEqValue()

bool operations_research::sat::PresolveContext::StoreLiteralImpliesVarEqValue	(	int	literal,
		int	var,
		int64_t	value )

Stores the fact that literal implies var == value. It returns true if that information is new.

Definition at line 1524 of file presolve_context.cc.

◆ StoreLiteralImpliesVarNEqValue()

bool operations_research::sat::PresolveContext::StoreLiteralImpliesVarNEqValue	(	int	literal,
		int	var,
		int64_t	value )

Stores the fact that literal implies var != value. It returns true if that information is new.

Definition at line 1533 of file presolve_context.cc.

◆ SubstituteVariableInObjective()

bool operations_research::sat::PresolveContext::SubstituteVariableInObjective	(	int	var_in_equality,
		int64_t	coeff_in_equality,
		const ConstraintProto &	equality )

Given a variable defined by the given inequality that also appear in the objective, remove it from the objective by transferring its cost to other variables in the equality.

Returns false, if the substitution cannot be done. This is the case if the model become UNSAT or if doing it will result in an objective that do not satisfy our overflow preconditions. Note that this can only happen if the substituted variable is not implied free (i.e. if its domain is smaller than the implied domain from the equality).

We can only "easily" substitute if the objective coefficient is a multiple of the one in the constraint.

Abort if the new objective seems to violate our overflow preconditions.

Compute the objective offset change.

We also need to make sure the integer_offset will not overflow.

Perform the substitution.

Because we can assume that the constraint we used was constraining (otherwise it would have been removed), the objective domain should be now constraining.

Definition at line 1940 of file presolve_context.cc.

◆ time_limit()

TimeLimit * operations_research::sat::PresolveContext::time_limit ( )

inline

Definition at line 583 of file presolve_context.h.

◆ UpdateConstraintVariableUsage()

void operations_research::sat::PresolveContext::UpdateConstraintVariableUsage ( int c )

Updates the constraints <-> variables graph. This needs to be called each time a constraint is modified.

We don't optimize the interval usage as this is not super frequent.

For the variables, we avoid an erase() followed by an insert() for the variables that didn't change.

Definition at line 667 of file presolve_context.cc.

◆ UpdateNewConstraintsVariableUsage()

void operations_research::sat::PresolveContext::UpdateNewConstraintsVariableUsage ( )

Calls UpdateConstraintVariableUsage() on all newly created constraints.

Definition at line 720 of file presolve_context.cc.

◆ UpdateRuleStats()

void operations_research::sat::PresolveContext::UpdateRuleStats	(	const std::string &	name,
		int	num_times = 1 )

Stores a description of a rule that was just applied to have a summary of what the presolve did at the end.

Hack: we don't want to count

Todo: rules as this is used to decide if we loop again.

Definition at line 594 of file presolve_context.cc.

◆ VarHasSolutionHint()

bool operations_research::sat::PresolveContext::VarHasSolutionHint ( int var ) const

inline

Solution hint accessor.

Definition at line 578 of file presolve_context.h.

◆ VariableIsNotUsedAnymore()

bool operations_research::sat::PresolveContext::VariableIsNotUsedAnymore ( int ref ) const

Returns true if this ref no longer appears in the model.

Here, even if the variable is equivalent to others, if its affine defining constraints where removed, then it is not needed anymore.

Definition at line 417 of file presolve_context.cc.

◆ VariableIsOnlyUsedInEncodingAndMaybeInObjective()

bool operations_research::sat::PresolveContext::VariableIsOnlyUsedInEncodingAndMaybeInObjective ( int var ) const

Returns true if an integer variable is only appearing in the rhs of constraints of the form lit => var in domain. When this is the case, then we can usually remove this variable and replace these constraints with the proper constraints on the enforcement literals.

Definition at line 448 of file presolve_context.cc.

◆ VariableIsOnlyUsedInLinear1AndOneExtraConstraint()

bool operations_research::sat::PresolveContext::VariableIsOnlyUsedInLinear1AndOneExtraConstraint ( int var ) const

Similar to VariableIsOnlyUsedInEncodingAndMaybeInObjective() for the case where we have one extra constraint instead of the objective. Sometimes it is possible to transfer the linear1 domain restrictions to another variable. for instance if the other constraint is of the form Y = abs(X) or Y = X^2, then a domain restriction on Y can be transferred to X. We can then move the extra constraint to the mapping model and remove one variable. This happens on the flatzinc celar problems for instance.

Definition at line 458 of file presolve_context.cc.

◆ VariableIsUnique()

bool operations_research::sat::PresolveContext::VariableIsUnique ( int ref ) const

Returns true if this ref only appear in one constraint.

Tricky: If this variable is equivalent to another one (but not the representative) and appear in just one constraint, then this constraint must be the affine defining one. And in this case the code using this function should do the proper stuff.

Definition at line 387 of file presolve_context.cc.

◆ VariableIsUniqueAndRemovable()

bool operations_research::sat::PresolveContext::VariableIsUniqueAndRemovable ( int ref ) const

Definition at line 393 of file presolve_context.cc.

◆ VariableWasRemoved()

bool operations_research::sat::PresolveContext::VariableWasRemoved ( int ref ) const

Note(user): I added an indirection and a function for this to be able to display debug information when this return false. This should actually never return false in the cases where it is used.

It is okay to reuse removed fixed variable.

Definition at line 429 of file presolve_context.cc.

◆ VariableWithCostIsUnique()

bool operations_research::sat::PresolveContext::VariableWithCostIsUnique ( int ref ) const

Same as VariableIsUniqueAndRemovable() except that in this case the variable also appear in the objective in addition to a single constraint.

Definition at line 397 of file presolve_context.cc.

◆ VariableWithCostIsUniqueAndRemovable()

bool operations_research::sat::PresolveContext::VariableWithCostIsUniqueAndRemovable ( int ref ) const

Tricky: Same remark as for VariableIsUniqueAndRemovable().

Also if the objective domain is constraining, we can't have a preferred direction, so we cannot easily remove such variable.

Definition at line 408 of file presolve_context.cc.

◆ VarToConstraints()

const absl::flat_hash_set< int > & operations_research::sat::PresolveContext::VarToConstraints ( int var ) const

inline

Definition at line 519 of file presolve_context.h.

◆ WriteObjectiveToProto()

void operations_research::sat::PresolveContext::WriteObjectiveToProto ( ) const

We need to sort the entries to be deterministic.

Note: –cpu_profile shows it is slightly faster to only compare key.

Definition at line 2111 of file presolve_context.cc.

◆ WriteVariableDomainsToProto()

void operations_research::sat::PresolveContext::WriteVariableDomainsToProto ( ) const

Some function need the domain to be up to date in the proto. This make sures our in-memory domain are writted back to the proto.

Definition at line 2145 of file presolve_context.cc.

Member Data Documentation

◆ deductions

DomainDeductions operations_research::sat::PresolveContext::deductions

Advanced presolve. See this class comment.

Definition at line 617 of file presolve_context.h.

◆ keep_all_feasible_solutions

bool operations_research::sat::PresolveContext::keep_all_feasible_solutions = false

Indicate if we are allowed to remove irrelevant feasible solution from the set of feasible solution. For example, if a variable is unused, can we fix it to an arbitrary value (or its mimimum objective one)? This must be true if the client wants to enumerate all solutions or wants correct tightened bounds in the response.

Definition at line 594 of file presolve_context.h.

◆ mapping_model

CpModelProto* operations_research::sat::PresolveContext::mapping_model = nullptr

Definition at line 587 of file presolve_context.h.

◆ modified_domains

SparseBitset<int> operations_research::sat::PresolveContext::modified_domains

Each time a domain is modified this is set to true.

Definition at line 610 of file presolve_context.h.

◆ num_presolve_operations

int64_t operations_research::sat::PresolveContext::num_presolve_operations = 0

Number of "rules" applied. This should be equal to the sum of all numbers in stats_by_rule_name. This is used to decide if we should do one more pass of the presolve or not. Note that depending on the presolve transformation, a rule can correspond to a tiny change or a big change. Because of that, this isn't a perfect proxy for the efficacy of the presolve.

Definition at line 601 of file presolve_context.h.

◆ tmp_left_domains

std::vector<Domain> operations_research::sat::PresolveContext::tmp_left_domains

Definition at line 606 of file presolve_context.h.

◆ tmp_literal_set

absl::flat_hash_set<int> operations_research::sat::PresolveContext::tmp_literal_set

Definition at line 607 of file presolve_context.h.

◆ tmp_literals

std::vector<int> operations_research::sat::PresolveContext::tmp_literals

Temporary storage.

Definition at line 604 of file presolve_context.h.

◆ tmp_term_domains

std::vector<Domain> operations_research::sat::PresolveContext::tmp_term_domains

Definition at line 605 of file presolve_context.h.

◆ var_with_reduced_small_degree

SparseBitset<int> operations_research::sat::PresolveContext::var_with_reduced_small_degree

Each time the constraint <-> variable graph is updated, we update this. A variable is added here iff its usage decreased and is now one or two.

Definition at line 614 of file presolve_context.h.

◆ working_model

CpModelProto* operations_research::sat::PresolveContext::working_model = nullptr

Definition at line 586 of file presolve_context.h.

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

ortools/sat/presolve_context.h
ortools/sat/presolve_context.cc

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ PresolveContext()

Member Function Documentation

◆ AddImplication()

◆ AddImplyInDomain()

◆ AddLiteralToObjective()

◆ AddToObjective()

◆ AddToObjectiveOffset()

◆ AffineRelationDebugString()

◆ CanBeUsedAsLiteral()

◆ CanonicalizeAffineVariable()

◆ CanonicalizeDomainOfSizeTwo()

◆ CanonicalizeLinearConstraint()

◆ CanonicalizeLinearExpression()

◆ CanonicalizeObjective()

◆ CanonicalizeOneObjectiveVariable()

◆ CanonicalizeVariable()

◆ CappedUpdateMinMaxActivity()

◆ ClearPrecedenceCache()

◆ ClearStats()

◆ ComputeMinMaxActivity()

◆ ConstraintIsInactive()

◆ ConstraintIsOptional()

◆ ConstraintToVars()

◆ ConstraintVariableGraphIsUpToDate()

◆ ConstraintVariableUsageIsConsistent()

◆ DomainContains() [1/2]

◆ DomainContains() [2/2]

◆ DomainIsEmpty()

◆ DomainOf()

◆ DomainOfVarIsIncludedIn()

◆ DomainSuperSetOf()

◆ EndMax()

◆ EndMin()

◆ ExploitExactlyOneInObjective()

◆ ExpressionIsAffineBoolean()

◆ ExpressionIsALiteral()

◆ ExpressionIsSingleVariable()

◆ FixedValue() [1/2]

◆ FixedValue() [2/2]

◆ GetAffineRelation()

◆ GetFalseLiteral()

◆ GetLiteralRepresentative()

◆ GetOrCreateAffineValueEncoding()

◆ GetOrCreateReifiedPrecedenceLiteral()

◆ GetOrCreateVarValueEncoding()

◆ GetReifiedPrecedenceKey()

◆ GetTrueLiteral()

◆ HasVarValueEncoding()

◆ InitializeNewDomains()

◆ InsertVarValueEncoding()

◆ IntersectDomainWith() [1/2]

◆ IntersectDomainWith() [2/2]

◆ IntervalDebugString()

◆ IntervalIsConstant()

◆ IntervalUsage()

◆ IsFixed() [1/2]

◆ IsFixed() [2/2]

◆ IsFullyEncoded() [1/2]

◆ IsFullyEncoded() [2/2]

◆ LiteralForExpressionMax()

◆ LiteralIsFalse()

◆ LiteralIsTrue()

◆ LoadSolutionHint()

◆ logger()

◆ LogInfo()

◆ MarkVariableAsRemoved()

◆ MaxOf() [1/2]

◆ MaxOf() [2/2]

◆ MinOf() [1/2]

◆ MinOf() [2/2]

◆ ModelIsExpanded()

◆ ModelIsUnsat()

◆ NewBoolVar()

◆ NewBoolVarWithClause()

◆ NewIntVar()

◆ NewIntVarWithDefinition()