### Upward Planarity Testing in Practice: SAT Formulations and Comparative StudyUpward Planarity Testing in Practice: SAT Formulations and Comparative Study

Access Restriction
Subscribed

 Author Chimani, Markus ♦ Zeranski, Robert Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2015 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data Subject Keyword SAT formulation ♦ Upward planarity ♦ Combinatorial algorithms ♦ Experimental evaluation ♦ Graph drawing ♦ Implementations Abstract A directed acyclic graph (DAG) is upward planar if it can be drawn without any crossings while all edges—when following them in their direction—are drawn with strictly monotonously increasing $\textit{y}-coordinates.$ Testing whether a graph allows such a drawing is known to be NP-complete, and while the problem is polynomial-time solvable for special graph classes, there is not much known about solving the problem for $\textit{general}$ graphs in practice. The only attempt so far has been a branch-and-bound algorithm over the graph’s triconnectivity structure, which was able to solve small graphs. Furthermore, there are some known FPT algorithms to deal with the problem. In this article, we propose two fundamentally different approaches based on the seemingly novel concept of ordered embeddings and on the concept of a Hanani-Tutte-type characterization of monotone drawings. In both approaches, we model the problem as special SAT instances, that is, logic formulae for which we check satisfiability. Solving these SAT instances allows us to decide upward planarity for arbitrary graphs. For the first time, we give an extensive experimental comparison between virtually all known approaches to the problem. To this end, we also investigate implementation issues and different variants of the known algorithms as well as of our SAT approaches and evaluate all algorithms on real-world as well as on constructed instances. We also give a detailed performance study of the novel SAT approaches. We show that the SAT formulations outperform all known approaches for graphs with up to 400 edges. For even larger graphs, a modified branch-and-bound algorithm becomes competitive. ISSN 10846654 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2015-04-01 Publisher Place New York e-ISSN 10846654 Journal Journal of Experimental Algorithmics (JEA) Volume Number 20 Page Count 27 Starting Page 1 Ending Page 27

#### Open content in new tab

Source: ACM Digital Library