UpSAT.h

Go to the documentation of this file.

 
#pragma once
 
#include <ogdf/basic/Graph.h>
 
#include <ogdf/external/Minisat.h>
 
#include <vector>
 
namespace ogdf {
class GraphCopy;
template<class E>
class List;
 
class UpSAT {
public:
    //constructor
    explicit UpSAT(Graph& G);
    UpSAT(GraphCopy& G, bool feasibleOriginalEdges);
 
private:
    class Comp;
 
    //FLAGS
    bool feasibleOriginalEdges;
    //copy of the input graph
    Graph& m_G;
    //number of clauses and variables
    int numberOfVariables;
    long long numberOfClauses;
    //Indices of the nodes and edges of m_G
    NodeArray<int> N;
    EdgeArray<int> M;
    //Dominating edges-pairs
    EdgeArray<List<edge>> D;
    //Variables of the formulation(s)
    std::vector<std::vector<int>> tau;
    std::vector<std::vector<int>> sigma;
    std::vector<std::vector<int>> mu;
    //Formula
    Minisat::Formula m_F;
 
public:
    bool testUpwardPlanarity(NodeArray<int>* nodeOrder = nullptr);
    bool embedUpwardPlanar(adjEntry& externalToItsRight, NodeArray<int>* nodeOrder = nullptr);
    long long getNumberOfClauses();
    int getNumberOfVariables();
    void reset();
 
private:
    void computeDominatingEdges();
    void computeTauVariables();
    void computeSigmaVariables();
    void computeMuVariables();
    void ruleTauTransitive();
    void ruleSigmaTransitive();
    void ruleUpward();
    void rulePlanarity();
    void ruleTutte();
    void ruleFixed(const Minisat::Model& model);
    void sortBySigma(List<adjEntry>& adjList, const Minisat::Model& model);
    void embedFromModel(const Minisat::Model& model, adjEntry& externalToItsRight);
    bool OE(bool embed, adjEntry& externalToItsRight, NodeArray<int>* nodeOrder);
    bool FPSS(NodeArray<int>* nodeOrder); // cannot embed
    bool HL(bool embed, adjEntry& externalToItsRight, NodeArray<int>* nodeOrder);
    void writeNodeOrder(const Minisat::Model& model, NodeArray<int>* nodeOrder);
};
 
}