#include <integer.h>

Inheritance diagram for operations_research::sat::GenericLiteralWatcher:

Public Member Functions
	GenericLiteralWatcher (Model *model)

	GenericLiteralWatcher (const GenericLiteralWatcher &)=delete
	This type is neither copyable nor movable.

GenericLiteralWatcher &	operator= (const GenericLiteralWatcher &)=delete

	~GenericLiteralWatcher () final=default

void	ReserveSpaceForNumVariables (int num_vars)
	Memory optimization: you can call this before registering watchers.

bool	Propagate (Trail *trail) final

void	Untrail (const Trail &trail, int literal_trail_index) final

int	Register (PropagatorInterface *propagator)
	Registers a propagator and returns its unique ids.

void	SetPropagatorPriority (int id, int priority)

void	NotifyThatPropagatorMayNotReachFixedPointInOnePass (int id)

void	AlwaysCallAtLevelZero (int id)

void	WatchLiteral (Literal l, int id, int watch_index=-1)

void	WatchLowerBound (IntegerVariable var, int id, int watch_index=-1)

void	WatchUpperBound (IntegerVariable var, int id, int watch_index=-1)

void	WatchIntegerVariable (IntegerVariable i, int id, int watch_index=-1)

void	WatchLowerBound (AffineExpression e, int id)

void	WatchUpperBound (AffineExpression e, int id)

void	WatchAffineExpression (AffineExpression e, int id)

void	WatchLowerBound (IntegerValue, int)

void	WatchUpperBound (IntegerValue, int)

void	WatchIntegerVariable (IntegerValue, int)

void	RegisterReversibleClass (int id, ReversibleInterface *rev)

void	RegisterReversibleInt (int id, int *rev)

void	SetUntilNextBacktrack (bool *is_in_dive)

int	NumPropagators () const
	Returns the number of registered propagators.

void	RegisterLevelZeroModifiedVariablesCallback (const std::function< void(const std::vector< IntegerVariable > &)> cb)

void	SetStopPropagationCallback (std::function< bool()> callback)

int	GetCurrentId () const

void	CallOnNextPropagate (int id)
	Add the given propagator to its queue.

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 allows registering Propagator that will be called if a watched Literal or LbVar changes.

Todo: (user): Move this to its own file. Add unit tests!

Definition at line 1462 of file integer.h.

Constructor & Destructor Documentation

◆ GenericLiteralWatcher() [1/2]

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

explicit

Todo: (user): This propagator currently needs to be last because it is the only one enforcing that a fix-point is reached on the integer variables. Figure out a better interaction between the sat propagation loop and this one.

Definition at line 2087 of file integer.cc.

◆ GenericLiteralWatcher() [2/2]

operations_research::sat::GenericLiteralWatcher::GenericLiteralWatcher ( const GenericLiteralWatcher & )

delete

This type is neither copyable nor movable.

◆ ~GenericLiteralWatcher()

operations_research::sat::GenericLiteralWatcher::~GenericLiteralWatcher ( )

finaldefault

Member Function Documentation

◆ AlwaysCallAtLevelZero()

void operations_research::sat::GenericLiteralWatcher::AlwaysCallAtLevelZero ( int id )

Whether we call a propagator even if its watched variables didn't change. This is only used when we are back to level zero. This was introduced for the LP propagator where we might need to continue an interrupted solve or add extra cuts at level zero.

Definition at line 2370 of file integer.cc.

◆ CallOnNextPropagate()

void operations_research::sat::GenericLiteralWatcher::CallOnNextPropagate ( int id )

Add the given propagator to its queue.

Definition at line 2108 of file integer.cc.

◆ GetCurrentId()

int operations_research::sat::GenericLiteralWatcher::GetCurrentId ( ) const

inline

Returns the id of the propagator we are currently calling. This is meant to be used from inside Propagate() in case a propagator was registered more than once at different priority for instance.

Definition at line 1599 of file integer.h.

◆ NotifyThatPropagatorMayNotReachFixedPointInOnePass()

void operations_research::sat::GenericLiteralWatcher::NotifyThatPropagatorMayNotReachFixedPointInOnePass ( int id )

The default behavior is to assume that a propagator does not need to be called twice in a row. However, propagators on which this is called will be called again if they change one of their own watched variables.

Definition at line 2365 of file integer.cc.

◆ NumPropagators()

int operations_research::sat::GenericLiteralWatcher::NumPropagators ( ) const

inline

Returns the number of registered propagators.

Definition at line 1571 of file integer.h.

◆ operator=()

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

delete

◆ Propagate()

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

finalvirtual

On propagate, the registered propagators will be called if they need to until a fixed point is reached. Propagators with low ids will tend to be called first, but it ultimately depends on their "waking" order.

Only once per call to Propagate(), if we are at level zero, we might want to call propagators even if the bounds didn't change.

Increase the deterministic time depending on some basic fact about our propagation.

Note: the priority may be set to -1 inside the loop in order to restart at zero.

We test the time limit from time to time. This is in order to return in case of slow propagation.

Todo: (user): The queue will not be emptied, but I am not sure the solver will be left in an usable state. Fix if it become needed to resume the solve from the last time it was interrupted. In particular, we might want to call UpdateCallingNeeds()?

Before we propagate, make sure any reversible structure are up to date.

Note: we never do anything expensive more than once per level.

This is needed to detect if the propagator propagated anything or not.

Todo: (user): Maybe just provide one function Propagate(watch_indices) ?

Update the propagation queue. At this point, the propagator has been removed from the queue but in_queue_ is still true.

If the propagator is assumed to be idempotent, then we set in_queue_ to false after UpdateCallingNeeds() so this later function will never add it back.

Otherwise, we set in_queue_ to false first so that UpdateCallingNeeds() may add it back if the propagator modified any of its watched variables.

If the propagator pushed a literal, we exit in order to rerun all SAT only propagators first. Note that since a literal was pushed we are guaranteed to be called again, and we will resume from priority 0.

Important: for now we need to re-run the clauses propagator each time we push a new literal because some propagator like the arc consistent all diff relies on this.

Todo: (user): However, on some problem, it seems to work better to not do that. One possible reason is that the reason of a "natural" propagation might be better than one we learned.

If the propagator pushed an integer bound, we revert to priority = 0.

We wait until we reach the fix point before calling the callback.

Implements operations_research::sat::SatPropagator.

Definition at line 2155 of file integer.cc.

◆ Register()

int operations_research::sat::GenericLiteralWatcher::Register ( PropagatorInterface * propagator )

Registers a propagator and returns its unique ids.

Call this propagator at least once the next time Propagate() is called.

Todo: (user): This initial propagation does not respect any later priority settings. Fix this. Maybe we should force users to pass the priority at registration. For now I didn't want to change the interface because there are plans to implement a kind of "dynamic" priority, and if it works we may want to get rid of this altogether.

Definition at line 2332 of file integer.cc.

◆ RegisterLevelZeroModifiedVariablesCallback()

void operations_research::sat::GenericLiteralWatcher::RegisterLevelZeroModifiedVariablesCallback ( const std::function< void(const std::vector< IntegerVariable > &)> cb )

inline

Set a callback for new variable bounds at level 0.

This will be called (only at level zero) with the list of IntegerVariable with changed lower bounds. Note that it might be called more than once during the same propagation cycle if we fix variables in "stages".

Also note that this will be called if some BooleanVariable where fixed even if no IntegerVariable are changed, so the passed vector to the function might be empty.

Definition at line 1582 of file integer.h.

◆ RegisterReversibleClass()

void operations_research::sat::GenericLiteralWatcher::RegisterReversibleClass	(	int	id,
		ReversibleInterface *	rev )

Registers a reversible class with a given propagator. This class will be changed to the correct state just before the propagator is called.

Doing it just before should minimize cache-misses and bundle as much as possible the "backtracking" together. Many propagators only watches a few variables and will not be called at each decision levels.

Definition at line 2374 of file integer.cc.

◆ RegisterReversibleInt()

void operations_research::sat::GenericLiteralWatcher::RegisterReversibleInt	(	int	id,
		int *	rev )

Registers a reversible int with a given propagator. The int will be changed to its correct value just before Propagate() is called.

Note: this will work in O(num_rev_int_of_propagator_id) per call to Propagate() and happens at most once per decision level. As such this is meant for classes that have just a few reversible ints or that will have a similar complexity anyway.

Alternatively, one can directly get the underlying RevRepository<int> with a call to model.Get<>(), and use SaveWithStamp() before each modification to have just a slight overhead per int updates. This later option is what is usually done in a CP solver at the cost of a slightly more complex API.

Definition at line 2380 of file integer.cc.

◆ ReserveSpaceForNumVariables()

void operations_research::sat::GenericLiteralWatcher::ReserveSpaceForNumVariables ( int num_vars )

Memory optimization: you can call this before registering watchers.

Definition at line 2104 of file integer.cc.

◆ SetPropagatorPriority()

void operations_research::sat::GenericLiteralWatcher::SetPropagatorPriority	(	int	id,
		int	priority )

Changes the priority of the propagator with given id. The priority is a non-negative integer. Propagators with a lower priority will always be run before the ones with a higher one. The default priority is one.

Definition at line 2358 of file integer.cc.

◆ SetStopPropagationCallback()

void operations_research::sat::GenericLiteralWatcher::SetStopPropagationCallback ( std::function< bool()> callback )

inline

This will be called not too often during propagation (when we finish propagating one priority). If it returns true, we will stop propagation there. It is used by LbTreeSearch as we can stop as soon as the objective lower bound crossed a threshold and do not need to call expensive propagator when this is the case.

Definition at line 1592 of file integer.h.

◆ SetUntilNextBacktrack()

void operations_research::sat::GenericLiteralWatcher::SetUntilNextBacktrack ( bool * is_in_dive )

inline

A simple form of incremental update is to maintain state as we dive into the search tree but forget everything on every backtrack. A propagator can be called many times by decision, so this can make a large proportion of the calls incremental.

This allows to achieve this with a really low overhead.

The propagator can define a bool rev_is_in_dive_ = false; and at the beginning of each propagate do: const bool no_backtrack_since_last_call = rev_is_in_dive_; watcher_->SetUntilNextBacktrack(&rev_is_in_dive_);

Definition at line 1563 of file integer.h.

◆ Untrail()

void operations_research::sat::GenericLiteralWatcher::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.

Nothing to do since we found a conflict before Propagate() was called.

The assumption is not always true if we are currently aborting.

Note: we can do that after the test above: If none of the propagator where called, there are still technically "in dive" if we didn't backtrack past their last Propagate() call.

We need to clear the watch indices on untrail.

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 2297 of file integer.cc.

◆ WatchAffineExpression()

void operations_research::sat::GenericLiteralWatcher::WatchAffineExpression	(	AffineExpression	e,
		int	id )

inline

Definition at line 1520 of file integer.h.

◆ WatchIntegerVariable() [1/2]

void operations_research::sat::GenericLiteralWatcher::WatchIntegerVariable	(	IntegerValue	,
		int	)

inline

Definition at line 1528 of file integer.h.

◆ WatchIntegerVariable() [2/2]

void operations_research::sat::GenericLiteralWatcher::WatchIntegerVariable	(	IntegerVariable	i,
		int	id,
		int	watch_index = -1 )

inline

Definition at line 1876 of file integer.h.

◆ WatchLiteral()

void operations_research::sat::GenericLiteralWatcher::WatchLiteral	(	Literal	l,
		int	id,
		int	watch_index = -1 )

inline

Watches the corresponding quantity. The propagator with given id will be called if it changes. Note that WatchLiteral() only trigger when the literal becomes true.

If watch_index is specified, it is associated with the watched literal. Doing this will cause IncrementalPropagate() to be called (see the documentation of this interface for more detail).

Definition at line 1844 of file integer.h.

◆ WatchLowerBound() [1/3]

void operations_research::sat::GenericLiteralWatcher::WatchLowerBound	(	AffineExpression	e,
		int	id )

inline

Because the coeff is always positive, watching an affine expression is the same as watching its var.

Definition at line 1514 of file integer.h.

◆ WatchLowerBound() [2/3]

void operations_research::sat::GenericLiteralWatcher::WatchLowerBound	(	IntegerValue	,
		int	)

inline

No-op overload for "constant" IntegerVariable that are sometimes templated as an IntegerValue.

Definition at line 1526 of file integer.h.

◆ WatchLowerBound() [3/3]

void operations_research::sat::GenericLiteralWatcher::WatchLowerBound	(	IntegerVariable	var,
		int	id,
		int	watch_index = -1 )

inline

Minor optim, so that we don't watch the same variable twice. Propagator code is easier this way since for example when one wants to watch both an interval start and interval end, both might have the same underlying variable.

Definition at line 1852 of file integer.h.

◆ WatchUpperBound() [1/3]

void operations_research::sat::GenericLiteralWatcher::WatchUpperBound	(	AffineExpression	e,
		int	id )

inline

Definition at line 1517 of file integer.h.

◆ WatchUpperBound() [2/3]

void operations_research::sat::GenericLiteralWatcher::WatchUpperBound	(	IntegerValue	,
		int	)

inline

Definition at line 1527 of file integer.h.

◆ WatchUpperBound() [3/3]

void operations_research::sat::GenericLiteralWatcher::WatchUpperBound	(	IntegerVariable	var,
		int	id,
		int	watch_index = -1 )

inline

Definition at line 1870 of file integer.h.

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

ortools/sat/integer.h
ortools/sat/integer.cc

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ GenericLiteralWatcher() [1/2]

◆ GenericLiteralWatcher() [2/2]

◆ ~GenericLiteralWatcher()

Member Function Documentation

◆ AlwaysCallAtLevelZero()

◆ CallOnNextPropagate()

◆ GetCurrentId()

◆ NotifyThatPropagatorMayNotReachFixedPointInOnePass()

◆ NumPropagators()

◆ operator=()

◆ Propagate()

◆ Register()

◆ RegisterLevelZeroModifiedVariablesCallback()

◆ RegisterReversibleClass()

◆ RegisterReversibleInt()

◆ ReserveSpaceForNumVariables()

◆ SetPropagatorPriority()

◆ SetStopPropagationCallback()

◆ SetUntilNextBacktrack()

◆ Untrail()

◆ WatchAffineExpression()

◆ WatchIntegerVariable() [1/2]

◆ WatchIntegerVariable() [2/2]

◆ WatchLiteral()

◆ WatchLowerBound() [1/3]

◆ WatchLowerBound() [2/3]

◆ WatchLowerBound() [3/3]

◆ WatchUpperBound() [1/3]

◆ WatchUpperBound() [2/3]

◆ WatchUpperBound() [3/3]