C++ Reference: class MutableUpperBoundedLinearConstraint
Note: 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: Arguments: 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: Arguments: Adds a non-negative value to this constraint Rhs(). |
CancelationAmount | Return type: Arguments: Returns the "cancelation" amount of AddTerm(literal, coeff). |
ClearAll | Return type: Reset the constraint to 0 <= 0. Note that the constraint size stays the same. |
ClearAndResize | Return type: Arguments: This must be called before any other functions is used with an higher variable index. |
ComputeSlackForTrailPrefix | Return type: Arguments: Compute the constraint slack assuming that only the variables with index < trail_index are assigned. |
CopyIntoVector | Return type: Arguments: Copies this constraint into a vector |
DebugString | Return type: Returns a string representation of the constraint. |
GetCoefficient | Return type: Arguments: Returns the coefficient (>= 0) of the given variable. |
GetLiteral | Return type: Arguments: 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: |
PossibleNonZeros | Return type: 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: 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: Arguments: 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: Arguments: Same as ReduceCoefficients() but only consider the coefficient of the given variable. |
ReduceSlackTo | Return type: Arguments: 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: |