operations_research::sat::CircuitCoveringPropagator Class Reference

#include <circuit.h>

Inheritance diagram for operations_research::sat::CircuitCoveringPropagator:

Public Member Functions
	CircuitCoveringPropagator (std::vector< std::vector< Literal > > graph, const std::vector< int > &distinguished_nodes, Model *model)
void	SetLevel (int level) final
bool	Propagate () final
bool	IncrementalPropagate (const std::vector< int > &watch_indices) final
void	RegisterWith (GenericLiteralWatcher *watcher)

Detailed Description

This constraint ensures that the graph is a covering of all nodes by circuits and loops, such that all circuits contain exactly one distinguished node. Those distinguished nodes are meant to be depots.

This constraint does not need ExactlyOnePerRowAndPerColumn() to be correct, but it does not propagate degree deductions (only fails if a node has more than one outgoing arc or more than one incoming arc), so that adding ExactlyOnePerRowAndPerColumn() should work better.

Todo

(user): Make distinguished nodes an array of Boolean variables, so this can be used for facility location problems.

Definition at line 173 of file circuit.h.

Constructor & Destructor Documentation

CircuitCoveringPropagator()

operations_research::sat::CircuitCoveringPropagator::CircuitCoveringPropagator	(	std::vector< std::vector< Literal > >	graph,
		const std::vector< int > &	distinguished_nodes,
		Model *	model )

Definition at line 484 of file circuit.cc.

Member Function Documentation

IncrementalPropagate()

bool operations_research::sat::CircuitCoveringPropagator::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 529 of file circuit.cc.

Propagate()

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

Gather next_ and prev_ from fixed arcs.

Two arcs go out of arc.first, forbidden.

Two arcs come into arc.second, forbidden.

For every node, find partial path/circuit in which the node is. Use visited_ to visit each path/circuit only once.

Skip if already visited, isolated or loop.

Find start of path/circuit.

Find distinguished node of path. Fail if there are several, fail if this is a non loop circuit and there are none.

Circuit with no distinguished nodes, forbidden.

Path with no distinguished node: forbid to close it.

Implements operations_research::sat::PropagatorInterface.

Definition at line 550 of file circuit.cc.

RegisterWith()

void operations_research::sat::CircuitCoveringPropagator::RegisterWith

(

GenericLiteralWatcher *

watcher

)

Fill fixed_arcs_ with arcs that are initially fixed to true, assign arcs to watch indices.

Definition at line 496 of file circuit.cc.

SetLevel()

void operations_research::sat::CircuitCoveringPropagator::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 516 of file circuit.cc.

---

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

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