Advertisement

The Book Embedding Problem from a SAT-Solving Perspective

  • Michael A. BekosEmail author
  • Michael Kaufmann
  • Christian Zielke
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9411)

Abstract

In a book embedding, the vertices of a graph are placed on the spine of a book and the edges are assigned to pages, so that edges of the same page do not cross. In this paper, we approach the problem of determining whether a graph can be embedded in a book of a certain number of pages from a different perspective: We propose a simple and quite intuitive SAT formulation, which is robust enough to solve non-trivial instances of the problem in reasonable time. As a byproduct, we show a lower bound of 4 on the page number of 1-planar graphs.

Keywords

Planar Graph Delaunay Triangulation Conjunctive Normal Form Page Number Outerplanar Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Embedding graphs in books is a fundamental issue in graph theory that has received considerable attention (see, e.g., [5] for an overview). In a book embedding [26], the vertices of a graph are restricted to a line, referred to as the spine of the book, and the edges are drawn at different half-planes delimited by the spine, called pages of the book. The task is to find a so-called linear order of the vertices along the spine and an assignment of the edges of the graph to the pages of the book, so that no two edges of the same page cross; see Fig. 1b. The book thickness or page number of a graph is the smallest number of pages that are required by any book embedding of the graph.

Problems on book embeddings are mainly classified into two categories based on whether the graph to be embedded is planar or not. For non-planar graphs, it is known that there exist graphs on n vertices that have book thickness \(\varTheta (n)\), e.g., the book thickness of the complete graph \(K_n\) is \(\lceil n/2 \rceil \) [3]. Sublinear book thickness have, e.g., graphs with subquadratic number of edges [24], subquadratic genus [23] or sublinear treewidth [13]. Constant book thickness have, e.g., all minor-closed graphs [6] or the k-trees for fixed k [16]. Another class of non-planar graphs that was recently proved to have constant book thickness is the class of 1-planar graphs [2].

For planar graphs, a remarkable result is due to Yannakakis, who back in 1986 proved that any planar graph can be embedded in a book with four pages [33]. However, more restricted subclasses of planar graphs allow embeddings in books with fewer pages. Bernhart and Kainen [3] showed that the graphs which can be embedded in single-page books are the outerplanar graphs, while the graphs which can be embedded in books with two pages are the subhamiltonian ones.

It is known that not all planar graphs are subhamiltonian and the corresponding decision problem whether a maximal planar graph is Hamiltonian (and therefore two-page book embeddable) is NP-complete [32]. However, several subclasses of planar graphs are known to be Hamiltonian or subhamiltonian, see, e.g., [1, 11, 12, 19, 21, 25].

A well-known non-subhamiltonian graph is the Goldner-Harary one [17]. This graph, however, is a planar 3-tree and hence 3-page book embeddable [18]. To the best of our knowledge, there is no planar graph whose page number is four. In other words, it is not known whether the upper bound of four pages of Yannakakis [33] is tight or not.

Our Contribution. We suggest an alternative approach to the problem of determining whether a graph can be embedded in a book of a certain number of pages. We propose a formulation of the problem as a SAT instance, which can be useful in practice (note that, apart from their independent theoretical interest, book embeddings find applications in several contexts, such as VLSI design, fault-tolerant processing, sorting networks and parallel matrix multiplication, see e.g., [11, 20, 28, 30]). It turns out that our formulation is of a simple nature, quite intuitive and easy-to-implement, but simultaneously robust enough to solve non-trivial instances of the problem in reasonable amount of time (e.g., within 20 min we can test whether a maximal planar graphs with up to 400 vertices is 3-page book embeddable), as we will see in our experimental study.

Note that SAT formulations are not so common in graph drawing. A few notable exceptions are [4, 10, 15]. In our context, of interest is the work of Biedl et al. [4], who proposed ILP and SAT formulations for several grid-based graph problems. Their general formulation can be extended to solve our problem as well. However, from the authors’ experimental evaluation (and we could also confirm it) it follows that their approach is limited to solve relatively small instances within reasonable time, e.g., within 20 min one can cope with graphs whose size in vertices and edges does not exceed 100.

A List of Hypotheses. When we started working on this project, we placed several hypotheses that we wanted to prove or disprove. So, before we proceed with the description of our formulation, we first list and then discuss the most important ones:
  • H1: There is a (maximal) planar graph whose book thickness is four.

  • H2: There is a 1-planar graph whose book thickness is (at least) four.

  • H3: There is a (maximal) planar graph, which cannot be embedded in a book of three pages, if the subgraphs embedded at each page must be acyclic.

  • H4: There is a maximal planar graph, say \(G_a\), which in any of its book embeddings on three pages has at least one face whose edges are on the same page.

  • H5: There is a maximal planar graph, say \(G_c\), which in any of its book embeddings on three pages has a face, say \(f^*_c\), whose edges cannot be on the same page.

Summary and Discussion. Clearly, our ultimate goal was to find a planar graph supporting Hypothesis 1. During our extensive practical analysis, we tested several hundreds maximal planar graphs (both randomly created and crafted), but we did not manage to find one supporting Hypothesis 1. We also tested a specific graph with roughly 600 vertices out of the family of planar graphs that Yannakakis proposed to require page number four, but it turned out to be 3-page book embeddable for this particular size.

On the positive side, we proved that the weakest version of Hypothesis 2 holds. In particular, we managed to find a relatively small 1-planar graph whose book thickness is exactly four; see Fig. 1. To the best of our knowledge, this is the first (non-trivial) lower bound on the book thickness of 1-planar graphs.
Fig. 1.

(a) A 1-planar graph, whose underlying planar structure (solid drawn) is the cube graph. (b) A 4-page embedding, in which the fourth page contains a single edge (dotted drawn).

We were surprised that we did not succeed in proving that Hypothesis 3 holds. Note that it is very natural to try to embed a tree-structured subgraph at each of the available pages of the book, if one seeks to prove that indeed all planar graphs can be embedded in books of three pages. For example, Heath [18] who constructively proved that all planar 3-trees fit into books with three pages used exactly this approach: the subgraphs embedded at each of the three pages of the book are acyclic.

Note that we managed to prove a weaker version of Hypothesis 3, according to which the input maximal planar graph has n vertices and cannot be embedded in a book with three pages, so that:(i)the subgraph assigned to each of the three pages is a tree on \(n-1\) vertices and, additionally, (ii) the three vertices, that are not spanned by the three trees are pairwise adjacent forming a face \(f_o\) of the graph, say w.l.o.g. its outerface. This negative results implies that it is not always possible to construct a 3-page book embedding based on a Schnyder decomposition into three trees (regardless of the linear order underneath).

From our experimental evaluation (see Sect. 3), we quickly observed that the practical limitation of testing the book-embedability of maximal planar graphs on three pages with our SAT formulation (that we present in Sect. 2) lies at around 600 to 700 vertices. Larger graphs lead to instance sizes, that excess several gigabytes of random access memory. Hypotheses 4 and 5 in conjunction describe an approach, that could potentially overcome this bottleneck. To see this, assume that the two planar graphs, denoted by \(G_a\) and \(G_c\) in Hypotheses 4 and 5, exist (note, however, that we did not succeed in finding them). If for each face \(f_a\) of \(G_a\), we create a copy of graph \(G_c\) and identify each of the vertices of face \(f^*_c\) of \(G_c\) with one of the vertices of face \(f_a\) of \(G_a\), then we will obtain a (drastically larger) planar graph, that is not 3-page book-embeddable. This is because \(G_a\) must contain at least one face whose edges are on the same page, while in the same time face \(f^*_c\) would require at least one of them not to be at the same page.

2 SAT Formulation

Let \(G=(V,E)\), with \(V=\{v_1,v_2,\ldots ,v_n\}\) and \(E=\{e_1,e_2,\ldots ,e_m\}\), be a graph for which we seek to decide, whether it can be embedded in a book with \(p \ge 2\) pages. Next we describe a logic formula \(\mathcal {F}(G,p)\) that will solve this problem by encoding it as a SAT instance. Recall that any SAT problem can be described in conjunctive normal form (CNF), which is a conjunction of clauses; each clause being a disjunction of (possibly negated) literals. We will define \(\mathcal {F}(G,p)\) by its set of variables and a corresponding set of rules. The rules will ensure the proper assignment of the variables and will be given in propositional logic, which can be converted into CNF clauses straightforwardly [27].

The variables of \(\mathcal {F}(G,p)\) model a book embedding of G in a book with p pages, if it exists. Thus, we use variables \(\sigma (v_i,v_j)\) for each pair of vertices \(v_i, v_j \in V\) to determine, whether vertex \(v_i\) is to the left of vertex \(v_j\) along the spine. If that is the case, the assignment is \(\sigma (v_i,v_j) = \texttt {true}\). In this so-called relative encoding, the variables encode a relative order between the vertices. Clearly, asymmetry has to hold for these variables, which is ensured by the following rule:
$$\sigma (v_i,v_j) \leftrightarrow \lnot \sigma (v_j,v_i)$$
With this asymmetry rule, variables \(\sigma (v_i,v_j)\) can be defined only for \(i < j\). The other literals, \(\sigma (v_i,v_j)\) with \(i > j\), can be replaced by \(\lnot \sigma (v_j,v_i)\). This results in a significantly smaller formula, which is easier to be solved by a SAT solver [31]. The following transitivity rule for the \(\sigma \)-relation ensures a proper order of the vertices along the spine:
$$\begin{aligned} \sigma (v_i,v_j) \wedge \sigma (v_j,v_k) \rightarrow \sigma (v_i,v_k)&\forall \;\text {pairwise distinct}\; v_i,v_j,v_k \in V \end{aligned}$$
The search space of possible satisfying assignments can be reduced by choosing a particular vertex as the first vertex along the spine and by assuming w.l.o.g. that \(v_2\) is to the left of \(v_3\). These choices can be easily encoded by the direction rules:
$$\begin{aligned} \sigma (v_1,v_i)&\forall v_i \in V \; \text {with} \; i > 1\\ \sigma (v_2,v_3)&\end{aligned}$$
Note that the direction rules are represented by unit clauses that fix \(\sigma (v_1, v_i)\), for \(i>1\) and \(\sigma (v_2,v_3)\) to be true. Via unit propagation (that is, a basic operation performed by all SAT solvers [14]) other constraints may become simpler or even already satisfied.
To encode the assignment of the edges to the pages of the book, we introduce a variable \(\phi _q(e_i)\) for every edge \(e_i \in E\) and every possible page \(1 \le q \le p\). Thereby \(\phi _q(e_i) = \texttt {true}\) means that the edge \(e_i\) is assigned to the q-th page of the book. Every edge has to be assigned to one page, which is ensured by the page assignment rule:
$$\begin{aligned} \phi _1(e_i) \vee \phi _2(e_i) \vee \ldots \vee \phi _p(e_i)&\forall e_i \in E \end{aligned}$$
We can again reduce the search space by the fixed page assignment rule, that fixes a single edge on a particular page, e.g., edge \(e_1 \in E\) to page 1:
$$\begin{aligned} \phi _1(e_1) \end{aligned}$$
To forbid crossings among edges of the same page, we first introduce a variable \(\chi (e_i,e_j)\) for each pair of edges \(e_i, e_j \in E\), which describes whether \(e_i\) and \(e_j\) are assigned to the same page. \(e_i, e_j \in E\) are assigned to the same page, if and only if, they are both assigned to one of the available pages, which is ensured by the same page rule:
$$\begin{aligned} (( \phi _1(e_i) \wedge \phi _1(e_j) ) \vee \ldots \vee ( \phi _k(e_i) \wedge \phi _k(e_j) ) ) \rightarrow \chi (e_i,e_j)&\forall e_i,e_j \in E \end{aligned}$$
To ensure planarity, it is enough to ensure that two edges which are assigned to the same page do not cross. So, if \((v_i,v_j), (v_k,v_\ell ) \in E\) are two edges of G, such that vertices \(v_i\), \(v_j\), \(v_k\) and \(v_\ell \) are pairwise different, this can be ensured by the following planarity rule:

Theorem 1

Let \(G = (V,E)\) be a graph and \(p \in \mathbb {N}\). Then, G admits a book embedding on p pages, if and only if, \(\mathcal {F}(G,p)\) is satisfiable. In addition, \(\mathcal {F}(G,p)\) has \(O(n^2+m^2+pm)\) variables and \(O(n^3+m^2)\) clauses.

Proof

The number of \(\sigma \)-, \(\chi \)- and \(\phi \)-variables are \(O(n^2)\), \(O(m^2)\) and O(pm), respectively, which implies that \(\mathcal {F}(G,p)\) has \(O(n^2+m^2+pm)\) variables. The number of clauses of \(\mathcal {F}(G,p)\) is dominated by the number of transitivity, same-page and planarity rules, which yield in total \(O(n^3+m^2)\) clauses. So, to prove this theorem, it remains to show that: (i) a book embedding on p pages yields a satisfying assignment of \(\mathcal {F}(G,p)\) and (ii)a satisfying assignment of \(\mathcal {F}(G,p)\) yields a book embedding on p pages.

(i) From an embedding to an assignment: Assume that G has a book embedding \(\mathcal {E}(G,p)\) on p pages. From \(\mathcal {E}(G,p)\), we obtain an order of the vertices along the spine and an assignment of the edges to the pages. We define an assignment (\(\hat{\sigma },\hat{\phi },\hat{\chi }\)) to the \(\sigma \)-, \(\phi \)- and \(\chi \)-variables of \(\mathcal {F}(G,p)\) consistent with the intended meaning of the variables as follows. (a) \(\hat{\sigma }(v_i,v_j)=\texttt {true}\), if and only if \(v_i\) is before \(v_j\) along the spine, (b) \(\hat{\phi }_q(e_i)=\texttt {true}\), if and only if \(e_i\) is assigned to the q-th page, (c) \(\hat{\chi }(e_i,e_j)=\texttt {true}\), if and only if \(e_i\) and \(e_j\) are assigned to the same page. To prove that assignment (\(\hat{\sigma }, \hat{\phi }, \hat{\chi }\)) satisfies \(\mathcal {F}(G,p)\), we consider all rules of \(\mathcal {F}(G,p)\):
  • The transitivity and asymmetry rules are satisfied by (\(\hat{\sigma }, \hat{\phi }, \hat{\chi }\)), since \(\hat{\sigma }\) is a complete order over the vertices of G (by definition of the assignment).

  • The direction rules are also satisfied, since we can assume w.l.o.g. that in \(\mathcal {E}(G,p)\) vertex \(v_1 \in V\) is the first vertex along the spine and \(v_2\) is to the left of \(v_3\). Note that if this is not the case, then we can circularly-shift the vertices of G along the spine and potentially mirror \(\mathcal {E}(G,p)\) and obtain an equivalent embedding which has the aforementioned properties; see e.g., [33].

  • The page assignment rule is trivially satisfied by the definition of the assignment and the fact that \(\mathcal {E}(G,p)\) was given.

  • The fixed page assignment rule can be satisfied as well, since we can assume w.l.o.g. that the first page of \(\mathcal {E}(G,p)\) is the page where edge \(e_1 \in E\) is assigned to.

  • The same page rule is trivially satisfied due to the definition of the assignment.

  • It remains to show that all planarity rules are satisfied. For the sake of contradiction, assume that the assignment (\(\hat{\sigma }, \hat{\phi }, \hat{\chi }\)) violates a planarity rule for some pair of edges \( (v_i,v_j)\) and \((v_k, v_\ell )\). We know that \(\hat{\chi }((v_i,v_j), (v_k, v_\ell )) = \texttt {true}\) and further \(\hat{\sigma }(v_i,v_k) = \hat{\sigma }(v_k,v_j) = \hat{\sigma }(v_j,v_\ell ) = \texttt {true}\). Hence, in \(\mathcal {E}(G,p)\) we have that \(v_k\) is between \(v_i\) and \(v_j\), while \(v_\ell \) is not between \(v_i\) and \(v_j\). Thus, \((v_i,v_j)\) and \((v_k, v_\ell )\) are on the same page and cross in \(\mathcal {E}(G,p)\), which is a clear contradiction.

(ii) From an assignment to an embedding: Let (\(\hat{\sigma }, \hat{\phi }, \hat{\chi }\)) be a satisfying assignment to \(\mathcal {F}(G,p)\). Let \(\xi : V \mapsto \{ 1 ,\ldots , n \}\) be a function which maps each vertex \(v \in V\) to a position along the spine. Based on (\(\hat{\sigma }, \hat{\phi }, \hat{\chi }\)), map \(\xi \) can be defined as follows:
$$ \xi (v_i) = 1 + | \{ v_j : \sigma (v_j,v_i) = \texttt {true}, 1 \le j \le n,~j \ne i\} |$$
Since (\(\hat{\sigma }, \hat{\phi }, \hat{\chi }\)) satisfies the asymmetry and transitivity rules, it follows that all positions assigned to the vertices of G are pairwise different. Therefore, a proper global ordering is obtained. Since by the page assignment rule, every edge of G is assigned to at least one page, we only have to show that each page is crossing-free. Assume for the sake of contradiction that \((v_i,v_j)\) and \((v_k,v_\ell )\) are two edges of G that are assigned to the same page and cross. In this case, one of the following relationships must hold:
$$\min \{\xi (v_i),\xi (v_j)\} < \min \{\xi (v_k),\xi (v_\ell )\} < \max \{\xi (v_i),\xi (v_j)\} < \max \{\xi (v_k),\xi (v_\ell )\}$$
$$\min \{\xi (v_k),\xi (v_\ell )\} < \min \{\xi (v_i),\xi (v_j)\} < \max \{\xi (v_k),\xi (v_\ell )\} < \max \{\xi (v_i),\xi (v_j)\}$$
However, neither is possible, since both configurations do not comply with the planarity rule of (\(\hat{\sigma }, \hat{\phi }, \hat{\chi }\)). Therefore, each page is crossing-free, as desired.   \(\square \)

So far, we have described a SAT formulation that tests, whether a given graph \(G=(V,E)\) admits an embedding in a book with \(p \ge 2\) pages. Of course, this formulation can be extended with additional variables and rules. In the following, we will introduce three different extensions, which encode Hypotheses 3, 4 and 5.

2.1 A First Variant to check Hypothesis 3

In this subsection, we present a SAT formulation to check Hypothesis 3. Recall that, we seek to check whether a maximal planar graph G can be embedded in \(p=3\) pages, so that the subgraph assigned to each of the three pages is an acyclic graph. In the following, we will extend formula \(\mathcal {F}(G,3)\) with new variables and rules to encode the additional requirement. We denote by \(\mathcal {F}_f(G,3)\) the resulting formula.

Let \(\mathcal {N}(v)\) be the set of vertices adjacent to \(v \in V\). For every edge \((v_i,v_j) \in E\), variable \(\pi _q(v_i,v_j)\) describes, whether vertex \(v_i\) is the parent of vertex \(v_j\) in the forest of page \(q \in \{1,2,3\}\). Variable \(\pi _q(v_j,v_i)\) is defined symmetrically. We ensure, that exactly one of the two variables is true when \((v_i,v_j)\) is assigned to page q, and both of the variables are false, when \((v_i,v_j)\) is not assigned to page q, by the parent rules:
$$\begin{aligned} \phi _q((v_i,v_j))\rightarrow & {} (\pi _q(v_i,v_j) \wedge \lnot \pi _q(v_j,v_i)) \vee (\lnot \pi _q(v_i,v_j) \wedge \pi _q(v_j,v_i))\\ \lnot \phi _q((v_i,v_j))\rightarrow & {} ( \lnot \pi _q(v_i,v_j) \wedge \lnot \pi _q(v_j,v_i) ) \end{aligned}$$
We also have to ensure, that every vertex \(v_i \in V\) has at most one parent vertex in the forest of page q, which can be done via the single parent rule:
$$\begin{aligned} ( \lnot \pi _q(v_k,v_i) \vee \lnot \pi _q(v_\ell , v_i) ),~\forall v_k,v_\ell \in \mathcal {N}(v_i):v_k \ne v_\ell \end{aligned}$$
To ensure acyclicity, we use variables \(\alpha _q(v_i,v_j)\) that describe, whether vertex \(v_i\) is an ancestor of \(v_j\) in the forest of page q. We know that whenever for an edge \((v_i,v_j) \in E\) vertex \(v_i\) is the parent of vertex \(v_j\) on page q, that \(v_i\) is the ancestor for \(v_j\) on that page as well, which results in the parent ancestor rule:
$$\begin{aligned} \pi _q(v_i,v_j) \rightarrow \alpha _q(v_i, v_j) \end{aligned}$$
Clearly, transitivity as well as antisymmetry has to hold for the ancestor relationship:
$$\begin{aligned} (\alpha _q(v_i,v_j) \wedge \alpha _q(v_j,v_k)) \rightarrow&\alpha _q(v_i,v_k) \;&\forall \; \text {pairwise distinct} \; v_i, v_j, v_k \in V\\ \alpha _q(v_i,v_j) \rightarrow&\lnot \alpha _q(v_j,v_i)&\forall \; \text {pairwise distinct} \; v_i, v_j \in V \end{aligned}$$

Theorem 2

Let \(G = (V,E)\) be a (maximal) planar graph. Then, G admits a book embedding on three pages, so that the subgraph assigned to each of the three pages is a forest, if and only, if \(\mathcal {F}_f(G,3)\) is satisfiable.

Proof

We use the same technique as in the proof of Theorem 1. So, consider an embedding \(\mathcal {E}(G,3)\) in three pages yield by our formulation. We claim that the subgraphs embedded at each page are acyclic. For contradiction, assume that there is a cycle \(\mathcal {C}_q\) at page q. If we direct each edge of \(\mathcal {C}_q\) from the child to the parent vertex, then all edges of \(\mathcal {C}_q\) must have the same orientation, that is, either clockwise or counterclockwise along \(\mathcal {C}_q\) (otherwise, there is a vertex of \(\mathcal {C}_q\) that has two parents, deviating the single parent rule). The transitivity of the ancestor relationship implies that the antisymmetry property is deviated along \(\mathcal {C}_q\), which is a contradiction. Hence, the subgraphs embedded at each page of \(\mathcal {E}(G,3)\) are indeed acyclic. Following similar arguments as in the second part of the proof of Theorem 1, we can easily prove that a satisfying assignment of \(\mathcal {F}_f(G,3)\) yields a book embedding on 3 pages, in which the subgraph assigned to each page is a forest, which completes the proof.   \(\square \)

Note that \(\mathcal {F}_f(G,3)\) has asymptotically the same number of variables and clauses as \(\mathcal {F}(G,3)\). Our formulation can be easily adjusted to check whether the subgraph assigned to each page is a tree. In this scenario, we employ an additional variable \(\rho _q(v_i)\) for each vertex \(v_i \in V\) that describes whether \(v_i\) is the root of the tree of page \(q\in \{1,2,3\}\). Vertex \(v_i\) is the root of the tree of page q if and only if it has no parent and (at least) one child at page q, which can be ensured via the following root rule:
$$\begin{aligned} (\bigwedge _{v_j \in \mathcal {N}(v_i) }\lnot \pi _q(v_j,v_i)) \wedge ( \bigvee _{v_k \in \mathcal {N}(v_i) }\pi _q(v_i,v_k) ) \leftrightarrow \rho _q(v_i) \end{aligned}$$
We ensure that there are not two or more roots on the same page q via the single root rule:
$$\begin{aligned} ( \lnot \rho _q(v_i) \vee \lnot \rho _q(v_j) ),~\forall v_i,v_j \in V; i \ne j \end{aligned}$$

2.2 A Second Variant to Check Hypothesis 4

Assume that \(G_a=(V_a, E_a)\) is a maximal planar graph, that is embeddable in a book with 3 pages. Let \(\varDelta (G_a) = \{ f_1,f_2, \ldots ,f_{2\vert V_a \vert -4}\}\) be the set of faces of \(G_a\). In the following, we describe an extension to the formula \(\mathcal {F}(G_a,3)\) that forbids the so-called unicolored faces, that is, faces whose edges are assigned to the same page of the book. We denote the resulting formula by \(\mathcal {F}_a(G_a,3)\).

In comparison to our previous approaches, we are not searching for a single book embedding, for which an additional property holds, but rather we have to test whether all possible book embeddings have this property. We will use the same page variables already present in \(\mathcal {F}(G_a,3)\) to ensure this property via the forbid unicolored face rule:
$$\begin{aligned} (\lnot \chi (e_i, e_j) \vee \lnot \chi (e_i, e_k))&\; \forall f = \{ e_i, e_j, e_k \} \in \varDelta (G_a) \end{aligned}$$

Theorem 3

\(\mathcal {F}_a(G_a,3)\) is unsatisfiable, if and only if, for every possible book embedding \(\mathcal {E}(G_a,3)\) there exists a unicolored face \(f_i \in \varDelta (G_a)\), \(i=1,\ldots ,2|V_a|-4\).

Proof

Directly follows from the validity of \(\mathcal {F}(G_a,3)\).    \(\square \)

2.3 A Third Variant to Check Hypothesis 5

Assume that \(G_c=(V_c, E_c)\) is a maximal planar graph, that is embeddable in a book with 3 pages and let \(\varDelta (G_c)\) be the set of faces of \(G_c\). To check whether a particular face \(f^* = \{e_i, e_j, e_k\} \in \varDelta (G_c)\) cannot be unicolored in any possible book embedding of \(G_c\), we again use the already present same page variables of \(\mathcal {F}(G_c,3)\):
$$\begin{aligned} ( \chi (e_i,e_j) \wedge \chi (e_i, e_k) ), f^* = \{e_i, e_j, e_k\} \in \varDelta (G_c) \end{aligned}$$
The force unicolored face rule yields a new formula, which we denote by \(\mathcal {F}_{c}(G_c;f^*,3)\). By the following theorem, it follows that in order to check Hypothesis 5 one has to check \(2|V_c|-4\), different formulas; one for each face of \(G_c\).

Theorem 4

\(\mathcal {F}_{c}(G_c;f^*,3)\) is unsatisfiable, if and only, if there exists no book embedding of \(G_c\) with \(f^*\) being unicolored.

Proof

Directly follows from the validity of \(\mathcal {F}(G_c,3)\).    \(\square \)

3 Experiments

In this section, we present an experimental evaluation of our SAT formulation. We ran our experiments on a Linux machine with four cores at 2, 5 GHz and 8 GB of RAM. The implementation that creates the SAT instances was done in Java. For solving the SAT instances, we used the SApperloT solver [22]. This solver is as fast as the well-known minisat [14] solver for smaller graphs, but it considerably outperforms minisat for increasing instance sizes. The runtime we report consists of both, the time to create the instance and the time to solve it. Note that the time to create the SAT instance for small graphs is neglectable. For large graphs, however, that step can take a few minutes.

Established Benchmark Sets. Since the Rome and the North graphs are popular test sets for planar and nearly planar graphs, we also used them as test sets for our experiment (cf. http://www.graphdrawing.org). The Rome graphs are 11534 graphs; 3281 of them are planar and 8253 are non-planar. Their average density is 0.069, where the density of a graph \(G=(V,E)\) is \(2|E|/(|V|(|V|-1))\). The number of vertices of the Rome graphs range from 10 to 110. The corresponding number of edges range from 9 to 158.

It is eye-catching, that all planar Rome graphs are 2-page book embeddable (see Table 1). The non-planar ones are 3-page embeddable. But since the Rome graphs are very sparse this result was more or less expected. Note that \(99\,\%\) of the planar Rome graphs (that is, 3248 out of 3282) are solved within 2 s. For the non-planar Rome graphs, the same ratio (that is, 8169 out of 8253) is achieved after 6.25 s.

As a second benchmark set, we used the North graphs which are 1277 graphs; 854 of them are planar and 423 are non-planar. The number of vertices of these graphs range from 10 to 100. The corresponding number of edges range from 9 to 241. Their average density is 0.13. Again, all planar graphs were 2-page book embeddable. The runtime to compute the corresponding embedding for the vast majority of the planar North graphs was rather small. In particular, \(97.5\,\%\) of them (that is, 833 out of 854 graphs) were solved within 3 s, with the maximum runtime being 9.4 s.
Table 1.

Overview of the results for the established benchmark sets.

planar

nonplanar

Graph class

\(\#\)

\(p=2\)

\(\#\)

\(p=3\)

\(p=4\)

\(p=5\)

see below

Rome

3281

3281

8253

8253

0

0

North

854

854

423

329

25

8

61

The non-planar North graphs show the practical limitations of our formulation. In particular, we could determine the page number of only 344 out of 423 graphs within the time limit of 1200 s. Finding a 3-page book embedding is much faster than proving that such an embedding does not exist (see Fig. 2b). For the remaining 79 graphs, we increased the timeout to 3 h and we managed to get at least some partial results: (i) for 18 graphs we computed their exact page number, (ii) 27 graphs fit in four pages but we were not able to determine whether they could fit in three pages, (iii) 32 graphs did not fit in three pages (and 6 out of them did not even fit in four pages), but we did not manage to determine their page number. Nevertheless, all non-planar North graphs could fit into 8 pages and since the focus of the paper is mostly on planar and 1-planar graphs, we did not further investigated the book embeddability of these graphs.
Fig. 2.

(a) Rome graphs: Runtime to compute 2-page embeddings for the planar ones (green) and 3-page embeddings for the non-planar ones (red). (b) Non-planar North graphs: Time needed to compute 3-page embeddings (green) and to prove that no 3-page embedding exist (red). (c) The runtime for maximal 1-planar graphs with 25 vertices. The red curve shows the runtime to prove that no 3-page embedding exist; the green curve shows the runtime to compute 4-page embeddings. (d) The runtime to compute 4-page embeddings for randomized maximal 1-planar graphs.

Crafted Graphs. To prove Hypothesis 1, we also crafted several maximal planar graphs with at least 500 vertices each, which we tested for 3-page book embeddability. To avoid testing Hamiltonian graphs, we adopted a two-step approach that was inspired by the graph class that Yannakakis proposed as candidate to require four pages. In the first step, we chose a triangulated planar (not necessarily non-Hamiltonian) graph as the base for the second step. In the second step, we augmented the base graph by specific operations to make it non-Hamiltonian (and therefore not 2-page embeddable). Examples of these operations are: (i) stellate a face f, that is, introduce a new vertex and connect it to all vertices of f, (ii) replace a triangular face by an octahedron, (iii) embed a non-Hamiltonian planar graph \(G_f\) to a face f by identifying the vertices of f with the vertices of a particular face of \(G_f\).

We observed that these operations most of the times yield non-Hamiltonian planar graphs. Note that they do not generate the whole class of non-Hamiltonian planar graphs and not even a uniformly-distributed random subset. The graphs, that we crafted and tested with this approach, were all maximal planar with at least 500 and at most 700 vertices. The runtime to check each instance ranged from few hours to a couple of days.

1-Planar Graphs. To check Hypothesis 2 for more than four pages, we initially generated all 2,098,675 planar triconnected quadrangulations with 25 vertices and minimum degree three using plantri [8]. By augmenting every face with two crossing edges, the generated quadrangulations yield optimal 1-planar graphs (recall that a 1-planar graph on n vertices is said to be optimal, if it has exactly \(4n-8\) edges, which is the maximum possible [7]). Our experiments showed that all tested optimal 1-planar graphs required four pages. The runtime distribution is shown in Fig. 2c. Computing a 4-page embedding was always fast: For \(99.06\,\%\) of the graphs the solver found a solution within 4.7 s. The maximum runtime for a single instance was 186 s. Proving that no 3-page embedding existed was harder. In less than 5 min., \(94.4\,\%\) of the instances could be solved. However, for very few instances this could take up to two hours.

To obtain a better understanding of the connection between the runtime of our approach and the size of the graphs, we randomly created 8312 optimal 1-planar graphs of different sizes varying from 50 to 155 vertices. Starting from the cube graph (see Fig. 1), we iteratively applied at random one of the two operations described in [29] in order to generate all optimal 1-planar graphs, until we reached the desired size of the graph. The runtime to compute 4-page embeddings for these graphs is shown in Fig. 2d. For nearly all graphs up to 100 vertices a 4-page embedding could be computed within two minutes. However, with increasing vertex-count, the amount of graphs that could take up to several hours to compute a 4-page embedding rises rapidly.

Randomized Planar Graphs. To check Hypotheses 3-5, we generated a large set of random maximal planar graphs as follows. We applied Delaunay triangulation on a set of randomly created points within a triangular region. To avoid Hamiltonian graphs, we stellated every face of the produced Delaunay triangulations. Our results are summarized in the following. Note that none of the tested graphs corroborate Hypotheses 3-5.

  • For Hypothesis 3, we tested 15, 040 maximal planar graphs of varying number of vertices between 25 and 80. We were able to solve \(70.78\,\%\) of the instances (that is, 10, 646 out of 15, 040) within 3 min. and \(76.37\,\%\) (that is, 11, 487 out of 15, 040) of the instances within 20 min., which was the time limit of the computation.

  • For Hypothesis 4, we tested 7, 174 maximal planar graphs of varying number of vertices between 59 and 125. We were able to solve \(92.75\,\%\) of the instances (that is, 6621 out of 7174) within 10 min. and \(99\,\%\) of the instances within an hour. The maximum time that was needed to solve a single instance was 5 h and 6 min.

  • For Hypothesis 5, we managed to test 277, 284 maximal planar graphs of varying number n of vertices between 59 and 95. Every single instance, each containing \(2n-4\) different SAT formulas, required only few seconds to be tested.

4 Conclusions and Discussion

In this paper, we approached the problem of determining whether a graph can be embedded in a book of a given number of pages from a SAT-solving perspective. By elaborating natural hypotheses for planar and 1-planar graphs, we gained valuable insights to the problem. We now tend to believe that the following refined hypotheses hold:
  • H6: All planar graphs admit 3-page book embeddings, in which additionally the subgraphs assigned to each page are trees.

  • H7: Optimal 1-planar graphs have book thickness four.

  • H8: The book thickness of general 1-planar graphs is not more than five.

Our experimental evaluation showed that our approach can be useful, since it can cope with non-trivial instances in reasonable amount of time. However, around the optimal solution, where the problem switches from unsatisfiable to satisfiable, we observed the well-known phase transitional behavior for SAT problems [9]. So, in this context, we mention two more major open problems. The first one is to refine our SAT approach to support denser graphs. The second one is to extend it to other grid-based problems. For example, with our formulation it could be possible to solve larger instances for several of the problems studied, e.g., by Biedl et al. [4].

References

  1. 1.
    Bekos, M., Gronemann, M., Raftopoulou, C.N.: Two-page book embeddings of 4-planar graphs. In: STACS, vol. 25, pp. 137–148. LIPIcs, Schloss Dagstuhl (2014)Google Scholar
  2. 2.
    Bekos, M.A., Bruckdorfer, T., Kaufmann, M., Raftopoulou, C.: 1-planar graphs have constant book thickness. In: Bansal, N., Finocchi, I. (eds.) ESA 2015. LNCS, vol. 9294, pp. 130–141. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  3. 3.
    Bernhart, F., Kainen, P.: The book thickness of a graph. Comb. Theory 27(3), 320–331 (1979)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Biedl, T., Bläsius, T., Niedermann, B., Nöllenburg, M., Prutkin, R., Rutter, I.: Using ILP/SAT to determine pathwidth, visibility representations, and other grid-based graph drawings. In: Wismath, S., Wolff, A. (eds.) GD 2013. LNCS, vol. 8242, pp. 460–471. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  5. 5.
    Bilski, T.: Embedding graphs in books: a survey. IEEE Proc. Comput. Digit. Tech. 139(2), 134–138 (1992)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Blankenship, R.: Book embeddings of graphs. Ph.D. thesis, Louisiana State University (2003)Google Scholar
  7. 7.
    Bodendiek, R., Schumacher, H., Wagner, K.: Über 1-optimale graphen. Math. Nachr. 117(1), 323–339 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Brinkmann, G., Greenberg, S., Greenhill, C.S., McKay, B.D., Thomas, R., Wollan, P.: Generation of simple quadrangulations of the sphere. Discrete Math. 305(1–3), 33–54 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Cheeseman, P., Kanefsky, B., Taylor, W.M.: Where the really hard problems are. In: Mylopoulos, J., Reiter, R. (eds.) AI, pp. 331–340. Morgan Kaufmann (1991)Google Scholar
  10. 10.
    Chimani, M., Zeranski, R.: Upward planarity testing via SAT. In: Didimo, W., Patrignani, M. (eds.) GD 2012. LNCS, vol. 7704, pp. 248–259. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  11. 11.
    Chung, F.R.K., Leighton, F.T., Rosenberg, A.L.: Embedding graphs in books: a layout problem with applications to VLSI design. SIAM J. Algebraic Discrete Method 8(1), 33–58 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Cornuéjols, G., Naddef, D., Pulleyblank, W.: Halin graphs and the travelling salesman problem. Math. Programm. 26(3), 287–294 (1983)CrossRefzbMATHGoogle Scholar
  13. 13.
    Dujmović, V., Wood, D.: Graph treewidth and geometric thickness parameters. Discrete Comput. Geom. 37(4), 641–670 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  15. 15.
    Gange, G., Stuckey, P.J., Marriott, K.: Optimal k-level planarization and crossing minimization. In: Brandes, U., Cornelsen, S. (eds.) GD 2010. LNCS, vol. 6502, pp. 238–249. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  16. 16.
    Ganley, J.L., Heath, L.S.: The pagenumber of \(k\)-trees is \(O(k)\). Discrete Appl. Math. 109(3), 215–221 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Goldner, A., Harary, F.: Note on a smallest nonhamiltonian maximal planar graph. Bull. Malays. Math. Sci. Soc. 1(6), 41–42 (1975)Google Scholar
  18. 18.
    Heath, L.: Embedding planar graphs in seven pages. In: FOCS, pp. 74–83. IEEE Computer Society (1984)Google Scholar
  19. 19.
    Heath, L.: Algorithms for embedding graphs in books. Ph.D. thesis, University of N. Carolina (1985)Google Scholar
  20. 20.
    Heath, L.S., Leighton, F.T., Rosenberg, A.L.: Comparing queues and stacks as machines for laying out graphs. SIAM J. Discrete Math. 3(5), 398–412 (1992)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Kainen, P.C., Overbay, S.: Extension of a theorem of Whitney. Appl. Math. Lett. 20(7), 835–837 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Kottler, S.: Description of the SApperloT, SArTagnan and MoUsSaka solvers for the SAT-competition 2011 (2011)Google Scholar
  23. 23.
    Malitz, S.: Genus \(g\) graphs have pagenumber \(O(\sqrt{q})\). J. Algorithms 17(1), 85–109 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Malitz, S.: Graphs with \(e\) edges have pagenumber \(O(\sqrt{E})\). J. Algorithms 17(1), 71–84 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Nishizeki, T., Chiba, N.: Hamiltonian cycles. In: Planar Graphs: Theory and Algorithms, chap. 10, pp. 171–184. Dover Books on Mathematics, Courier Dover Publications (2008)Google Scholar
  26. 26.
    Ollmann, T.: On the book thicknesses of various graphs. In: Hoffman, F., Levow, R., Thomas, R. (eds.) Southeastern Conference on Combinatorics, Graph Theory and Computing. Congressus Numerantium, vol. VIII, p. 459 (1973)Google Scholar
  27. 27.
    Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbolic Comput. 2(3), 293–304 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Rosenberg, A.L.: The Diogenes approach to testable fault-tolerant arrays of processors. IEEE Trans. Comput. C–32(10), 902–910 (1983)CrossRefGoogle Scholar
  29. 29.
    Suzuki, Y.: Optimal 1-planar graphs which triangulate other surfaces. Discrete Math. 310(1), 6–11 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Tarjan, R.: Sorting using networks of queues and stacks. J. ACM 19(2), 341–346 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Velev, M.N., Gao, P.: Efficient SAT techniques for relative encoding of permutations with constraints. In: Nicholson, A., Li, X. (eds.) AI 2009. LNCS, vol. 5866, pp. 517–527. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  32. 32.
    Wigderson, A.: The complexity of the Hamiltonian circuit problem for maximal planar graphs. Technical report TR-298, EECS Department, Princeton University (1982)Google Scholar
  33. 33.
    Yannakakis, M.: Embedding planar graphs in four pages. J. Comput. Syst. Sci. C–38(1), 36–67 (1989)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Michael A. Bekos
    • 1
    Email author
  • Michael Kaufmann
    • 1
  • Christian Zielke
    • 1
  1. 1.Wilhelm-Schickard-Institut Für InformatikUniversität TübingenTübingenGermany

Personalised recommendations