Stay organized with collections Save and categorize content based on your preferences.

C++ Reference: class IntegerSumLE

Note: This documentation is automatically generated.

A really basic implementation of an upper-bounded sum of integer variables. The complexity is in O(num_variables) at each propagation.

Note that we assume that there can be NO integer overflow. This must be checked at model validation time before this is even created.

TODO(user): If one has many such constraint, it will be more efficient to propagate all of them at once rather than doing it one at the time.

TODO(user): Explore tree structure to get a log(n) complexity.

TODO(user): When the variables are Boolean, use directly the pseudo-Boolean constraint implementation. But we do need support for enforcement literals there.

Return type: std::pair<IntegerValue, IntegerValue>

Arguments: IntegerLiteral integer_literal, IntegerVariable target_var

This is a pretty usage specific function. Returns the implied lower bound on target_var if the given integer literal is false (resp. true). If the variables do not appear both in the linear inequality, this returns two kMinIntegerValue.


Arguments: const std::vector<Literal>& enforcement_literals, const std::vector<IntegerVariable>& vars, const std::vector<IntegerValue>& coeffs, IntegerValue upper_bound, Model* model

If refied_literal is kNoLiteralIndex then this is a normal constraint, otherwise we enforce the implication refied_literal => constraint is true. Note that we don't do the reverse implication here, it is usually done by another IntegerSumLE constraint on the negated variables.


Return type: bool

We propagate: - If the sum of the individual lower-bound is > upper_bound, we fail. - For all i, upper-bound of i <= upper_bound - Sum {individual lower-bound excluding i).


Return type: bool

Same as Propagate() but only consider current root level bounds. This is mainly useful for the LP propagator since it can find relevant optimal really late in the search tree.


Return type: void

Arguments: GenericLiteralWatcher* watcher