#include <ogdf/upward/internal/UpSAT.h>
Public Member Functions | |
| UpSAT (Graph &G) | |
| UpSAT (GraphCopy &G, bool feasibleOriginalEdges) | |
| bool | embedUpwardPlanar (adjEntry &externalToItsRight, NodeArray< int > *nodeOrder=nullptr) |
| long long | getNumberOfClauses () |
| int | getNumberOfVariables () |
| void | reset () |
| bool | testUpwardPlanarity (NodeArray< int > *nodeOrder=nullptr) |
Private Member Functions | |
| void | computeDominatingEdges () |
| void | computeMuVariables () |
| void | computeSigmaVariables () |
| void | computeTauVariables () |
| void | embedFromModel (const Minisat::Model &model, adjEntry &externalToItsRight) |
| bool | FPSS (NodeArray< int > *nodeOrder) |
| bool | HL (bool embed, adjEntry &externalToItsRight, NodeArray< int > *nodeOrder) |
| bool | OE (bool embed, adjEntry &externalToItsRight, NodeArray< int > *nodeOrder) |
| void | ruleFixed (const Minisat::Model &model) |
| void | rulePlanarity () |
| void | ruleSigmaTransitive () |
| void | ruleTauTransitive () |
| void | ruleTutte () |
| void | ruleUpward () |
| void | sortBySigma (List< adjEntry > &adjList, const Minisat::Model &model) |
| void | writeNodeOrder (const Minisat::Model &model, NodeArray< int > *nodeOrder) |
Private Attributes | |
| EdgeArray< List< edge > > | D |
| bool | feasibleOriginalEdges |
| EdgeArray< int > | M |
| Minisat::Formula | m_F |
| Graph & | m_G |
| std::vector< std::vector< int > > | mu |
| NodeArray< int > | N |
| long long | numberOfClauses |
| int | numberOfVariables |
| std::vector< std::vector< int > > | sigma |
| std::vector< std::vector< int > > | tau |
|
explicit |
|
private |
|
private |
|
private |
|
private |
|
private |
| bool ogdf::UpSAT::embedUpwardPlanar | ( | adjEntry & | externalToItsRight, |
| NodeArray< int > * | nodeOrder = nullptr |
||
| ) |
| int ogdf::UpSAT::getNumberOfVariables | ( | ) |
|
private |
|
private |
| void ogdf::UpSAT::reset | ( | ) |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |