#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 |