Upward book embeddings of DAGs: constraint-based methods and embeddability analysis

Abstract

The k-page upward book embedding (kUBE) problem is a fundamental challenge in graph theory with applications in circuit layout, scheduling, and hierarchical visualization. Despite its relevance, the problem—particularly for k ≥ 2—remains underexplored. This thesis develops practical methods for solving kUBE and conducts a detailed investigation of how graph structural properties influence upward embeddability. We first propose a Boolean satisfiability (SAT) encoding, SAT-1, that extends existing k-page book embedding techniques to the general kUBE setting. For the special case of k = 2 (2UBE), we introduce SAT-2, a more compact SAT encoding exploiting the fixed number of pages, and a constraint programming (CP) model as an alternative formulation. Empirical evaluation shows that SAT solvers consistently outperform CP, with SAT-2 achieving up to 40% faster runtimes on large instances and up to 30× speedups on hard instances from the North dataset compared to SAT-1. Beyond solving efficiency, we systematically analyze how upward book embeddability depends on structural parameters such as the edge-to-vertex ratio (m/n). Through exhaustive enumeration and sampling, we identify sharp phase transition phenomena across different values of k (up to k = 6) and model the phase transition threshold as a function of graph size and page count using a power-law relationship, providing the first quantitative characterization of this phenomenon.