operations_research::sat::CircuitPropagator Class Reference

#include <circuit.h>

Inheritance diagram for operations_research::sat::CircuitPropagator:

Classes
struct	Options

Public Member Functions
	CircuitPropagator (int num_nodes, const std::vector< int > &tails, const std::vector< int > &heads, const std::vector< Literal > &literals, Options options, Model *model)
	CircuitPropagator (const CircuitPropagator &)=delete
	This type is neither copyable nor movable.
CircuitPropagator &	operator= (const CircuitPropagator &)=delete
void	SetLevel (int level) final
bool	Propagate () final
bool	IncrementalPropagate (const std::vector< int > &watch_indices) final
void	RegisterWith (GenericLiteralWatcher *watcher)

Detailed Description

Circuit/sub-circuit constraint.

Nodes that are not in the unique allowed sub-circuit must point to themseves. A nodes that has no self-arc must thus be inside the sub-circuit. If there is no self-arc at all, then this constraint forces the circuit to go through all the nodes. Multi-arcs are NOT supported.

Important: for correctness, this constraint requires that "exactly one" constraints have been added for all the incoming (resp. outgoing) arcs of each node. Also, such constraint must propagate before this one.

Definition at line 46 of file circuit.h.

Constructor & Destructor Documentation

CircuitPropagator() [1/2]

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

The constraints take a sparse representation of a graph on [0, n). Each arc being present when the given literal is true.

Temporary data to fill watch_index_to_arcs_.

Tricky: For self-arc, we watch instead when the arc become false.

For the multiple_subcircuit_through_zero case, must_be_in_cycle_ will be const and only contains zero.

Definition at line 35 of file circuit.cc.

CircuitPropagator() [2/2]

operations_research::sat::CircuitPropagator::CircuitPropagator ( const CircuitPropagator & )

delete

This type is neither copyable nor movable.

Member Function Documentation

IncrementalPropagate()

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

Special case for self-arc.

Get rid of the trivial conflicts: At most one incoming and one outgoing arc for each nodes.

Add the arc.

Reimplemented from operations_research::sat::PropagatorInterface.

Definition at line 170 of file circuit.cc.

operator=()

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

delete

Propagate()

bool operations_research::sat::CircuitPropagator::Propagate ( )

finalvirtual

This function assumes that next_, prev_, next_literal_ and must_be_in_cycle_ are all up to date.

Todo

(user): both this and the loop on must_be_in_cycle_ might take some time on large graph. Optimize if this become an issue.

Find the start and end of the path containing node n. If this is a circuit, we will have start_node == end_node.

Todo

(user): we can fail early in more case, like no more possible path to any of the mandatory node.

Any cycle must contain zero.

An incomplete path cannot be closed except if one of the end-points is zero.

None of the other propagation below are valid in case of multiple circuits.

Check if we miss any node that must be in the circuit. Note that the ones for which self_arcs_[i] is kFalseLiteralIndex are first. This is good as it will produce shorter reason. Otherwise we prefer the first that was assigned in the trail.

A circuit that miss a mandatory node is a conflict.

We have an unclosed path. Propagate the fact that it cannot be closed into a cycle, i.e. not(end_node -> start_node).

If we have a cycle, we can propagate all the other nodes to point to themselves. Otherwise there is nothing else to do.

This shouldn't happen because ExactlyOnePerRowAndPerColumn() should have executed first and propagated self_arcs_[node] to false.

We should have detected that above (miss_some_nodes == true). But we still need this for corner cases where the same literal is used for many arcs, and we just propagated it here.

Propagate.

Implements operations_research::sat::PropagatorInterface.

Definition at line 214 of file circuit.cc.

RegisterWith()

void operations_research::sat::CircuitPropagator::RegisterWith

(

GenericLiteralWatcher *

watcher

)

This is needed in case a Literal is used for more than one arc, we may propagate it to false/true here, and it might trigger more propagation.

Todo

(user): come up with a test that fail when this is not here.

Definition at line 110 of file circuit.cc.

SetLevel()

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

---

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

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