A simple solver for TwoSAT instances, representing the instance as implication graph and solving it via its strongly-connected components. More...

#include <ogdf/cluster/sync_plan/basic/TwoSAT.h>

Inheritance diagram for ogdf::TwoSAT:

Public Types
using	const_iterator = typename std::vector< bool >::const_iterator

using	const_reverse_iterator = typename std::vector< bool >::const_reverse_iterator

Public Member Functions
	TwoSAT ()

const_iterator	begin () const

int	clauseCount () const

void	clear () override
	Removes all nodes and all edges from the graph. More...

const_iterator	end () const

bool	getAssignment (twosat_var var) const

int	newClause (twosat_var var1, bool sign1, twosat_var var2, bool sign2)

twosat_var	newVariable ()

const_reverse_iterator	rbegin () const

const_reverse_iterator	rend () const

bool	solve ()

int	variableCount () const

Protected Member Functions
node	getNode (twosat_var var, bool sign) const

int	getNodeIndex (twosat_var var, bool sign) const

std::pair< node, node >	getNodes (twosat_var var, bool flip=false) const

Protected Member Functions inherited from ogdf::Graph
virtual void *	preInsert (bool copyEmbedding, bool copyIDs, bool notifyObservers, bool edgeFilter, NodeArray< node > &nodeMap, EdgeArray< edge > &edgeMap, int newNodes, int newEdges)
	Callback notifying subclasses that some graph is about to be insert() -ed. More...

virtual void	nodeInserted (void *userData, node original, node copy)
	Callback notifying subclasses that insert() copied a node. More...

virtual void	edgeInserted (void *userData, edge original, edge copy)
	Callback notifying subclasses that insert() copied an edge. More...

virtual void	postInsert (void *userData, int newNodes, int newEdges)
	Callback notifying subclasses that an insert() call has finished. More...

	Graph ()
	Constructs an empty graph. More...

	Graph (const Graph &copy)
	Constructs a graph that is a copy of `G`. More...

	Graph (Graph &&move)=delete

virtual	~Graph ()
	Destructor. More...

Graph &	operator= (const Graph &copy)
	Overwrites this graph to be a copy of `G`. More...

Graph &	operator= (Graph &&move)=delete

bool	empty () const
	Returns true iff the graph is empty, i.e., contains no nodes. More...

int	numberOfNodes () const
	Returns the number of nodes in the graph. More...

int	numberOfEdges () const
	Returns the number of edges in the graph. More...

int	maxNodeIndex () const
	Returns the largest used node index. More...

int	maxEdgeIndex () const
	Returns the largest used edge index. More...

int	maxAdjEntryIndex () const
	Returns the largest used adjEntry index. More...

node	firstNode () const
	Returns the first node in the list of all nodes. More...

node	lastNode () const
	Returns the last node in the list of all nodes. More...

edge	firstEdge () const
	Returns the first edge in the list of all edges. More...

edge	lastEdge () const
	Returns the last edge in the list of all edges. More...

node	chooseNode (std::function< bool(node)> includeNode=[](node) { return true;}, bool isFastTest=true) const
	Returns a random node. More...

edge	chooseEdge (std::function< bool(edge)> includeEdge=[](edge) { return true;}, bool isFastTest=true) const
	Returns a random edge. More...

template<class CONTAINER >
void	allNodes (CONTAINER &nodeContainer) const
	Returns a container with all nodes of the graph. More...

template<class CONTAINER >
void	allEdges (CONTAINER &edgeContainer) const
	Returns a container with all edges of the graph. More...

node	newNode (int index=-1)
	Creates a new node and returns it. More...

edge	newEdge (node v, node w, int index=-1)
	Creates a new edge (`v`,`w`) and returns it. More...

edge	newEdge (node v, adjEntry adjTgt, int index=-1)
	Creates a new edge at predefined positions in the adjacency lists. More...

edge	newEdge (adjEntry adjSrc, node w, int index=-1)
	Creates a new edge at predefined positions in the adjacency lists. More...

edge	newEdge (adjEntry adjSrc, adjEntry adjTgt, Direction dir=Direction::after, int index=-1)
	Creates a new edge at predefined positions in the adjacency lists. More...

template<typename S , typename T >
edge	newEdge (S src, Direction dirSrc, T tgt, Direction dirTgt, int index=-1)
	Creates a new edge at predefined positions in the adjacency lists. More...

virtual void	delNode (node v)
	Removes node `v` and all incident edges from the graph. More...

virtual void	delEdge (edge e)
	Removes edge `e` from the graph. More...

void	restoreAllEdges ()
	Restore all hidden edges and invalidate all HiddenEdgeSets. More...

virtual edge	split (edge e)
	Splits edge `e` into two edges introducing a new node. More...

void	unsplit (node u)
	Undoes a split operation. More...

virtual void	unsplit (edge eIn, edge eOut)
	Undoes a split operation. More...

node	splitNode (adjEntry adjStartLeft, adjEntry adjStartRight)
	Splits a node while preserving the order of adjacency entries. More...

node	contract (edge e, bool keepSelfLoops=false)
	Contracts edge `e` while preserving the order of adjacency entries. More...

void	move (edge e, adjEntry adjSrc, Direction dirSrc, adjEntry adjTgt, Direction dirTgt)
	Moves edge `e` to a different adjacency list. More...

void	moveTarget (edge e, node w)
	Moves the target node of edge `e` to node `w`. More...

void	moveTarget (edge e, adjEntry adjTgt, Direction dir)
	Moves the target node of edge `e` to a specific position in an adjacency list. More...

void	moveSource (edge e, node w)
	Moves the source node of edge `e` to node `w`. More...

void	moveSource (edge e, adjEntry adjSrc, Direction dir)
	Moves the source node of edge `e` to a specific position in an adjacency list. More...

edge	searchEdge (node v, node w, bool directed=false) const
	Searches and returns an edge connecting nodes `v` and `w` in time O( min(deg(`v` ), deg(`w` ))). More...

void	reverseEdge (edge e)
	Reverses the edge `e`, i.e., exchanges source and target node. More...

void	reverseAllEdges ()
	Reverses all edges in the graph. More...

template<class NODELIST >
void	collapse (NODELIST &nodesToCollapse)
	Collapses all nodes in the list `nodesToCollapse` to the first node in the list. More...

template<class ADJ_ENTRY_LIST >
void	sort (node v, const ADJ_ENTRY_LIST &newOrder)
	Sorts the adjacency list of node `v` according to `newOrder`. More...

template<class IT >
void	sort (node v, IT begin, IT end)
	Sorts the adjacency list of node `v` according to the range denoted by two iterators. More...

void	reverseAdjEdges (node v)
	Reverses the adjacency list of `v`. More...

void	moveAdj (adjEntry adjMove, Direction dir, adjEntry adjPos)
	Moves adjacency entry `adjMove` before or after `adjPos`. More...

void	moveAdjAfter (adjEntry adjMove, adjEntry adjAfter)
	Moves adjacency entry `adjMove` after `adjAfter`. More...

void	moveAdjBefore (adjEntry adjMove, adjEntry adjBefore)
	Moves adjacency entry `adjMove` before `adjBefore`. More...

void	reverseAdjEdges ()
	Reverses all adjacency lists. More...

void	swapAdjEdges (adjEntry adj1, adjEntry adj2)
	Exchanges two entries in an adjacency list. More...

int	genus () const
	Returns the genus of the graph's embedding. More...

bool	representsCombEmbedding () const
	Returns true iff the graph represents a combinatorial embedding. More...

void	consistencyCheck () const
	Asserts that this graph is consistent. More...

internal::GraphNodeRegistry &	nodeRegistry ()
	Returns a reference to the registry of node arrays associated with this graph. More...

const internal::GraphNodeRegistry &	nodeRegistry () const
	Returns a const reference to the registry of node arrays associated with this graph. More...

	operator const internal::GraphNodeRegistry & () const

internal::GraphEdgeRegistry &	edgeRegistry ()
	Returns a reference to the registry of edge arrays associated with this graph. More...

const internal::GraphEdgeRegistry &	edgeRegistry () const
	Returns a const reference to the registry of edge arrays associated with this graph. More...

	operator const internal::GraphEdgeRegistry & () const

internal::GraphAdjRegistry &	adjEntryRegistry ()
	Returns a reference to the registry of adjEntry arrays associated with this graph. More...

const internal::GraphAdjRegistry &	adjEntryRegistry () const
	Returns a const reference to the registry of adjEntry arrays associated with this graph. More...

	operator const internal::GraphAdjRegistry & () const

void	resetEdgeIdCount (int maxId)
	Resets the edge id count to `maxId`. More...

void	resetNodeIdCount (int maxId)

template<OGDF_NODE_ITER NI, OGDF_EDGE_ITER EI, bool copyEmbedding = true, bool copyIDs = false, bool notifyObservers = true>
std::pair< int, int >	insert (const NI &nodesBegin, const NI &nodesEnd, const EI &edgesBegin, const EI &edgesEnd, NodeArray< node > &nodeMap, EdgeArray< edge > &edgeMap)
	Inserts a copy of a given subgraph into this graph. More...

template<OGDF_NODE_ITER NI, OGDF_EDGE_FILTER EF, bool copyIDs = false, bool notifyObservers = true>
std::pair< int, int >	insert (const NI &nodesBegin, const NI &nodesEnd, const EF &edgeFilter, NodeArray< node > &nodeMap, EdgeArray< edge > &edgeMap)
	Inserts a copy of a given subgraph into this graph. More...

template<OGDF_NODE_LIST NL>
std::pair< int, int >	insert (const NL &nodeList, const EdgeSet< true > &edgeSet, NodeArray< node > &nodeMap, EdgeArray< edge > &edgeMap)
	Inserts a copy of a given subgraph into this graph. More...

template<OGDF_NODE_LIST NL>
std::pair< int, int >	insert (const NL &nodeList, const EdgeSet< false > &edgeSet, NodeArray< node > &nodeMap, EdgeArray< edge > &edgeMap)
	Inserts a copy of a given subgraph into this graph. More...

template<OGDF_NODE_LIST NL, OGDF_EDGE_LIST EL>
std::pair< int, int >	insert (const NL &nodeList, const EL &edgeList, NodeArray< node > &nodeMap, EdgeArray< edge > &edgeMap)
	Inserts a copy of a given subgraph into this graph. More...

std::pair< int, int >	insert (const CCsInfo &info, int cc, NodeArray< node > &nodeMap, EdgeArray< edge > &edgeMap)
	Inserts a copy of a given connected component `cc` into this graph. More...

std::pair< int, int >	insert (const Graph &G, NodeArray< node > &nodeMap, EdgeArray< edge > &edgeMap)
	Inserts a copy of a given Graph `G` into this graph. More...

std::pair< int, int >	insert (const Graph &G)
	Inserts a copy of a given Graph `G` into this graph. More...

Protected Member Functions inherited from ogdf::Observable< GraphObserver, Graph >
void	clearObservers ()

const ListPure< GraphObserver * > &	getObservers () const

	Observable ()=default

	Observable (const Observable &copy)=delete
	If you want to copy a subclass of Observable, call the default Observable() constructor. More...

	Observable (Observable &&move)=delete
	If you want to move a subclass of Observable, call the default Observable() constructor. More...

virtual	~Observable ()

Observable &	operator= (const Observable &copy)=delete

Observable &	operator= (Observable &&move)=delete

Private Attributes
std::vector< bool >	m_assignment

std::vector< node >	m_node_map

Additional Inherited Members
Protected Types inherited from ogdf::Graph
enum	EdgeType { EdgeType::association = 0, EdgeType::generalization = 1, EdgeType::dependency = 2 }
	The type of edges (only used in derived classes). More...

enum	NodeType { NodeType::vertex = 0, NodeType::dummy = 1, NodeType::generalizationMerger = 2, NodeType::generalizationExpander = 3, NodeType::highDegreeExpander = 4, NodeType::lowDegreeExpander = 5, NodeType::associationClass = 6 }
	The type of nodes. More...

using	node_iterator = internal::GraphIterator< node >
	Provides a bidirectional iterator to a node in a graph. More...

using	edge_iterator = internal::GraphIterator< edge >
	Provides a bidirectional iterator to an edge in a graph. More...

using	adjEntry_iterator = internal::GraphIterator< adjEntry >
	Provides a bidirectional iterator to an entry in an adjacency list. More...

Protected Attributes inherited from ogdf::Graph
internal::GraphObjectContainer< NodeElement >	nodes
	The container containing all node objects. More...

internal::GraphObjectContainer< EdgeElement >	edges
	The container containing all edge objects. More...

Detailed Description

A simple solver for TwoSAT instances, representing the instance as implication graph and solving it via its strongly-connected components.

Definition at line 71 of file TwoSAT.h.

Member Typedef Documentation

◆ const_iterator

using ogdf::TwoSAT::const_iterator = typename std::vector<bool>::const_iterator

Definition at line 138 of file TwoSAT.h.

◆ const_reverse_iterator

using ogdf::TwoSAT::const_reverse_iterator = typename std::vector<bool>::const_reverse_iterator

Definition at line 139 of file TwoSAT.h.

Constructor & Destructor Documentation

◆ TwoSAT()

ogdf::TwoSAT::TwoSAT ( )

inline

Definition at line 76 of file TwoSAT.h.

Member Function Documentation

◆ begin()

const_iterator ogdf::TwoSAT::begin ( ) const

inline

Definition at line 141 of file TwoSAT.h.

◆ clauseCount()

int ogdf::TwoSAT::clauseCount ( ) const

inline

Definition at line 105 of file TwoSAT.h.

◆ clear()

void ogdf::TwoSAT::clear ( )

inlineoverridevirtual

Removes all nodes and all edges from the graph.

Reimplemented from ogdf::Graph.

Definition at line 133 of file TwoSAT.h.

◆ end()

const_iterator ogdf::TwoSAT::end ( ) const

inline

Definition at line 143 of file TwoSAT.h.

◆ getAssignment()

bool ogdf::TwoSAT::getAssignment ( twosat_var var ) const

inline

Definition at line 131 of file TwoSAT.h.

◆ getNode()

node ogdf::TwoSAT::getNode	(	twosat_var	var,
		bool	sign
	)		const

inlineprotected

Definition at line 165 of file TwoSAT.h.

◆ getNodeIndex()

int ogdf::TwoSAT::getNodeIndex	(	twosat_var	var,
		bool	sign
	)		const

inlineprotected

Definition at line 172 of file TwoSAT.h.

◆ getNodes()

std::pair<node, node> ogdf::TwoSAT::getNodes	(	twosat_var	var,
		bool	flip = `false`
	)		const

inlineprotected

Definition at line 150 of file TwoSAT.h.

◆ newClause()

int ogdf::TwoSAT::newClause	(	twosat_var	var1,
		bool	sign1,
		twosat_var	var2,
		bool	sign2
	)

inline

Definition at line 95 of file TwoSAT.h.

◆ newVariable()

twosat_var ogdf::TwoSAT::newVariable ( )

inline

Definition at line 78 of file TwoSAT.h.

◆ rbegin()

const_reverse_iterator ogdf::TwoSAT::rbegin ( ) const

inline

Definition at line 145 of file TwoSAT.h.

◆ rend()

const_reverse_iterator ogdf::TwoSAT::rend ( ) const

inline

Definition at line 147 of file TwoSAT.h.

◆ solve()

bool ogdf::TwoSAT::solve ( )

inline

Definition at line 110 of file TwoSAT.h.

◆ variableCount()

int ogdf::TwoSAT::variableCount ( ) const

inline

Definition at line 90 of file TwoSAT.h.

Member Data Documentation

◆ m_assignment

std::vector<bool> ogdf::TwoSAT::m_assignment

private

Definition at line 72 of file TwoSAT.h.

◆ m_node_map

std::vector<node> ogdf::TwoSAT::m_node_map

private

Definition at line 73 of file TwoSAT.h.

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

include/ogdf/cluster/sync_plan/basic/TwoSAT.h

OpenGraph DrawingFramework

Public Types

Public Member Functions

Protected Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ const_reverse_iterator

Constructor & Destructor Documentation

◆ TwoSAT()

Member Function Documentation

◆ begin()

◆ clauseCount()

◆ clear()

◆ end()

◆ getAssignment()

◆ getNode()

◆ getNodeIndex()

◆ getNodes()

◆ newClause()

◆ newVariable()

◆ rbegin()

◆ rend()

◆ solve()

◆ variableCount()

Member Data Documentation

◆ m_assignment

◆ m_node_map

Open
Graph Drawing
Framework