operations_research::sat::NoCyclePropagator Class Reference

Enforce the fact that there is no cycle in the given directed graph. More...

#include <circuit.h>

Inheritance diagram for operations_research::sat::NoCyclePropagator:

Public Member Functions
	NoCyclePropagator (int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, Model *model)
void	SetLevel (int level) final
bool	Propagate () final
bool	IncrementalPropagate (const std::vector< int > &watch_indices) final

Detailed Description

Enforce the fact that there is no cycle in the given directed graph.

Definition at line 122 of file circuit.h.

Constructor & Destructor Documentation

NoCyclePropagator()

operations_research::sat::NoCyclePropagator::NoCyclePropagator	(	int	num_nodes,
		const std::vector< int > &	tails,
		const std::vector< int > &	heads,
		const std::vector< Literal > &	literals,
		Model *	model )

Fixed arc. It will never be removed.

We have to deal with the same literal controlling more than one arc.

We register at construction.

Todo

(user): Uniformize this across propagator. Sometimes it is nice not to register them, but most of them can be registered right away.

Definition at line 359 of file circuit.cc.

Member Function Documentation

IncrementalPropagate()

bool operations_research::sat::NoCyclePropagator::IncrementalPropagate ( const std::vector< int > & )

finalvirtual

This will only be called on a non-empty vector, otherwise Propagate() will be called. The passed vector will contain the "watch index" of all the literals that were given one at registration and that changed since the last call to Propagate(). This is only true when going down in the search tree, on backjump this list will be cleared.

Notes:

• The indices may contain duplicates if the same integer variable as been updated many times or if different watched literals have the same watch_index.
• At level zero, it will not contain any indices associated with literals that were already fixed when the propagator was registered. Only the indices of the literals modified after the registration will be present.

Reimplemented from operations_research::sat::PropagatorInterface.

Definition at line 433 of file circuit.cc.

Propagate()

bool operations_research::sat::NoCyclePropagator::Propagate ( )

finalvirtual

Todo

(user): only explore node with newly added arcs.

Todo

(user): We could easily re-index the graph so that only nodes with arcs are used. Because right now we are in O(num_nodes) even if the graph is empty.

The graph should be up to date when this is called thanks to IncrementalPropagate(). We just do a SCC on the graph.

We collect all arc from this compo.

Todo

(user): We could be more efficient here, but this is only executed on conflicts. We should at least make sure we return a single cycle even though if this is called often enough, we shouldn't have a lot more than this.

Implements operations_research::sat::PropagatorInterface.

Definition at line 451 of file circuit.cc.

SetLevel()

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

Backtrack.

Implements operations_research::ReversibleInterface.

Definition at line 415 of file circuit.cc.

---

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

• ortools/sat/circuit.h
• ortools/sat/circuit.cc