C++ Reference: class PrecedencesPropagator

This documentation is automatically generated.

This class implement a propagator on simple inequalities between integer variables of the form (i1 + offset <= i2). The offset can be constant or given by the value of a third integer variable. Offsets can also be negative.

The algorithm work by mapping the problem onto a graph where the edges carry the offset and the nodes correspond to one of the two bounds of an integer variable (lower_bound or -upper_bound). It then find the fixed point using an incremental variant of the Bellman-Ford(-Tarjan) algorithm.

This is also known as an "integer difference logic theory" in the SMT world. Another word is "separation logic".

TODO(user): We could easily generalize the code to support any relation of the form a*X + b*Y + c*Z >= rhs (or <=). Do that since this class should be a lot faster at propagating small linear inequality than the generic propagator and the overhead of supporting coefficient should not be too bad.
Method
AddConditionalPrecedence

Return type: void

Arguments: IntegerVariable i1, IntegerVariable i2, Literal l

Same as above, but the relation is only true when the given literal is.

AddConditionalPrecedenceWithOffset

Return type: void

Arguments: IntegerVariable i1, IntegerVariable i2, IntegerValue offset, Literal l

AddGreaterThanAtLeastOneOfConstraints

Return type: int

Arguments: Model* model

Advanced usage. To be called once all the constraints have been added to the model. This will loop over all "node" in this class, and if one of its optional incoming arcs must be chosen, it will add a corresponding GreaterThanAtLeastOneOfConstraint(). Returns the number of added constraint. TODO(user): This can be quite slow, add some kind of deterministic limit so that we can use it all the time.

AddPrecedence

Return type: void

Arguments: IntegerVariable i1, IntegerVariable i2

Add a precedence relation (i1 + offset <= i2) between integer variables. Important: The optionality of the variable should be marked BEFORE this is called.

AddPrecedenceReason

Return type: void

Arguments: int arc_index, IntegerValue min_offset, std::vector<Literal>* literal_reason, std::vector<IntegerLiteral>* integer_reason

AddPrecedenceWithAllOptions

Return type: void

Arguments: IntegerVariable i1, IntegerVariable i2, IntegerValue offset, IntegerVariable offset_var, absl::Span<const Literal> presence_literals

Generic function that cover all of the above case and more.

AddPrecedenceWithOffset

Return type: void

Arguments: IntegerVariable i1, IntegerVariable i2, IntegerValue offset

AddPrecedenceWithVariableOffset

Return type: void

Arguments: IntegerVariable i1, IntegerVariable i2, IntegerVariable offset_var

ComputePrecedences

Return type: void

Arguments: const std::vector<IntegerVariable>& vars, std::vector<IntegerPrecedences>* output

PrecedencesPropagator

Return type: explicit

Arguments: Model* model

Propagate

Return type: bool

Propagate

Return type: bool

Arguments: Trail* trail

PropagateOutgoingArcs

Return type: bool

Arguments: IntegerVariable var

Propagates all the outgoing arcs of the given variable (and only those). It is more efficient to do all these propagation in one go by calling Propagate(), but for scheduling problem, we wants to propagate right away the end of an interval when its start moved.

Untrail

Return type: void

Arguments: const Trail& trail, int trail_index