Upward planarity testing in practice: SAT formulations and comparative study

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 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 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. © Versita Sp. z o.o.