#include <pb_constraint.h>

Public Member Functions
void	ClearAndResize (int num_variables)

void	ClearAll ()

Coefficient	GetCoefficient (BooleanVariable var) const
	Returns the coefficient (>= 0) of the given variable.

Literal	GetLiteral (BooleanVariable var) const

void	ReduceCoefficients ()

void	ReduceGivenCoefficient (BooleanVariable var)

Coefficient	ComputeSlackForTrailPrefix (const Trail &trail, int trail_index) const

Coefficient	ReduceCoefficientsAndComputeSlackForTrailPrefix (const Trail &trail, int trail_index)

void	ReduceSlackTo (const Trail &trail, int trail_index, Coefficient initial_slack, Coefficient target)

void	CopyIntoVector (std::vector< LiteralWithCoeff > *output)
	Copies this constraint into a vector<LiteralWithCoeff> representation.

void	AddToRhs (Coefficient value)
	Adds a non-negative value to this constraint Rhs().

Coefficient	Rhs () const

Coefficient	MaxSum () const

void	AddTerm (Literal literal, Coefficient coeff)

Coefficient	CancelationAmount (Literal literal, Coefficient coeff) const
	Returns the "cancelation" amount of AddTerm(literal, coeff).

const std::vector< BooleanVariable > &	PossibleNonZeros () const

std::string	DebugString ()
	Returns a string representation of the constraint.

Detailed Description

Encode a constraint sum term <= rhs, where each term is a positive Coefficient times a literal. This class allows efficient modification of the constraint and is used during pseudo-Boolean resolution.

Definition at line 186 of file pb_constraint.h.

Member Function Documentation

◆ AddTerm()

void operations_research::sat::MutableUpperBoundedLinearConstraint::AddTerm	(	Literal	literal,
		Coefficient	coeff )

inline

Adds a term to this constraint. This is in the .h for efficiency. The encoding used internally is described below in the terms_ comment.

The two terms are of opposite sign, a "cancelation" happens. We need to change the encoding of the lower magnitude term.

If term > 0, term . x -> term . (x - 1) + term
If term < 0, term . (x - 1) -> term . x - term In both cases, rhs -= abs(term).

Both terms are of the same sign (or terms_[var] is zero).

Definition at line 286 of file pb_constraint.h.

◆ AddToRhs()

void operations_research::sat::MutableUpperBoundedLinearConstraint::AddToRhs ( Coefficient value )

inline

Adds a non-negative value to this constraint Rhs().

Definition at line 277 of file pb_constraint.h.

◆ CancelationAmount()

Coefficient operations_research::sat::MutableUpperBoundedLinearConstraint::CancelationAmount	(	Literal	literal,
		Coefficient	coeff ) const

inline

Returns the "cancelation" amount of AddTerm(literal, coeff).

Definition at line 309 of file pb_constraint.h.

◆ ClearAll()

void operations_research::sat::MutableUpperBoundedLinearConstraint::ClearAll ( )

Reset the constraint to 0 <= 0.

Note: the constraint size stays the same.

Todo: (user): We could be more efficient and have only one loop here.

Definition at line 264 of file pb_constraint.cc.

◆ ClearAndResize()

void operations_research::sat::MutableUpperBoundedLinearConstraint::ClearAndResize ( int num_variables )

This must be called before any other functions is used with an higher variable index.

Definition at line 253 of file pb_constraint.cc.

◆ ComputeSlackForTrailPrefix()

Coefficient operations_research::sat::MutableUpperBoundedLinearConstraint::ComputeSlackForTrailPrefix	(	const Trail &	trail,
		int	trail_index ) const

Compute the constraint slack assuming that only the variables with index < trail_index are assigned.

Todo: (user): Keep this for DCHECK(), but maintain the slack incrementally instead of recomputing it.

Definition at line 304 of file pb_constraint.cc.

◆ CopyIntoVector()

void operations_research::sat::MutableUpperBoundedLinearConstraint::CopyIntoVector ( std::vector< LiteralWithCoeff > * output )

Copies this constraint into a vector<LiteralWithCoeff> representation.

Definition at line 384 of file pb_constraint.cc.

◆ DebugString()

std::string operations_research::sat::MutableUpperBoundedLinearConstraint::DebugString ( )

Returns a string representation of the constraint.

Definition at line 291 of file pb_constraint.cc.

◆ GetCoefficient()

Coefficient operations_research::sat::MutableUpperBoundedLinearConstraint::GetCoefficient ( BooleanVariable var ) const

inline

Returns the coefficient (>= 0) of the given variable.

Definition at line 197 of file pb_constraint.h.

◆ GetLiteral()

Literal operations_research::sat::MutableUpperBoundedLinearConstraint::GetLiteral ( BooleanVariable var ) const

inline

Returns the literal under which the given variable appear in the constraint. Note that if GetCoefficient(var) == 0 this just returns Literal(var, true).

Definition at line 204 of file pb_constraint.h.

◆ MaxSum()

Coefficient operations_research::sat::MutableUpperBoundedLinearConstraint::MaxSum ( ) const

inline

Definition at line 282 of file pb_constraint.h.

◆ PossibleNonZeros()

const std::vector< BooleanVariable > & operations_research::sat::MutableUpperBoundedLinearConstraint::PossibleNonZeros ( ) const

inline

Returns a set of positions that contains all the non-zeros terms of the constraint. Note that this set can also contains some zero terms.

Definition at line 318 of file pb_constraint.h.

◆ ReduceCoefficients()

void operations_research::sat::MutableUpperBoundedLinearConstraint::ReduceCoefficients ( )

If we have a lower bounded constraint sum terms >= rhs, then it is trivial to see that the coefficient of any term can be reduced to rhs if it is bigger. This does exactly this operation, but on the upper bounded representation.

If we take a constraint sum ci.xi <= rhs, take its negation and add max_sum on both side, we have sum ci.(1 - xi) >= max_sum - rhs So every ci > (max_sum - rhs) can be replacend by (max_sum - rhs). Not that this operation also change the original rhs of the constraint.

Todo: (user): Also reduce the trivially false literal when coeff > rhs_ ?

Definition at line 275 of file pb_constraint.cc.

◆ ReduceCoefficientsAndComputeSlackForTrailPrefix()

Coefficient operations_research::sat::MutableUpperBoundedLinearConstraint::ReduceCoefficientsAndComputeSlackForTrailPrefix	(	const Trail &	trail,
		int	trail_index )

Same as ReduceCoefficients() followed by ComputeSlackForTrailPrefix(). It allows to loop only once over all the terms of the constraint instead of doing it twice. This helps since doing that can be the main bottleneck.

Note: this function assumes that the returned slack will be negative. This allow to DCHECK some assumptions on what coefficients can be reduced or not.

Todo: (user): Ideally the slack should be maitainable incrementally.

Because we assume the slack (rhs - activity) to be negative, we have coeff + rhs - max_sum_ <= coeff + rhs - (activity + coeff) <= slack < 0

Definition at line 317 of file pb_constraint.cc.

◆ ReduceGivenCoefficient()

void operations_research::sat::MutableUpperBoundedLinearConstraint::ReduceGivenCoefficient ( BooleanVariable var )

inline

Same as ReduceCoefficients() but only consider the coefficient of the given variable.

Definition at line 221 of file pb_constraint.h.

◆ ReduceSlackTo()

void operations_research::sat::MutableUpperBoundedLinearConstraint::ReduceSlackTo	(	const Trail &	trail,
		int	trail_index,
		Coefficient	initial_slack,
		Coefficient	target )

Relaxes the constraint so that:

ComputeSlackForTrailPrefix(trail, trail_index) == target;
All the variables that were propagated given the assignment < trail_index are still propagated.

As a precondition, ComputeSlackForTrailPrefix(trail, trail_index) >= target

Note: nothing happen if the slack is already equals to target.

Algorithm: Let diff = slack - target (>= 0). We will split the constraint linear expression in 3 parts:

P1: the true variables (only the one assigned < trail_index).
P2: the other variables with a coeff > diff.
Note
all these variables were the propagated ones.
P3: the other variables with a coeff <= diff. We can then transform P1 + P2 + P3 <= rhs_ into P1 + P2' <= rhs_ - diff Where P2' is the same sum as P2 with all the coefficient reduced by diff.

Proof: Given the old constraint, we want to show that the relaxed one is always true. If all the variable in P2' are false, then P1 <= rhs_ - slack <= rhs_ - diff is always true. If at least one of the P2' variable is true, then P2 >= P2' + diff and we have P1 + P2' + diff <= P1 + P2 <= rhs_.

Positive slack.

This is not stricly needed, but true in our use case: The variable assigned at trail_index was causing a conflict.

Nothing to do if the slack is already target.

Applies the algorithm described in the .h

Definition at line 347 of file pb_constraint.cc.

◆ Rhs()

Coefficient operations_research::sat::MutableUpperBoundedLinearConstraint::Rhs ( ) const

inline

Definition at line 281 of file pb_constraint.h.

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

ortools/sat/pb_constraint.h
ortools/sat/pb_constraint.cc

Public Member Functions

Detailed Description

Member Function Documentation

◆ AddTerm()

◆ AddToRhs()

◆ CancelationAmount()

◆ ClearAll()

◆ ClearAndResize()

◆ ComputeSlackForTrailPrefix()

◆ CopyIntoVector()

◆ DebugString()

◆ GetCoefficient()

◆ GetLiteral()

◆ MaxSum()

◆ PossibleNonZeros()

◆ ReduceCoefficients()

◆ ReduceCoefficientsAndComputeSlackForTrailPrefix()

◆ ReduceGivenCoefficient()

◆ ReduceSlackTo()

◆ Rhs()