Public Member Functions
	PropagationGraph (double deterministic_time_limit, SatSolver *solver)

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

PropagationGraph &	operator= (const PropagationGraph &)=delete

const std::vector< int32_t > &	operator[] (int32_t index) const

Detailed Description

A simple graph where the nodes are the literals and the nodes adjacent to a literal l are the propagated literal when l is assigned in the underlying sat solver.

This can be used to do a strong component analysis while probing all the literals of a solver. Note that this can be expensive, hence the support for a deterministic time limit.

Definition at line 1097 of file simplification.cc.

Constructor & Destructor Documentation

◆ PropagationGraph() [1/2]

operations_research::sat::PropagationGraph::PropagationGraph	(	double	deterministic_time_limit,
		SatSolver *	solver )

inline

Definition at line 1099 of file simplification.cc.

◆ PropagationGraph() [2/2]

operations_research::sat::PropagationGraph::PropagationGraph ( const PropagationGraph & )

delete

This type is neither copyable nor movable.

Member Function Documentation

◆ operator=()

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

delete

◆ operator[]()

const std::vector< int32_t > & operations_research::sat::PropagationGraph::operator[] ( int32_t index ) const

inline

Returns the set of node adjacent to the given one. Interface needed by FindStronglyConnectedComponents(), note that it needs to be const.

Note: when the time limit is reached, we just keep returning empty adjacency list. This way, the SCC algorithm will terminate quickly and the equivalent literals detection will be incomplete but correct. Note also that thanks to the SCC algorithm, we will explore the connected components first.; the +1 is to avoid adding a => a.

Definition at line 1111 of file simplification.cc.

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

ortools/sat/simplification.cc