Open
Graph Drawing
Framework

 v. 2022.02 (Dogwood)
 

ogdf::UpSAT Class Reference

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

Detailed Description

Definition at line 47 of file UpSAT.h.

Constructor & Destructor Documentation

◆ UpSAT() [1/2]

ogdf::UpSAT::UpSAT ( Graph G)
explicit

◆ UpSAT() [2/2]

ogdf::UpSAT::UpSAT ( GraphCopy G,
bool  feasibleOriginalEdges 
)

Member Function Documentation

◆ computeDominatingEdges()

void ogdf::UpSAT::computeDominatingEdges ( )
private

◆ computeMuVariables()

void ogdf::UpSAT::computeMuVariables ( )
private

◆ computeSigmaVariables()

void ogdf::UpSAT::computeSigmaVariables ( )
private

◆ computeTauVariables()

void ogdf::UpSAT::computeTauVariables ( )
private

◆ embedFromModel()

void ogdf::UpSAT::embedFromModel ( const Minisat::Model model,
adjEntry externalToItsRight 
)
private

◆ embedUpwardPlanar()

bool ogdf::UpSAT::embedUpwardPlanar ( adjEntry externalToItsRight,
NodeArray< int > *  nodeOrder = nullptr 
)

◆ FPSS()

bool ogdf::UpSAT::FPSS ( NodeArray< int > *  nodeOrder)
private

◆ getNumberOfClauses()

long long ogdf::UpSAT::getNumberOfClauses ( )

◆ getNumberOfVariables()

int ogdf::UpSAT::getNumberOfVariables ( )

◆ HL()

bool ogdf::UpSAT::HL ( bool  embed,
adjEntry externalToItsRight,
NodeArray< int > *  nodeOrder 
)
private

◆ OE()

bool ogdf::UpSAT::OE ( bool  embed,
adjEntry externalToItsRight,
NodeArray< int > *  nodeOrder 
)
private

◆ reset()

void ogdf::UpSAT::reset ( )

◆ ruleFixed()

void ogdf::UpSAT::ruleFixed ( const Minisat::Model model)
private

◆ rulePlanarity()

void ogdf::UpSAT::rulePlanarity ( )
private

◆ ruleSigmaTransitive()

void ogdf::UpSAT::ruleSigmaTransitive ( )
private

◆ ruleTauTransitive()

void ogdf::UpSAT::ruleTauTransitive ( )
private

◆ ruleTutte()

void ogdf::UpSAT::ruleTutte ( )
private

◆ ruleUpward()

void ogdf::UpSAT::ruleUpward ( )
private

◆ sortBySigma()

void ogdf::UpSAT::sortBySigma ( List< adjEntry > &  adjList,
const Minisat::Model model 
)
private

◆ testUpwardPlanarity()

bool ogdf::UpSAT::testUpwardPlanarity ( NodeArray< int > *  nodeOrder = nullptr)

◆ writeNodeOrder()

void ogdf::UpSAT::writeNodeOrder ( const Minisat::Model model,
NodeArray< int > *  nodeOrder 
)
private

Member Data Documentation

◆ D

EdgeArray< List<edge> > ogdf::UpSAT::D
private

Definition at line 65 of file UpSAT.h.

◆ feasibleOriginalEdges

bool ogdf::UpSAT::feasibleOriginalEdges
private

Definition at line 53 of file UpSAT.h.

◆ M

EdgeArray<int> ogdf::UpSAT::M
private

Definition at line 63 of file UpSAT.h.

◆ m_F

Minisat::Formula ogdf::UpSAT::m_F
private

Definition at line 71 of file UpSAT.h.

◆ m_G

Graph& ogdf::UpSAT::m_G
private

Definition at line 57 of file UpSAT.h.

◆ mu

std::vector< std::vector<int> > ogdf::UpSAT::mu
private

Definition at line 69 of file UpSAT.h.

◆ N

NodeArray<int> ogdf::UpSAT::N
private

Definition at line 62 of file UpSAT.h.

◆ numberOfClauses

long long ogdf::UpSAT::numberOfClauses
private

Definition at line 60 of file UpSAT.h.

◆ numberOfVariables

int ogdf::UpSAT::numberOfVariables
private

Definition at line 59 of file UpSAT.h.

◆ sigma

std::vector< std::vector<int> > ogdf::UpSAT::sigma
private

Definition at line 68 of file UpSAT.h.

◆ tau

std::vector< std::vector<int> > ogdf::UpSAT::tau
private

Definition at line 67 of file UpSAT.h.


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