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 1136 of file simplification.cc.

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

Constructor & Destructor Documentation

◆ PropagationGraph() [1/2]

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

inline

Definition at line 1138 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 1150 of file simplification.cc.

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

ortools/sat/simplification.cc