operations_research::sat::PrecedencesPropagator Class Reference

#include <precedences.h>

Inheritance diagram for operations_research::sat::PrecedencesPropagator:

Public Member Functions
	PrecedencesPropagator (Model *model)
	PrecedencesPropagator (const PrecedencesPropagator &)=delete
	This type is neither copyable nor movable.
PrecedencesPropagator &	operator= (const PrecedencesPropagator &)=delete
	~PrecedencesPropagator () override
bool	Propagate () final
bool	Propagate (Trail *trail) final
void	Untrail (const Trail &trail, int trail_index) final
bool	PropagateOutgoingArcs (IntegerVariable var)
void	AddPrecedence (IntegerVariable i1, IntegerVariable i2)
void	AddPrecedenceWithOffset (IntegerVariable i1, IntegerVariable i2, IntegerValue offset)
void	AddPrecedenceWithVariableOffset (IntegerVariable i1, IntegerVariable i2, IntegerVariable offset_var)
void	AddConditionalPrecedence (IntegerVariable i1, IntegerVariable i2, Literal l)
	Same as above, but the relation is only true when the given literal is.
void	AddConditionalPrecedenceWithOffset (IntegerVariable i1, IntegerVariable i2, IntegerValue offset, Literal l)
void	AddPrecedenceWithAllOptions (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.
bool	AddPrecedenceWithOffsetIfNew (IntegerVariable i1, IntegerVariable i2, IntegerValue offset)
	This version check current precedence. It is however "slow".
Public Member Functions inherited from operations_research::sat::SatPropagator
	SatPropagator (const std::string &name)
	SatPropagator (const SatPropagator &)=delete
	This type is neither copyable nor movable.
SatPropagator &	operator= (const SatPropagator &)=delete
virtual	~SatPropagator ()=default
void	SetPropagatorId (int id)
	Sets/Gets this propagator unique id.
int	PropagatorId () const
virtual absl::Span< const Literal >	Reason (const Trail &, int, int64_t) const
bool	PropagatePreconditionsAreSatisfied (const Trail &trail) const
	######################## Implementations below ########################
bool	PropagationIsDone (const Trail &trail) const
	Returns true iff all the trail was inspected by this propagator.
virtual bool	IsEmpty () const

Additional Inherited Members
Protected Attributes inherited from operations_research::sat::SatPropagator
const std::string	name_
int	propagator_id_
int	propagation_trail_index_

Detailed Description

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 works 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.

Definition at line 267 of file precedences.h.

Constructor & Destructor Documentation

PrecedencesPropagator() [1/2]

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

inlineexplicit

Definition at line 269 of file precedences.h.

PrecedencesPropagator() [2/2]

operations_research::sat::PrecedencesPropagator::PrecedencesPropagator ( const PrecedencesPropagator & )

delete

This type is neither copyable nor movable.

~PrecedencesPropagator()

operations_research::sat::PrecedencesPropagator::~PrecedencesPropagator ( )

override

Definition at line 498 of file precedences.cc.

Member Function Documentation

AddConditionalPrecedence()

void operations_research::sat::PrecedencesPropagator::AddConditionalPrecedence ( IntegerVariable i1, IntegerVariable i2, Literal l )

inline

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

Definition at line 589 of file precedences.h.

AddConditionalPrecedenceWithOffset()

void operations_research::sat::PrecedencesPropagator::AddConditionalPrecedenceWithOffset ( IntegerVariable i1, IntegerVariable i2, IntegerValue offset, Literal l )

inline

Definition at line 596 of file precedences.h.

AddPrecedence()

void operations_research::sat::PrecedencesPropagator::AddPrecedence ( IntegerVariable i1, IntegerVariable i2 )

inline

Add a precedence relation (i1 + offset <= i2) between integer variables.

Important: The optionality of the variable should be marked BEFORE this is called.

Implementation of the small API functions below.

Definition at line 578 of file precedences.h.

AddPrecedenceWithAllOptions()

void operations_research::sat::PrecedencesPropagator::AddPrecedenceWithAllOptions ( IntegerVariable i1, IntegerVariable i2, IntegerValue offset, IntegerVariable offset_var, absl::Span< const Literal > presence_literals )

inline

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

Definition at line 606 of file precedences.h.

AddPrecedenceWithOffset()

void operations_research::sat::PrecedencesPropagator::AddPrecedenceWithOffset ( IntegerVariable i1, IntegerVariable i2, IntegerValue offset )

inline

Definition at line 584 of file precedences.h.

AddPrecedenceWithOffsetIfNew()

bool operations_research::sat::PrecedencesPropagator::AddPrecedenceWithOffsetIfNew	(	IntegerVariable	i1,
		IntegerVariable	i2,
		IntegerValue	offset )

This version check current precedence. It is however "slow".

Todo

(user): Modify arc in place!

Definition at line 755 of file precedences.cc.

AddPrecedenceWithVariableOffset()

void operations_research::sat::PrecedencesPropagator::AddPrecedenceWithVariableOffset ( IntegerVariable i1, IntegerVariable i2, IntegerVariable offset_var )

inline

Definition at line 601 of file precedences.h.

operator=()

PrecedencesPropagator & operations_research::sat::PrecedencesPropagator::operator= ( const PrecedencesPropagator & )

delete

Propagate() [1/2]

bool operations_research::sat::PrecedencesPropagator::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.

IMPORTANT: Because of the way Untrail() work, we need to add all the potential arcs before we can abort. It is why we iterate twice here.

Iterate again to check for a propagation and indirectly update modified_vars_.

Do the actual propagation of the IntegerVariable bounds.

We can only test that no propagation is left if we didn't enqueue new literal in the presence of optional variables.

Todo

(user): Because of our code to deal with InPropagationLoop(), this is not always true. Find a cleaner way to DCHECK() while not failing in this corner case.

Propagate the presence literals of the arcs that can't be added.

Clean-up modified_vars_ to do as little as possible on the next call.

Implements operations_research::sat::PropagatorInterface.

Definition at line 511 of file precedences.cc.

Propagate() [2/2]

bool operations_research::sat::PrecedencesPropagator::Propagate ( Trail * trail )

finalvirtual

Inspects the trail from propagation_trail_index_ until at least one literal is propagated. Returns false iff a conflict is detected (in which case trail->SetFailingClause() must be called).

This must update propagation_trail_index_ so that all the literals before it have been propagated. In particular, if nothing was propagated, then PropagationIsDone() must return true.

Implements operations_research::sat::SatPropagator.

Definition at line 509 of file precedences.cc.

PropagateOutgoingArcs()

bool operations_research::sat::PrecedencesPropagator::PropagateOutgoingArcs

(

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.

Definition at line 564 of file precedences.cc.

Untrail()

void operations_research::sat::PrecedencesPropagator::Untrail ( const Trail & , int trail_index )

finalvirtual

Reverts the state so that all the literals with a trail index greater or equal to the given one are not processed for propagation. Note that the trail current decision level is already reverted before this is called.

Todo

(user): Currently this is called at each Backtrack(), but we could bundle the calls in case multiple conflict one after the other are detected even before the Propagate() call of a SatPropagator is called.

Todo

(user): It is not yet 100% the case, but this can be guaranteed to be called with a trail index that will always be the start of a new decision level.

This means that we already propagated all there is to propagate at the level trail_index, so we can safely clear modified_vars_ in case it wasn't already done.

Reimplemented from operations_research::sat::SatPropagator.

Definition at line 589 of file precedences.cc.

---

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

• ortools/sat/precedences.h
• ortools/sat/precedences.cc