#include <solution_crush.h>

Classes
struct	BoxInAreaLiteral

struct	StateVar
	Represents `var` = "automaton is in state `state` at time `time`". More...

struct	TableRowLiteral

struct	TransitionVar

Public Member Functions
	SolutionCrush ()=default

	SolutionCrush (const SolutionCrush &)=delete
	SolutionCrush is neither copyable nor movable.

	SolutionCrush (SolutionCrush &&)=delete

SolutionCrush &	operator= (const SolutionCrush &)=delete

SolutionCrush &	operator= (SolutionCrush &&)=delete

bool	SolutionIsLoaded () const

absl::Span< const int64_t >	GetVarValues () const
	Visible for testing.

void	LoadSolution (int num_vars, const absl::flat_hash_map< int, int64_t > &solution)

void	Resize (int new_size)

void	MaybeSetLiteralToValueEncoding (int literal, int var, int64_t value)

void	SetVarToLinearExpression (int var, absl::Span< const std::pair< int, int64_t > > linear, int64_t offset=0)

void	SetVarToLinearExpression (int var, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t offset=0)

void	SetVarToClause (int var, absl::Span< const int > clause)

void	SetVarToConjunction (int var, absl::Span< const int > conjunction)

void	SetVarToValueIfLinearConstraintViolated (int var, int64_t value, absl::Span< const std::pair< int, int64_t > > linear, const Domain &domain)

void	SetLiteralToValueIfLinearConstraintViolated (int literal, bool value, absl::Span< const std::pair< int, int64_t > > linear, const Domain &domain)

void	SetVarToValueIf (int var, int64_t value, int condition_lit)
	Sets the value of `var` to `value` if the value of `condition_lit` is true.

void	SetVarToLinearExpressionIf (int var, const LinearExpressionProto &expr, int condition_lit)

void	SetLiteralToValueIf (int literal, bool value, int condition_lit)

void	SetVarToConditionalValue (int var, absl::Span< const int > condition_lits, int64_t value_if_true, int64_t value_if_false)

void	MakeLiteralsEqual (int lit1, int lit2)

void	SetOrUpdateVarToDomain (int var, const Domain &domain)

void	UpdateLiteralsToFalseIfDifferent (int lit1, int lit2)

void	UpdateLiteralsWithDominance (int lit, int dominating_lit)

void	UpdateRefsWithDominance (int ref, int64_t min_value, int64_t max_value, absl::Span< const std::pair< int, Domain > > dominating_refs)

void	MaybeUpdateVarWithSymmetriesToValue (int var, bool value, absl::Span< const std::unique_ptr< SparsePermutation > > generators)

void	SetVarToLinearConstraintSolution (std::optional< int > var_index, absl::Span< const int > vars, absl::Span< const int64_t > coeffs, int64_t rhs)

void	SetReservoirCircuitVars (const ReservoirConstraintProto &reservoir, int64_t min_level, int64_t max_level, absl::Span< const int > level_vars, const CircuitConstraintProto &circuit)

void	SetVarToReifiedPrecedenceLiteral (int var, const LinearExpressionProto &time_i, const LinearExpressionProto &time_j, int active_i, int active_j)

void	SetIntModExpandedVars (const ConstraintProto &ct, int div_var, int prod_var, int64_t default_div_value, int64_t default_prod_value)

void	SetIntProdExpandedVars (const LinearArgumentProto &int_prod, absl::Span< const int > prod_vars)

void	SetLinMaxExpandedVars (const LinearArgumentProto &lin_max, absl::Span< const int > enforcement_lits)

void	SetAutomatonExpandedVars (const AutomatonConstraintProto &automaton, absl::Span< const StateVar > state_vars, absl::Span< const TransitionVar > transition_vars)

void	SetTableExpandedVars (absl::Span< const int > column_vars, absl::Span< const int > existing_row_lits, absl::Span< const TableRowLiteral > new_row_lits)

void	SetLinearWithComplexDomainExpandedVars (const LinearConstraintProto &linear, absl::Span< const int > bucket_lits)

void	StoreSolutionAsHint (CpModelProto &model) const
	Stores the solution as a hint in the given model.

void	AssignVariableToPackingArea (const CompactVectorVector< int, Rectangle > &areas, const CpModelProto &model, absl::Span< const int > x_intervals, absl::Span< const int > y_intervals, absl::Span< const BoxInAreaLiteral > box_in_area_lits)

Detailed Description

Transforms (or "crushes") solutions of the initial model into solutions of the presolved model.

Note: partial solution crushing is not a priority: as of Jan 2025, most methods of this class do nothing if some solution values are missing to perform their work. If one just want to complete a partial solution to a full one for convenience, it should be relatively easy to first solve a feasibility model where all hinted variables are fixed, and use the solution to that problem as a starting hint.

Note also that if the initial "solution" is incomplete or infeasible, the crushed "solution" might contain values outside of the domain of their variables. Consider for instance two constraints "b => v=1" and "!b => v=2", presolved into "v = b+1", with SetVarToLinearConstraintSolution called to set b's value from v's value. If the initial solution is infeasible, with v=0, this will set b to -1, which is outside of its [0,1] domain.

Definition at line 52 of file solution_crush.h.

Constructor & Destructor Documentation

◆ SolutionCrush() [1/3]

operations_research::sat::SolutionCrush::SolutionCrush ( )

default

◆ SolutionCrush() [2/3]

operations_research::sat::SolutionCrush::SolutionCrush ( const SolutionCrush & )

delete

SolutionCrush is neither copyable nor movable.

◆ SolutionCrush() [3/3]

operations_research::sat::SolutionCrush::SolutionCrush ( SolutionCrush && )

delete

Member Function Documentation

◆ AssignVariableToPackingArea()

void operations_research::sat::SolutionCrush::AssignVariableToPackingArea	(	const CompactVectorVector< int, Rectangle > &	areas,
		const CpModelProto &	model,
		absl::Span< const int >	x_intervals,
		absl::Span< const int >	y_intervals,
		absl::Span< const BoxInAreaLiteral >	box_in_area_lits )

Definition at line 628 of file solution_crush.cc.

◆ GetVarValues()

absl::Span< const int64_t > operations_research::sat::SolutionCrush::GetVarValues ( ) const

inline

Visible for testing.

Definition at line 65 of file solution_crush.h.

◆ LoadSolution()

void operations_research::sat::SolutionCrush::LoadSolution	(	int	num_vars,
		const absl::flat_hash_map< int, int64_t > &	solution )

Sets the given values in the solution. solution must be a map from variable indices to variable values. This must be called only once, before any other method.

Definition at line 44 of file solution_crush.cc.

◆ MakeLiteralsEqual()

void operations_research::sat::SolutionCrush::MakeLiteralsEqual	(	int	lit1,
		int	lit2 )

If one literal does not have a value, and the other one does, sets the value of the latter to the value of the former. If both literals have a value, sets the value of lit1 to the value of lit2.

Definition at line 209 of file solution_crush.cc.

◆ MaybeSetLiteralToValueEncoding()

void operations_research::sat::SolutionCrush::MaybeSetLiteralToValueEncoding	(	int	literal,
		int	var,
		int64_t	value )

Sets the value of literal to "`var`'s value == `value`". Does nothing if literal already has a value.

Definition at line 64 of file solution_crush.cc.

◆ MaybeUpdateVarWithSymmetriesToValue()

void operations_research::sat::SolutionCrush::MaybeUpdateVarWithSymmetriesToValue	(	int	var,
		bool	value,
		absl::Span< const std::unique_ptr< SparsePermutation > >	generators )

If var's value != value finds another variable in the orbit of var that can take that value, and permute the solution (using the symmetry generators) so that this other variable is at position var. If no other variable can be found, does nothing.

Definition at line 249 of file solution_crush.cc.

◆ operator=() [1/2]

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

delete

◆ operator=() [2/2]

SolutionCrush & operations_research::sat::SolutionCrush::operator= ( SolutionCrush && )

delete

◆ Resize()

void operations_research::sat::SolutionCrush::Resize ( int new_size )

Resizes the solution to contain new_size variables. Does not change the value of existing variables, and does not set any value for the new variables.

Warning: the methods below do not automatically resize the solution. To set the value of a new variable with one of them, call this method first.

Definition at line 58 of file solution_crush.cc.

◆ SetAutomatonExpandedVars()

void operations_research::sat::SolutionCrush::SetAutomatonExpandedVars	(	const AutomatonConstraintProto &	automaton,
		absl::Span< const StateVar >	state_vars,
		absl::Span< const TransitionVar >	transition_vars )

Sets the value of state_vars and transition_vars if all the variables in automaton have a value.

Definition at line 527 of file solution_crush.cc.

◆ SetIntModExpandedVars()

void operations_research::sat::SolutionCrush::SetIntModExpandedVars	(	const ConstraintProto &	ct,
		int	div_var,
		int	prod_var,
		int64_t	default_div_value,
		int64_t	default_prod_value )

Sets the value of div_var and prod_var if all the variables in the IntMod ct constraint have a value, assuming that this "target = x % m" constraint is expanded into "div_var = x / m", "prod_var = div_var * m", and "target = x - prod_var" constraints. If ct is not enforced, sets the values of div_var and prod_var to default_div_value and default_prod_value, respectively.

target_expr_value should be equal to "expr_value % mod_expr_value".

Definition at line 456 of file solution_crush.cc.

◆ SetIntProdExpandedVars()

void operations_research::sat::SolutionCrush::SetIntProdExpandedVars	(	const LinearArgumentProto &	int_prod,
		absl::Span< const int >	prod_vars )

Sets the value of as many variables in prod_vars as possible (depending on how many expressions in int_prod have a value), assuming that the int_prod constraint "target = x_0 * x_1 * ... * x_n" is expanded into "prod_var_1 = x_0 * x1", "prod_var_2 = prod_var_1 * x_2", ..., "prod_var_(n-1) = prod_var_(n-2) * x_(n-1)", and "target = prod_var_(n-1) * x_n" constraints.

Definition at line 489 of file solution_crush.cc.

◆ SetLinearWithComplexDomainExpandedVars()

void operations_research::sat::SolutionCrush::SetLinearWithComplexDomainExpandedVars	(	const LinearConstraintProto &	linear,
		absl::Span< const int >	bucket_lits )

Sets the value of bucket_lits if all the variables in linear have a value, assuming that they are expanded from the complex linear constraint (i.e. one whose domain has two or more intervals). The value of bucket_lits[i] is set to 1 iff the value of the linear expression is in the i-th interval of the domain.

Definition at line 594 of file solution_crush.cc.

◆ SetLinMaxExpandedVars()

void operations_research::sat::SolutionCrush::SetLinMaxExpandedVars	(	const LinearArgumentProto &	lin_max,
		absl::Span< const int >	enforcement_lits )

Sets the value of enforcement_lits if all the variables in lin_max have a value, assuming that the lin_max constraint "target = max(x_0, x_1, ..., x_(n-1))" is expanded into "enforcement_lits[i] => target <= x_i" constraints, with at most one enforcement value equal to true. enforcement_lits must have as many elements as lin_max.

Definition at line 504 of file solution_crush.cc.

◆ SetLiteralToValueIf()

void operations_research::sat::SolutionCrush::SetLiteralToValueIf	(	int	literal,
		bool	value,
		int	condition_lit )

Sets the value of literal to value if the value of condition_lit is true.

Definition at line 187 of file solution_crush.cc.

◆ SetLiteralToValueIfLinearConstraintViolated()

void operations_research::sat::SolutionCrush::SetLiteralToValueIfLinearConstraintViolated	(	int	literal,
		bool	value,
		absl::Span< const std::pair< int, int64_t > >	linear,
		const Domain &	domain )

Sets the value of literal to value if the value of the given linear expression is not in domain (or does nothing otherwise). linear must be a list of (variable index, coefficient) pairs.

Definition at line 162 of file solution_crush.cc.

◆ SetOrUpdateVarToDomain()

void operations_research::sat::SolutionCrush::SetOrUpdateVarToDomain	(	int	var,
		const Domain &	domain )

If var already has a value, updates it to be within the given domain. Otherwise, if the domain is fixed, sets the value of var to this fixed value. Otherwise does nothing.

Definition at line 218 of file solution_crush.cc.

◆ SetReservoirCircuitVars()

void operations_research::sat::SolutionCrush::SetReservoirCircuitVars	(	const ReservoirConstraintProto &	reservoir,
		int64_t	min_level,
		int64_t	max_level,
		absl::Span< const int >	level_vars,
		const CircuitConstraintProto &	circuit )

Sets the value of the variables in level_vars and in circuit if all the variables in reservoir have a value. This assumes that there is one level variable and one circuit node per element in reservoir (in the same order) – plus one last node representing the start and end of the circuit.

The values of the active events, in the order they should appear in the circuit. The values are collected first, and sorted later.

Update the level_vars values by computing the level at each active event.

Adjust the order of the events occurring at the same time, in the circuit, so that, at each node, the level is between var_min and var_max. For instance, if e1 = {t, +1} and e2 = {t, -1}, and if current_level = 0, var_min = -1 and var_max = 0, then e2 must occur before e1.

The index of each event in active_event_values, or -1 if the event's "active" value is false.

Self-arc on the start and end node.

Arc from the start node to an event node.

Arc from an event node to the end node.

Arc between two different event nodes.

Definition at line 350 of file solution_crush.cc.

◆ SetTableExpandedVars()

void operations_research::sat::SolutionCrush::SetTableExpandedVars	(	absl::Span< const int >	column_vars,
		absl::Span< const int >	existing_row_lits,
		absl::Span< const TableRowLiteral >	new_row_lits )

Sets the value of the new_row_lits literals if all the variables in column_vars and existing_row_lits have a value. For each row_lits, column_values must have the same size as column_vars. This method assumes that exactly one of existing_row_lits and new_row_lits must be true.

Definition at line 564 of file solution_crush.cc.

◆ SetVarToClause()

void operations_research::sat::SolutionCrush::SetVarToClause	(	int	var,
		absl::Span< const int >	clause )

Sets the value of var to 1 if the value of at least one literal in clause is equal to 1 (or to 0 otherwise). clause must be a list of literal indices.

Leave the new_var unassigned if any literal is unassigned.

Definition at line 101 of file solution_crush.cc.

◆ SetVarToConditionalValue()

void operations_research::sat::SolutionCrush::SetVarToConditionalValue	(	int	var,
		absl::Span< const int >	condition_lits,
		int64_t	value_if_true,
		int64_t	value_if_false )

Sets the value of var to value_if_true if the value of all the condition_lits literals is true, and to value_if_false otherwise.

Definition at line 194 of file solution_crush.cc.

◆ SetVarToConjunction()

void operations_research::sat::SolutionCrush::SetVarToConjunction	(	int	var,
		absl::Span< const int >	conjunction )

Sets the value of var to 1 if the value of all the literals in conjunction is 1 (or to 0 otherwise). conjunction must be a list of literal indices.

Leave the new_var unassigned if any literal is unassigned.

Definition at line 122 of file solution_crush.cc.

◆ SetVarToLinearConstraintSolution()

void operations_research::sat::SolutionCrush::SetVarToLinearConstraintSolution	(	std::optional< int >	var_index,
		absl::Span< const int >	vars,
		absl::Span< const int64_t >	coeffs,
		int64_t	rhs )

Sets the value of the i-th variable in vars so that the given constraint "dotproduct(coeffs, vars values) = rhs" is satisfied, if all the other variables have a value. i is equal to var_index if set. Otherwise it is the index of the variable without a value (if there is not exactly one, this method does nothing).

Definition at line 315 of file solution_crush.cc.

◆ SetVarToLinearExpression() [1/2]

void operations_research::sat::SolutionCrush::SetVarToLinearExpression	(	int	var,
		absl::Span< const int >	vars,
		absl::Span< const int64_t >	coeffs,
		int64_t	offset = 0 )

Sets the value of var to the value of the given linear expression. The two spans must have the same size.

Definition at line 85 of file solution_crush.cc.

◆ SetVarToLinearExpression() [2/2]

void operations_research::sat::SolutionCrush::SetVarToLinearExpression	(	int	var,
		absl::Span< const std::pair< int, int64_t > >	linear,
		int64_t	offset = 0 )

Sets the value of var to the value of the given linear expression, if all the variables in this expression have a value. linear must be a list of (variable index, coefficient) pairs.

Definition at line 73 of file solution_crush.cc.

◆ SetVarToLinearExpressionIf()

void operations_research::sat::SolutionCrush::SetVarToLinearExpressionIf	(	int	var,
		const LinearExpressionProto &	expr,
		int	condition_lit )

Sets the value of var to the value expr if the value of condition_lit is true.

Definition at line 176 of file solution_crush.cc.

◆ SetVarToReifiedPrecedenceLiteral()

void operations_research::sat::SolutionCrush::SetVarToReifiedPrecedenceLiteral	(	int	var,
		const LinearExpressionProto &	time_i,
		const LinearExpressionProto &	time_j,
		int	active_i,
		int	active_j )

Sets the value of var to "`time_i`'s value <= `time_j`'s value && `active_i`'s value == true && `active_j`'s value == true".

Definition at line 439 of file solution_crush.cc.

◆ SetVarToValueIf()

void operations_research::sat::SolutionCrush::SetVarToValueIf	(	int	var,
		int64_t	value,
		int	condition_lit )

Sets the value of var to value if the value of condition_lit is true.

Definition at line 170 of file solution_crush.cc.

◆ SetVarToValueIfLinearConstraintViolated()

void operations_research::sat::SolutionCrush::SetVarToValueIfLinearConstraintViolated	(	int	var,
		int64_t	value,
		absl::Span< const std::pair< int, int64_t > >	linear,
		const Domain &	domain )

Sets the value of var to value if the value of the given linear expression is not in domain (or does nothing otherwise). linear must be a list of (variable index, coefficient) pairs.

Definition at line 144 of file solution_crush.cc.

◆ SolutionIsLoaded()

bool operations_research::sat::SolutionCrush::SolutionIsLoaded ( ) const

inline

Definition at line 62 of file solution_crush.h.

◆ StoreSolutionAsHint()

void operations_research::sat::SolutionCrush::StoreSolutionAsHint ( CpModelProto & model ) const

Stores the solution as a hint in the given model.

Definition at line 611 of file solution_crush.cc.

◆ UpdateLiteralsToFalseIfDifferent()

void operations_research::sat::SolutionCrush::UpdateLiteralsToFalseIfDifferent	(	int	lit1,
		int	lit2 )

Updates the value of the given literals to false if their current values are different (or does nothing otherwise).

Set lit1 and lit2 to false if "lit1 - lit2 == 0" is violated.

Definition at line 227 of file solution_crush.cc.

◆ UpdateLiteralsWithDominance()

void operations_research::sat::SolutionCrush::UpdateLiteralsWithDominance	(	int	lit,
		int	dominating_lit )

Decrements the value of lit and increments the value of dominating_lit if their values are equal to 1 and 0, respectively.

Definition at line 238 of file solution_crush.cc.

◆ UpdateRefsWithDominance()

void operations_research::sat::SolutionCrush::UpdateRefsWithDominance	(	int	ref,
		int64_t	min_value,
		int64_t	max_value,
		absl::Span< const std::pair< int, Domain > >	dominating_refs )

Decrements the value of ref by the minimum amount necessary to be in [min_value, max_value], and increments the value of one or more dominating_refs by the same total amount (or less if it is not possible to exactly match this amount), while staying within their respective domains. The value of a negative reference index r is the opposite of the value of the variable PositiveRef(r).

min_value must be the minimum value of ref's current domain D, and max_value must be in D.

This can happen if the solution is not initially feasible (in which case we can't fix it).

If the value is already in the new domain there is nothing to do.

The quantity to subtract from the value of ref.

This might happen if the solution is not initially feasible.

Definition at line 284 of file solution_crush.cc.

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

ortools/sat/solution_crush.h
ortools/sat/solution_crush.cc

Classes

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ SolutionCrush() [1/3]

◆ SolutionCrush() [2/3]

◆ SolutionCrush() [3/3]

Member Function Documentation

◆ AssignVariableToPackingArea()

◆ GetVarValues()

◆ LoadSolution()

◆ MakeLiteralsEqual()

◆ MaybeSetLiteralToValueEncoding()

◆ MaybeUpdateVarWithSymmetriesToValue()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ Resize()

◆ SetAutomatonExpandedVars()

◆ SetIntModExpandedVars()

◆ SetIntProdExpandedVars()

◆ SetLinearWithComplexDomainExpandedVars()

◆ SetLinMaxExpandedVars()

◆ SetLiteralToValueIf()

◆ SetLiteralToValueIfLinearConstraintViolated()

◆ SetOrUpdateVarToDomain()

◆ SetReservoirCircuitVars()

◆ SetTableExpandedVars()

◆ SetVarToClause()

◆ SetVarToConditionalValue()

◆ SetVarToConjunction()

◆ SetVarToLinearConstraintSolution()

◆ SetVarToLinearExpression() [1/2]

◆ SetVarToLinearExpression() [2/2]

◆ SetVarToLinearExpressionIf()

◆ SetVarToReifiedPrecedenceLiteral()

◆ SetVarToValueIf()

◆ SetVarToValueIfLinearConstraintViolated()

◆ SolutionIsLoaded()

◆ StoreSolutionAsHint()

◆ UpdateLiteralsToFalseIfDifferent()

◆ UpdateLiteralsWithDominance()

◆ UpdateRefsWithDominance()