operations_research::sat::LinearPropagator Class Reference

Detailed Description

This is meant to supersede both IntegerSumLE and the PrecedencePropagator.

Todo

(user): This is a work in progress and is currently incomplete:

• Lack more incremental support for faster propag.
• Lack detection and propagation of at least one of these linear is true which can be used to propagate more bound if a variable appear in all these constraint.

Definition at line 332 of file linear_propagation.h.

#include <linear_propagation.h>

Inheritance diagram for operations_research::sat::LinearPropagator:

Public Member Functions
	LinearPropagator (Model *model)
	~LinearPropagator () override
bool	Propagate () final
void	SetLevel (int level) final
bool	AddConstraint (absl::Span< const Literal > enforcement_literals, absl::Span< const IntegerVariable > vars, absl::Span< const IntegerValue > coeffs, IntegerValue upper_bound)
	Adds a new constraint to the propagator.
void	Explain (int id, IntegerValue propagation_slack, IntegerVariable var_to_explain, int trail_index, std::vector< Literal > *literals_reason, std::vector< int > *trail_indices_reason) final
	For LazyReasonInterface.
void	SetPushAffineUbForBinaryRelation ()
Public Member Functions inherited from operations_research::sat::PropagatorInterface
	PropagatorInterface ()=default
virtual	~PropagatorInterface ()=default
virtual bool	IncrementalPropagate (const std::vector< int > &)

Constructor & Destructor Documentation

LinearPropagator()

operations_research::sat::LinearPropagator::LinearPropagator ( Model * model )

explicit

Note

we need this class always in sync.

Todo

(user): When we start to push too much (Cycle?) we should see what other propagator says before repropagating this one, system for call later?

Definition at line 378 of file linear_propagation.cc.

~LinearPropagator()

operations_research::sat::LinearPropagator::~LinearPropagator ( )

override

Definition at line 404 of file linear_propagation.cc.

Member Function Documentation

AddConstraint()

bool operations_research::sat::LinearPropagator::AddConstraint	(	absl::Span< const Literal >	enforcement_literals,
		absl::Span< const IntegerVariable >	vars,
		absl::Span< const IntegerValue >	coeffs,
		IntegerValue	upper_bound )

Adds a new constraint to the propagator.

Adds a new constraint to the propagator. We support adding constraint at a positive level:

• This will push new propagation right away.
• This will returns false if the constraint is currently a conflict.

Make sure max_variations_ is of correct size.

Note

we also have a hard limit of 1 << 29 on the size.

Initialize constraint data.

Todo

(user): we still waste the space in coeffs_buffer_ so that the start are aligned with the variables_buffer_.

Initialize watchers. Initially we want everything to be propagated at least once.

Todo

(user): With some care, when we cannot propagate or the constraint is not enforced, we could leave in_queue_[] at true but not put the constraint in the queue.

When a conditional precedence becomes enforced, add it.

Note

we only look at relation that were a "precedence" from the start, note the one currently of size 2 if we ignore fixed variables.

Todo

(user): Shall we register root level precedence from here rather than separately?

Transposed graph to know which constraint to wake up.

We need both the var entry and its negation to be allocated.

Todo

(user): Shall we decide on some ordering here? maybe big coeff first so that we get the largest change in slack? the idea being to propagate large change first in case of cycles.

We need to be registered to the watcher so Propagate() is called at the proper priority. But then we rely on modified_vars_.

Propagate this new constraint.

Todo

(user): Do we want to do that?

Definition at line 653 of file linear_propagation.cc.

Explain()

void operations_research::sat::LinearPropagator::Explain ( int id, IntegerValue propagation_slack, IntegerVariable var_to_explain, int trail_index, std::vector< Literal > * literals_reason, std::vector< int > * trail_indices_reason )

finalvirtual

For LazyReasonInterface.

Implements operations_research::sat::LazyReasonInterface.

Definition at line 967 of file linear_propagation.cc.

Propagate()

bool operations_research::sat::LinearPropagator::Propagate ( )

finalvirtual

This will be called after one or more literals that are watched by this propagator changed. It will also always be called on the first propagation cycle after registration.

Initial addition.

We will clear modified_vars_ on exit since everything we propagate here is handled by PropagateOneConstraint().

Cleanup.

We abort this propagator as soon as a Boolean is propagated, so that we always finish the Boolean propagation first. This can happen when we push a bound that has associated Booleans or push enforcement to false. The idea is to resume from our current state when we are called again. Note however that we have to clear the propagated_by_ info has other propagator might have pushed the same variable further.

Todo

(user): More than the propagation speed, I think it is important to have proper explanation, so if A pushes B, but later on the queue we have C that push A that push B again, that might be bad? We can try to avoid this even further, by organizing the queue in passes:

• Scan all relevant constraints, remember who pushes but DO NOT push yet!
• If no cycle, do not pushes constraint whose slack will changes due to other pushes.
• consider the new constraint that need to be scanned and repeat. I think it is okay to scan twice the constraints that push something in order to get better explanation. We tend to diverge from the class shortest path algo in this regard.

Todo

(user): If we push the idea further, can we first compute the fix point without pushing anything, then compute a good order of constraints for the explanations? what is tricky is that we might need to "scan" more than once a constraint I think. ex: Y, Z, T >=0

• 2 * Y + Z + T <= 11 ==> Y <= 5, Z <= 11, T <= 11 (1)
• Z + Y >= 6 ==> Z >= 1
• (1) again to push T <= 10 and reach the propagation fixed point.

We always process the whole queue in FIFO order.

Note

the order really only matter for infeasible constraint so it shouldn't have a big impact.

This is either a conflict or an enforcement propagation. We do it right away.

We abort after the first pushed boolean. We could abort later too, it is unclear what works best.

Todo

(user): Maybe we should "update" explanation if we have a shorter one to be less reliant on the propagation order.

Note

the last constraint added in to_propagate_ should never be "skipped" and have any variable marked as var_will_change_.

Look at linear3 and update our "linear2 affine upper bound". If we are here it means the constraint was in the queue, and its slack changed, so it might lead to stronger affine ub.

Todo

(user): This can be costly for no reason if we keep updating the bound for variable appearing in a single linear3. On another hand it is O(1) compared to what this class already do. Profile will tell if it is worth it. Maybe we can only share LinearExpression2 that we might look up.

Todo

(user): This only look at non-enforced linear3. We could look at constraint whose enforcement or other variables are fixed at level zero, but it is trickier. It could be done if we add a "batch clean up" to this class that runs at level zero, and reduce constraints accordingly.

A constraint A + B + C <= rhs can lead to up to 3 relations...

We don't "push" relation A + B <= ub if A or B is fixed, because the variable bound of the non-fixed A or B should just be as-strong as what can be inferred from the binary relation.

The fixed variable is always at index 2. The rev_rhs was updated to: initial_rhs - lb(vars[2]) * coeffs[2].

We can probably save the AnalyzeConstraint() cost, but then we only do that when the constraint propagate, and the context might have change since we computed it above.

Todo

(user): This do not seems always good, especially since we pushed Boolean with a really small explanation, maybe we want to push more of these rather than go back to pure-binary propagation.

Implements operations_research::sat::PropagatorInterface.

Definition at line 496 of file linear_propagation.cc.

SetLevel()

void operations_research::sat::LinearPropagator::SetLevel ( int level )

finalvirtual

Initially a reversible class starts at level zero. Increasing the level saves the state of the current old level. Decreasing the level restores the state to what it was at this level and all higher levels are forgotten. Everything done at level zero cannot be backtracked over.

The level is assumed to be non-negative.

If the solver backtracked at any point, we invalidate all our queue and propagated_by information.

Tricky: if we aborted the current propagation because we pushed a Boolean, by default, the GenericLiteralWatcher will only call Propagate() again if one of the watched variable changed. With this, it is guaranteed to call it again if it wasn't in the queue already.

Implements operations_research::ReversibleInterface.

Definition at line 428 of file linear_propagation.cc.

SetPushAffineUbForBinaryRelation()

void operations_research::sat::LinearPropagator::SetPushAffineUbForBinaryRelation ( )

inline

Definition at line 356 of file linear_propagation.h.

---

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

• ortools/sat/linear_propagation.h
• ortools/sat/linear_propagation.cc