operations_research::sat::LinearPropagator Class Reference

#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.
Public Member Functions inherited from operations_research::sat::PropagatorInterface
	PropagatorInterface ()=default
virtual	~PropagatorInterface ()=default
virtual bool	IncrementalPropagate (const std::vector< int > &)

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 300 of file linear_propagation.h.

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 358 of file linear_propagation.cc.

~LinearPropagator()

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

override

Definition at line 382 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. Initialy 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 576 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 888 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_.

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 472 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 406 of file linear_propagation.cc.

---

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

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