#include <presolve_context.h>

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

int	NewIntVar (const Domain &domain)
	Helpers to adds new variables to the presolved model.

int	NewBoolVar (absl::string_view source)

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

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

int	NewBoolVarWithConjunction (absl::Span< const int > conjunction)

int	GetTrueLiteral ()

int	GetFalseLiteral ()

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

void	AddImplyInDomain (int b, int x, const Domain &domain)
	b => (x ∈ domain).

void	AddImplyInDomain (int b, const LinearExpressionProto &expr, const Domain &domain)
	b => (expr ∈ domain).

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

absl::Span< const Domain >	AllDomains () 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

std::optional< int64_t >	FixedValueOrNullopt (const LinearExpressionProto &expr) const
	This is faster than testing IsFixed() + FixedValue().

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 ()

bool	HasUnusedAffineVariable () const

void	CanonicalizeVariable (int ref)

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

bool	StoreAffineRelation (int var_x, int var_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 var)

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

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

void	ResetAfterCopy ()

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

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	RemoveNonRepresentativeAffineVariableIfUnused (int var)

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 ()

SolutionCrush &	solution_crush ()

bool	DebugTestHintFeasibility ()

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

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 95 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 97 of file presolve_context.h.

Member Function Documentation

◆ AddImplication()

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

a => b.

Definition at line 152 of file presolve_context.cc.

◆ AddImplyInDomain() [1/2]

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

b => (expr ∈ domain).

Definition at line 172 of file presolve_context.cc.

◆ AddImplyInDomain() [2/2]

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

b => (x ∈ 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 160 of file presolve_context.cc.

◆ AddLiteralToObjective()

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

Definition at line 2097 of file presolve_context.cc.

◆ AddToObjective()

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

Definition at line 2085 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 2114 of file presolve_context.cc.

◆ AffineRelationDebugString()

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

Definition at line 1333 of file presolve_context.cc.

◆ AllDomains()

absl::Span< const Domain > operations_research::sat::PresolveContext::AllDomains ( ) const

inline

Definition at line 158 of file presolve_context.h.

◆ CanBeUsedAsLiteral()

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

Definition at line 192 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 1019 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 1404 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 2661 of file presolve_context.cc.

◆ CanonicalizeLinearExpression()

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

Definition at line 2674 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 1957 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.

After we removed the variable from the objective it might have become a unused affine. Add it to the list of variables to check so we reprocess it.

Do the substitution.

Process new term.

Definition at line 1899 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 991 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 206 of file presolve_context.h.

◆ ClearPrecedenceCache()

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

Clear the precedence cache.

Definition at line 2455 of file presolve_context.cc.

◆ ClearStats()

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

Clears the "rules" statistics.

Definition at line 72 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 186 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 599 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 611 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 567 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 neighborhood, many constraints will be reduced significantly by this "simple" presolve.

Definition at line 757 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 795 of file presolve_context.cc.

◆ DebugTestHintFeasibility()

bool operations_research::sat::PresolveContext::DebugTestHintFeasibility ( )

This is slow O(problem_size) but can be used to debug presolve, either by pinpointing the transition from feasible to infeasible or the other way around if for some reason the presolve drop constraint that it shouldn't.

Definition at line 2772 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).

We assume expression is validated for overflow initially, and the code below should be overflow safe.

Definition at line 510 of file presolve_context.cc.

◆ DomainContains() [2/2]

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

Definition at line 503 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 182 of file presolve_context.cc.

◆ DomainOf()

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

Definition at line 493 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 245 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 288 of file presolve_context.cc.

◆ EndMax()

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

Definition at line 391 of file presolve_context.cc.

◆ EndMin()

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

Definition at line 385 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 2204 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 298 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 315 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 310 of file presolve_context.cc.

◆ FixedValue() [1/2]

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

Definition at line 267 of file presolve_context.cc.

◆ FixedValue() [2/2]

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

Definition at line 227 of file presolve_context.cc.

◆ FixedValueOrNullopt()

std::optional< int64_t > operations_research::sat::PresolveContext::FixedValueOrNullopt ( const LinearExpressionProto & expr ) const

This is faster than testing IsFixed() + FixedValue().

Definition at line 276 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 1319 of file presolve_context.cc.

◆ GetFalseLiteral()

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

Definition at line 149 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 1288 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 1810 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 2338 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.

Return the literal itself if this was called or canonicalized to a Boolean.

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 1729 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 2436 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 140 of file presolve_context.cc.

◆ HasUnusedAffineVariable()

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

Loop over all variable and return true if one of them is only used in affine relation and is not a representative. This is in O(num_vars) and only meant to be used in DCHECKs.

We can leave non-optimal stuff around if we reach the time limit.

Definition at line 774 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 1685 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 1350 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 1647 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 566 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 525 of file presolve_context.cc.

◆ IntervalDebugString()

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

Definition at line 347 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 338 of file presolve_context.cc.

◆ IntervalUsage()

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

inline

Definition at line 575 of file presolve_context.h.

◆ IsFixed() [1/2]

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

Definition at line 260 of file presolve_context.cc.

◆ IsFixed() [2/2]

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

Definition at line 186 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 1723 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 1715 of file presolve_context.cc.

◆ LiteralForExpressionMax()

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

Definition at line 304 of file presolve_context.cc.

◆ LiteralIsFalse()

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

Definition at line 206 of file presolve_context.cc.

◆ LiteralIsTrue()

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

Definition at line 197 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. Hint values outside the domain of their variable are adjusted to the nearest value in this domain. Missing hint values are completed when possible (e.g. for the model proto's fixed variables).

Definition at line 1377 of file presolve_context.cc.

◆ logger()

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

inline

Definition at line 638 of file presolve_context.h.

◆ LogInfo()

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

Logs stats to the logger.

Definition at line 2459 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 449 of file presolve_context.cc.

◆ MaxOf() [1/2]

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

Definition at line 247 of file presolve_context.cc.

◆ MaxOf() [2/2]

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

Definition at line 221 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 234 of file presolve_context.cc.

◆ MinOf() [2/2]

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

Definition at line 215 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 600 of file presolve_context.h.

◆ ModelIsUnsat()

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

inline

Definition at line 306 of file presolve_context.h.

◆ NewBoolVar()

int operations_research::sat::PresolveContext::NewBoolVar ( absl::string_view source )

Creates a new Boolean variable.

Warning: this does not set any hint value for the new variable.

Definition at line 122 of file presolve_context.cc.

◆ NewBoolVarWithClause()

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

Creates a new bool var. Its hint value is set to the value of the given clause.

Definition at line 127 of file presolve_context.cc.

◆ NewBoolVarWithConjunction()

int operations_research::sat::PresolveContext::NewBoolVarWithConjunction ( absl::Span< const int > conjunction )

Creates a new bool var. Its hint value is set to the value of the given conjunction.

Definition at line 133 of file presolve_context.cc.

◆ NewIntVar()

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

Helpers to adds new variables to the presolved model.

Creates a new integer variable with the given domain.

Warning: this does not set any hint value for the new variable.

Definition at line 74 of file presolve_context.cc.

◆ NewIntVarWithDefinition()

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

Creates a new integer variable with the given domain and definition. By default this also creates the linking constraint new_var = definition. Its hint value is set to the value of the definition. Returns -1 if we couldn't create the definition due to overflow.

Create new linear constraint new_var = definition.

Todo: (user): When we encounter overflow (rare), we still create a variable.

Definition at line 81 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 2683 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 2693 of file presolve_context.cc.

◆ NotifyThatModelIsExpanded()

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

inline

Definition at line 601 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 299 of file presolve_context.h.

◆ NumAffineRelations()

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

inline

Used for statistics.

Definition at line 382 of file presolve_context.h.

◆ ObjectiveCoeff()

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

inline

Definition at line 538 of file presolve_context.h.

◆ ObjectiveDomain()

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

inline

Objective getters.

Definition at line 534 of file presolve_context.h.

◆ ObjectiveDomainIsConstraining()

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

inline

Returns false if the variables in the objective with a positive (resp. negative) coefficient can freely decrease (resp. increase) within their domain (if we ignore the other constraints). Otherwise, returns true.

Definition at line 547 of file presolve_context.h.

◆ ObjectiveMap()

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

inline

Definition at line 535 of file presolve_context.h.

◆ params()

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

inline

Definition at line 639 of file presolve_context.h.

◆ PropagateAffineRelation() [1/2]

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

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

Definition at line 902 of file presolve_context.cc.

◆ PropagateAffineRelation() [2/2]

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

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

Definition at line 909 of file presolve_context.cc.

◆ random()

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

inline

Definition at line 641 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.

Todo: (user): There should be no negative reference here !

We remove fixed terms as we read the objective. This can help a lot on LNS problems with a large proportions of fixed terms.

Definition at line 1829 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 2060 of file presolve_context.cc.

◆ RefDebugString()

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

To facilitate debugging.

Definition at line 1328 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 591 of file presolve_context.h.

◆ RemoveAllVariablesFromAffineRelationConstraint()

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

Definition at line 932 of file presolve_context.cc.

◆ RemoveNonRepresentativeAffineVariableIfUnused()

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

If var is an unused variable in an affine relation and is not a representative, we can remove it from the model. Note that this requires the variable usage graph to be up to date.

Add relation with current representative to the mapping model.

Definition at line 938 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 963 of file presolve_context.cc.

◆ RemoveVariableFromObjective()

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

Allows to manipulate the objective coefficients.

Definition at line 2078 of file presolve_context.cc.

◆ ResetAfterCopy()

void operations_research::sat::PresolveContext::ResetAfterCopy ( )

This is a bit hacky. Clear some fields. See call site.

Todo: (user): The ModelCopier should probably not depend on the full context it only need to read/write domains and call UpdateRuleStats(), so we might want to split that part out so that we can just initialize the full context later. Alternatively, we could just move more complex part of the context out, like the graph, the encoding, the affine representative, and so on to individual and easier to manage classes.

Definition at line 1339 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 589 of file presolve_context.cc.

◆ SetLiteralToTrue()

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

Definition at line 595 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 2226 of file presolve_context.cc.

◆ SizeMax()

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

Definition at line 403 of file presolve_context.cc.

◆ SizeMin()

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

Definition at line 397 of file presolve_context.cc.

◆ solution_crush()

SolutionCrush & operations_research::sat::PresolveContext::solution_crush ( )

inline

Definition at line 632 of file presolve_context.h.

◆ StartMax()

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

Definition at line 379 of file presolve_context.cc.

◆ StartMin()

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

Definition at line 373 of file presolve_context.cc.

◆ StoreAffineRelation()

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

Adds the relation (var_x = coeff * var_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 var_x and var_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).

Sets var_y's value to the solution of "var_x's value - coeff * var_y's value = offset".

Todo: (user): I am not 100% sure why, but sometimes the representative is fixed but that is not propagated to var_x or var_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:

var_x = coeff * var_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 1083 of file presolve_context.cc.

◆ StoreBooleanEqualityRelation()

ABSL_MUST_USE_RESULT 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 1261 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.

The literal cannot be true.

Definition at line 1665 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.

The constraint is trivial.

Definition at line 1675 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 2127 of file presolve_context.cc.

◆ time_limit()

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

inline

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

◆ UpdateNewConstraintsVariableUsage()

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

Calls UpdateConstraintVariableUsage() on all newly created constraints.

Definition at line 762 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 621 of file presolve_context.cc.

◆ 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 444 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 475 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 485 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 413 of file presolve_context.cc.

◆ VariableIsUniqueAndRemovable()

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

Definition at line 419 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 456 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 424 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 435 of file presolve_context.cc.

◆ VarToConstraints()

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

inline

Definition at line 571 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 2298 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 written back to the proto.

Definition at line 2332 of file presolve_context.cc.

Member Data Documentation

◆ deductions

DomainDeductions operations_research::sat::PresolveContext::deductions

Advanced presolve. See this class comment.

Definition at line 667 of file presolve_context.h.

◆ mapping_model

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

Definition at line 644 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 660 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 651 of file presolve_context.h.

◆ tmp_left_domains

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

Definition at line 656 of file presolve_context.h.

◆ tmp_literal_set

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

Definition at line 657 of file presolve_context.h.

◆ tmp_literals

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

Temporary storage.

Definition at line 654 of file presolve_context.h.

◆ tmp_term_domains

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

Definition at line 655 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 664 of file presolve_context.h.

◆ working_model

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

Definition at line 643 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() [1/2]

◆ AddImplyInDomain() [2/2]

◆ AddLiteralToObjective()

◆ AddToObjective()

◆ AddToObjectiveOffset()

◆ AffineRelationDebugString()

◆ AllDomains()

◆ CanBeUsedAsLiteral()

◆ CanonicalizeAffineVariable()

◆ CanonicalizeDomainOfSizeTwo()

◆ CanonicalizeLinearConstraint()

◆ CanonicalizeLinearExpression()

◆ CanonicalizeObjective()

◆ CanonicalizeOneObjectiveVariable()

◆ CanonicalizeVariable()

◆ CappedUpdateMinMaxActivity()

◆ ClearPrecedenceCache()

◆ ClearStats()

◆ ComputeMinMaxActivity()

◆ ConstraintIsInactive()

◆ ConstraintIsOptional()

◆ ConstraintToVars()

◆ ConstraintVariableGraphIsUpToDate()

◆ ConstraintVariableUsageIsConsistent()

◆ DebugTestHintFeasibility()

◆ DomainContains() [1/2]

◆ DomainContains() [2/2]

◆ DomainIsEmpty()

◆ DomainOf()

◆ DomainOfVarIsIncludedIn()

◆ DomainSuperSetOf()

◆ EndMax()

◆ EndMin()

◆ ExploitExactlyOneInObjective()

◆ ExpressionIsAffineBoolean()

◆ ExpressionIsALiteral()

◆ ExpressionIsSingleVariable()

◆ FixedValue() [1/2]

◆ FixedValue() [2/2]

◆ FixedValueOrNullopt()

◆ GetAffineRelation()

◆ GetFalseLiteral()

◆ GetLiteralRepresentative()

◆ GetOrCreateAffineValueEncoding()

◆ GetOrCreateReifiedPrecedenceLiteral()

◆ GetOrCreateVarValueEncoding()

◆ GetReifiedPrecedenceKey()

◆ GetTrueLiteral()

◆ HasUnusedAffineVariable()

◆ 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()