C++ Reference: class MutableUpperBoundedLinearConstraint

This documentation is automatically generated.

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.
Method
AddTerm

Return type: void

Arguments: Literal literal, Coefficient coeff

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

AddToRhs

Return type: void

Arguments: Coefficient value

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

CancelationAmount

Return type: Coefficient

Arguments: Literal literal, Coefficient coeff

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

ClearAll

Return type: void

Reset the constraint to 0 <= 0. Note that the contraint size stays the same.

ClearAndResize

Return type: void

Arguments: int num_variables

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

ComputeSlackForTrailPrefix

Return type: Coefficient

Arguments: const Trail& trail, int trail_index

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

CopyIntoVector

Return type: void

Arguments: std::vector<LiteralWithCoeff>* output

Copies this constraint into a std::vector representation.

DebugString

Return type: std::string

Returns a std::string representation of the constraint.

GetCoefficient

Return type: Coefficient

Arguments: BooleanVariable var

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

GetLiteral

Return type: Literal

Arguments: BooleanVariable var

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

MaxSum

Return type: Coefficient

PossibleNonZeros

Return type: const std::vector<BooleanVariable>&

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.

ReduceCoefficients

Return type: void

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.

ReduceCoefficientsAndComputeSlackForTrailPrefix

Return type: Coefficient

Arguments: 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 that 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.

ReduceGivenCoefficient

Return type: void

Arguments: BooleanVariable var

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

ReduceSlackTo

Return type: void

Arguments: 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 that 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 that 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_.

Rhs

Return type: Coefficient