OOPS: Optimized One-Planarity Solver via SAT

In this paper, we reduce the gap by designing and implementing a practical heuristic for testing 1-planarity. Besides a naïve exhaustive search to enumerate all possible crossings in a graph, we are aware of only one attempt to implement a general algorithm for recognizing 1-planar graphs [10]. While this backtracking algorithm is carefully engineered, it is not efficient enough to answer basic research questions like “What is the smallest bipartite non-1-planar graph?” or “Is the 28-vertex Coxeter graph 1-planar?”. In contrast, our new algorithm, which we call OOPS (Optimized One-Planarity Solver), provides a substantial speedup and thus capable to answer such questions in seconds.

Our heuristic is based on converting the 1-planarity problem into a propositional satisfiability (SAT) instance, which enables the use of modern SAT solvers. To this end, we design two novel schemes for encoding the 1-planarity of a graph (which is a problem of geometric flavor) into a discrete SAT instance. The first one is based on the Hanani-Tutte characterization of planar graphs, which has been used earlier for designing practical algorithms for upward planarity [15]. This type of encoding is rather flexible and allows to easily extend the algorithm to other use cases, such as 1-planarity of directed graphs. Our second encoding is tailored to 1-planar graphs and exploits a connection to book embeddings. It results in a specifically compact encoding and much faster processing times, and thus, can be an interesting contribution on its own.

We summarize the main contributions of the paper as follows.

• $\mathrm{■}$

  In Section 2 we describe our algorithm for the recognition of 1-planar graphs. It starts with a preprocessing step and an analysis of global properties of the input graph, such as edge density, that can eliminate some obviously non-1-planar instances. Then we present the two SAT encoding schemes for 1-planarity, followed by a set of more involved rules for breaking symmetries and reducing the search space.

• $\mathrm{■}$

  An implementation of the algorithm, OOPS, is open sourced in [34]. The implementation is self-contained and requires only a C++ compiler with C++17 support.

• $\mathrm{■}$

  Section 3 presents an extensive evaluation of the new approach, comparing its efficiency on a suite of benchmark graphs with alternatives. In particular, we provide the status of 1-planarity for named Wikipedia graphs (Table 2). Furthermore, we use OOPS to investigate two theoretical questions concerning 1-planarity regarding the smallest non-1-planar instances for several graph families (Problem 1) and the existence of a subclass of 1-planar graphs with certain properties (Problem 2).

Although the family of 1-planar graphs shares some similarities with planar graphs, there is a fundamental difference. Planarity can be characterized by Wagner’s theorem (forbidden minors $K_5$ and $K_{3,3}$) or by Kuratowski’s theorem (forbidden subdivisions of $K_5$ and $K_{3,3}$). In contrast, every graph admits a 1-planar subdivision, making it impossible to characterize 1-planar graphs via a Kuratowski-type theorem. Testing 1-planarity is $\mathrm{𝖭𝖯}$-complete. The first proof of this result is given by Grigoriev and Bodlaender [24], via a reduction from the 3-partition problem. An independent proof by Korzhik and Mohar [29] uses a reduction from the 3-coloring problem for planar graphs. The recognition problem remains $\mathrm{𝖭𝖯}$-complete even for graphs with bounded bandwidth, pathwidth, or treewidth [8]; for graphs obtained from planar graphs by the addition of a single edge [14], and for graphs with a fixed rotation system [6]. However, the problem becomes fixed-parameter tractable when parameterized by the vertex-cover number, cyclomatic number, or tree-depth [8]. Polynomial-time algorithms are known only for restricted subfamilies of 1-planar graphs [5, 25, 13]. The extensive literature on the topic reflects a strong interest in determining the boundary between tractable and intractable cases. Nevertheless, general-purpose algorithms that are both practical and widely applicable remain lacking.

To prove that a given graph is not 1-planar, one can attempt several approaches. One method is to show that the graph has too many edges, as a 1-planar graph with $n$ vertices has at most $4n-8$ edges [11]; better bounds exist for subclasses such as bipartite 1-planar graphs [27, 26]. Another approach is to leverage the chromatic number: 1-planar graphs are 6-colorable [12], so a graph requiring more colors cannot be 1-planar. Alternatively, one may identify a small non-1-planar subgraph (e.g., a complete multipartite graph [16]), or show that any drawing of the graph necessarily contains too many crossings [17]. However, once a graph passes these basic filters (consider for example a random cubic graph on $30$ vertices), determining whether a 1-planar drawing exists – or proving its nonexistence – remains a challenging and elusive problem. A brute-force approach is practical only for small instances, typically those with up to $16-20$ vertices, depending on the level of engineering effort. For this reason, Eppstein [46], Kobourov, Liotta, and Montecchiani [28] and Binucci, Didimo, and Montecchiani [10] discuss a need for a more powerful technique to attack larger graphs.

We consider a simple undirected graph $G=(V,E)$ with $n$ vertices and $m$ edges. A drawing $\mathrm{\Gamma }$ of $G$ maps vertices $V$ to distinct points of the plane and edges $E$ to Jordan curves connecting corresponding endpoints; the curves may not pass through vertices except their endpoints. Two edges cross if their Jordan curves intersect in a point different from the endpoints. For the ease of notation we often identify a vertex $v\in V$ and its drawing $\mathrm{\Gamma }(v)$ as well as an edge $e\in E$ and its drawing $\mathrm{\Gamma }(e)$. A drawing is planar if every edge is crossing-free, and a graph is planar if it admits a planar drawing. A drawing of a graph partitions the plane into connected regions, called faces; the unbounded region is called the outer face. The set of all faces describes the embedding of a planar graph $G$.

A graph is 1-planar if it admits a 1-planar drawing, that is, a drawing in which every edge is crossed at most once. The planarization of a 1-planar drawing of $G$ is a (planar) graph that replaces each pair of crossing edges, $(u,v)\in E$ and $(x,y)\in E$, by four edges $(u,d),(v,d),(x,d),(y,d)$, where $d$ is a new dummy vertex. The vertices of $G$ in the planarization are referred to as original. There are several important subclasses of 1-planar graphs; for example, optimal 1-planar graphs containing the maximum possible number of edges, $4n-8$ [11]. A graph is IC-planar (independent crossing planar) if it has a 1-planar embedding so that each vertex is incident to at most one crossing edge [1]. In NIC-planar graphs (near-independent crossing planar), two pairs of crossing edges share at most one vertex [39]. Outer 1-planar graphs are another subclass of 1-planar graphs; they admit a 1-planar drawing such that all vertices are in the outer face [5, 25].

We may simplify the testing of 1-planarity of an input graph $G$ by preprocessing the graph and eliminating some instances early. First, we split $G$ into (edge-disjoint) biconnected components and test each component independently, as a 1-planar drawing of $G$ can be easily composed from 1-planar drawings of its biconnected components. Second, we check the edge density of $G$ and reject instances violating the maximum possible density in a 1-planar graph. While there are several density-related results in the area (e.g., for IC and NIC graphs [40, 7]), we apply only the $4n-8$ bound for general graphs [11] and the $3n-8$ bound for bipartite ones [27]. Third, we test if $G$ is planar, which can be done efficiently. Finally, we verify if $G$ is 1-planar with skewness $1$, that is, if it admits a 1-planar drawing in which only one pair of edges cross. This can be done by enumerating all possible pairs of edges, and testing if replacing the pair of crossed edges with a vertex of degree four yields a planar graph.

After the preprocessing step, we may assume that the input graph is biconnected, non-planar, and does not violate the edge density.

To test whether a given graph $G=(V,E)$ admits a $1$-planar drawing, we formulate a Boolean Satisfiability Problem that has a solution if and only if $G$ is $1$-planar. We develop two encoding schemes for the problem; both are based on the concept of a linear graph layout (also referred to as an ordered embedding in [15]). Refer to [35] for a survey of various types of linear layouts. Assume that $G$ admits a 1-planar drawing; planarize it by adding a dummy vertex for every crossing and consider a straight-line planar drawing of the planarization. Now it is easy to perturb the vertices such that they have different $x$-coordinates, which yield a total (linear) order of the vertices; see Figure 1. Observe that the drawing can be modified so that the vertices lie on the same horizontal line (called the spine) while keeping planarity and the vertex $x$-coordinates. The edges in the drawing are curves that are monotone in the $x$ direction; they cannot cross each other but can pass through the spine multiple times, as the red edge $(c,e)$ in Figure 1(c).

Our encoding schemes operate with two auxiliary graphs built as follows. Subdivide every edge of $G$ with a new division vertex to get its subdivision $G^{\prime }=(V^{\prime },E^{\prime })$ with $|E^{\prime }|=2m$ and $|V^{\prime }|=n+m$. The division vertices are $D=V^{\prime }\setminus V$. From $G^{\prime }$ we build another graph, denoted $G_p^{\prime }$, by allowing to merge pairs of division vertices. Let $(u,v)\in E$ and $(x,y)\in E$ be two edges of $G$ that are subdivided by $d_{uv}\in D$ and $d_{xy}\in D$ in $G^{\prime }$. By merging $d_{uv}$ and $d_{xy}$, we get a new (dummy) vertex, $d$, and four new edges in $G_p^{\prime }$, namely $(u,d)$, $(v,d)$, $(x,d)$, and $(y,d)$. The construction of $G_p^{\prime }$ is similar to planarization of (a 1-planar drawing of) $G$, except that $G_p^{\prime }$ contains extra non-merged division vertices. The importance of $G_p^{\prime }$ is shown below.

Here we describe additional tricks to reduce the search space and speed up SAT solvers for recognizing 1-planar graphs. The first one is an improvement to relative variables, $𝕍1$. Observe that constraint $ℂ1$ enforces associativity for pairs of vertices that cannot be merged, including for example, pairs of original vertices. While modern SAT solvers are able to simplify a formula substituting variable $\sigma (v,u)$ with $\neg \sigma (u,v)$ (or vice versa), we found that performing this substitution directly during formula generation reduces both memory usage and solver runtime.

For the next optimization, we exploit a well-known property of 1-planar drawing. Consider a pair of crossing edges $e=(u,v)\in E$ and $f=(x,y)\in E$; then neither of the four adjacent edges (also called the kite edges in [10]) $(u,x),(x,v),(v,y),(y,u)$ can participate in a crossing. This leads to a set of extra constraints that forbid such a crossing: $\neg \chi (e,f)\vee \neg \chi (k,t)$, where $k\in E$ is one of the kite edges corresponding to pair $e,f$ and $t\in E$ is an arbitrary edge of $G$.

A particularly useful technique for improving the effectiveness of our approach is reducing the size of candidate pairs of edges that can cross in a 1-planar drawing, $C$. To this end, consider a potential crossing between edges $e=(u,v)\in E$ and $f=(x,y)\in E$. In certain cases, it might be possible to exchange the positions of $u$ and $x$ (swap $u$ and $x$) while keeping the remaining vertices of $G$ unchanged so as to eliminate the crossing. Consider the neighborhoods (set of adjacent vertices) of $u$ and $x$, that is, $N(u)=\{z:(u,z)\in E\}$ and $N(x)=\{z:(x,z)\in E\}$. If $N(u)\setminus \{v,x,y\}$ coincides with $N(x)\setminus \{u,v,y\}$ and at most one edge out of $(x,v),(u,y)$ is present in $E$, then one can swap $u$ and $x$ and eliminate the crossing from the drawing; see Figure 3(a). Hence, we may assume that $\chi (e,f)=\text{false}$ and remove the pair from the candidate set $C$. An extension of the rule can be applied for multiple crossing pairs. For example, if there are two crossings between $(u,v)\in E$ and $(a,y)\in E$ and between $(c,b)\in E$ with $(x,y)\in E$ and $N(u)=N(x)$ (see Figure 3(b)), then again swapping $u$ and $x$ reduces the number of crossings. In our implementation, we enumerate all possible pairs of crossings and test if swapping two vertices reduces the number of crossings; the corresponding 2-clauses forbidding one of the crossings are then added to the formula.

Finally, we observe that when a 1-planar drawing of a graph exists, it is not unique. In other words, there might be multiple satisfying assignments for a formula. To reduce the search space explored by a SAT solver, we employ symmetry breaking techniques; a similar approach has been used by Bekos, Kaufmann, and Zielke [9] in the context of finding stack layouts of graphs. It is easy to see that one chosen vertex, say $v_0\in V$, can be assumed to be the first in the order. This is enforced by constraints $\sigma (v_0,u)=\text{true}$ for all $u\in V^{\prime }\setminus v_0$. Furthermore, we may force a relative order for twin vertices $u,v\in V^{\prime }$ whose neighborhoods are identical; that is, $\sigma (u,v)=\text{true}$ for pairs of twins $u,v$. Last but not least, we integrate into the implementation of OOPS two generic symmetry-breaking engines, that can analyze the entire formula and add extra constraints without changing its satisfiability.

It is possible to extend the schemes provided in Sections 2.3.1 and 2.3.2 to several other tasks in the area of 1-planarity. Recall that a graph is NIC-planar (resp., IC-planar) if it admits a 1-planar drawing in which two pairs of crossing edges share at most one (resp., zero) vertices. This can be straightforwardly formulated using the following constraints: Let $d_i\in D$ be a division vertex adjacent to original vertices $u_i$ and $v_i$. We consider distinct division vertices $d_i,d_j,d_k,d_t$ and whenever $|\{u_i,v_i,u_j,v_j\}\cap \{u_k,v_k,u_t,v_t\}|>1$ (resp., $>0$), we introduce constraint $\neg \chi (d_i,d_j)\vee \neg \chi (d_k,d_t)$ to forbid a crossing for one of the pairs.

Another interesting extension is for directed acyclic graphs (DAG), whose 1-planarity has been recently studied [3, 4]. In this context, the input is a DAG and the question is whether it admits an upward drawing with at most one crossing per edge; a drawing is upward if for every (directed) edge $(u,v)$, the $y$-coordinate of $u$ is less than the $y$-coordinate of $v$. Our Hanani-Tutte encoding scheme can be applied for the setting by enforcing additional directional constraints $\sigma (u,v)=\text{true}$ for every edge $(u,v)$ of the DAG.

Here we analyze how the SAT-based 1-planarity solver compares to alternative solutions. Arguably the simplest approach for testing 1-planarity is based on an exhaustive search, which enumerates all possible combinations of crossing edges, inserts a dummy vertex for every crossing, and tests whether the resulting graph is planar. We call the heuristic brute-force; refer to [34] for the implementation. Another candidate solver is by Binucci, Didimo, and Montecchiani [10], which we refer to as 1PlanarTester. Since the solver is not open sourced¹¹1There exists an implementation of the algorithm at https://github.com/seemanne/1PlanarTester but a close inspection of the source code reveals substantial gaps both in performance and correctness; thus, we do not use it in our evaluation., we use the same datasets and report the measurements presented in the paper [10]. The algorithms are compared with two versions of our SAT-based solver, described in Section 2.3.1 and Section 2.3.2; they are referred to as OOPS (H-T) and OOPS (Stack), respectively²²2Further heuristics are being developed independently by Fink, Münch, Pfretzschner, and Rutter [22]..

We use the following datasets to compare the solvers:

• $\mathrm{■}$

  north50 graphs is a subset of the north benchmark [45] containing all instances with at most $50$ vertices; all planar graphs have been removed from the collection, resulting in a total of $297$ instances;

• $\mathrm{■}$

  rome50 graphs is a set of all non-planar Rome graphs [45] with at most $50$ vertices; it contains $2950$ instances.

In addition to the real-world graphs, we selected two datasets of graphs containing $45$ edges. The synthetic graph data is generated with the geng tool from nauty [43, 31].

• $\mathrm{■}$

  3reg-gir7 are all $546$ connected cubic ($3$-regular) graphs with $n=30,m=45$ and having girth $7$; all but five instances are known to be 1-planar;

• $\mathrm{■}$

  5reg-b is a random sample of $100$ connected $5$-regular bipartite graphs with $n=18,m=45$; all the graphs are non-1-planar.

We report the results of the experiment in Table 1, which contain the number of identified 1-planar and non-1-planar instances, along with the mean processing times (in seconds) and $95\%$ confidence intervals, for each of the benchmarks. To run the brute-force and OOPS solvers on the data, we use the single-core mode (which is comparable to the configuration reported in [10]) and set the runtime limit for each execution to $3$ minutes; for comparison, the runtime limit of 1PlanarTester in [10] is set to $3$ hours.

One prominent observation from the results is that there is a large gap between SAT-based approaches (OOPS) and the naïve ones (brute-force and 1PlanarTester). In most of the cases, OOPS is able to solve substantially more instances, both in the 1-planar and non-1-planar category. The relatively low runtime of 1PlanarTester suggests that it can handle only “easy” instances that do not require exploring a large search space. Similarly, the performance of brute-force on rome50, where it solves two thirds of the cases, implies that the collection contains many almost-planar graphs that require two or three crossings. The difference becomes striking for the “harder” collections, 3reg-gir7 and 5reg-b, where the exhaustive search is not able to solve any instance, while OOPS (Stack) solves a majority of cases. For this reason, we do not consider existing algorithms as a viable alternative to the new SAT-based technique.

A comparison between Hanani-Tutte and Stack SAT encodings reveals a significant advantage of the latter on all the benchmarks. While both encodings contain $\mathrm{\Theta }({(n+m)}^2)$ variables and $\mathrm{\Theta }({(n+m)}^3)$ constraints, the Stack-based encoding is more succinct, requiring approximately half as many constraints on the data. (Note however, that Hanani-Tutte-based encoding might be more flexible, as discussed in Section 2.5). Thus, we use the Stack-based encoding as a default one in the following experiments.

To further validate OOPS on a real-world benchmark, we apply the algorithm for a collection of named Wikipedia graphs available at [44]. We filtered out all planar instances, and all dense instances with $m>4n-8$ that are obviously non-1-planar, and all instances with $m\ge 100$, which are likely too difficult for our algorithm. The remaining $47$ graphs are tested with OOPS using the Stack-based encoding in the parallel mode. The status of 1-planarity, NIC-planarity, and IC-planarity (refer to Section 2.5) are presented in Table 2. Here we enforce a time limit of $24$ hours for the SAT solver.

To the best of our knowledge, this is the first study of 1-planarity for many of the graphs in the dataset. OOPS is able to determine the status in the majority of the cases. Interestingly, all the unsolved instances (marked TLE in the table) correspond to cubic ($3$-regular) graphs. To understand the performance of OOPS on the data, we plot its runtime as a function of the number of edges in the graph; see Figure 4. We look separately at satisfiable SAT instances (that is, 1-planar graphs) and non-satisfiable ones. Observe that on the benchmark data, every 1-planar graph takes less than $20$ seconds (and less than $50$ seconds for NIC/IC-planar instances). In contrast, most of the non-1-planar instances require substantially more time: the median runtime is around $4$ minutes, the mean is over $1.5$ hours, while the maximum (measured on IC-planarity of Tutte-Coxeter) is $23$ hours. The memory consumption of a SAT solver (Painless in this case) follows the same trend: it is below $4GB$ of RAM for all 1-planar instances but reaches $50-80$GB on the hardest non-1-planar graphs. Given the amount of RAM required for processing non-satisfiable instances, it seems tempting to explore alternative SAT solving strategies, such as cloud-based or incremental, which we leave as a possible future work.

We have also evaluated the encoding optimizations presented in Section 2.4. While the optimizations have a moderate impact on the runtime of OOPS for 1-planar graphs, they are very helpful for large non-1-planar instances. For example, while proving non-1-planarity of the Robertson graph requires $2300$ seconds using the basic encoding (Section 2.3.2), it needs $1750$ seconds with the optimizations, a $24\%$ speed up. For larger instances, the impact is even more pronounced: $30\%$ (reduction from $2$ hours to $85$ minutes) for the Brinkmann graph, and $50\%$ (from $10$ to $5$ hours) for Holt.

Arguably among the most natural applications of a tool for recognizing 1-planar graphs is finding the smallest non-1-planar instance in a family of graphs.

This question has two flavors depending on whether one is interested in vertex-minimal or edge-minimal instances. For planar graphs, it is well-known that smallest non-planar graphs contain $5$ vertices ($K_5$) or $9$ edges ($K_{3,3}$). For 1-planar graphs, it is known that $K_7$ is the smallest complete non-1-planar graphs (see e.g., [16]), however, no such bound is known for non-1-planar edge-minimal graph. To fill the gap, we computationally tested all simple connected instances with up to $m=18$ edges (generated with [43]). All graphs with up to $m=17$ are 1-planar and there are exactly $3$ (out of $164,551,477$ connected) non-1-planar instances with $m=18$; see Figure 5. For bipartite graphs, a graph on $9$ vertices (in fact, $K_{4,5}$ as shown by Czap and Hudák [16]) is one of the two vertex-minimal bipartite non-1-planar graphs. The second such graph, namely $K_{4,5}\setminus e$, is in addition the unique edge-minimal bipartite non-1-planar graph; see Figure 5(d). This is confirmed by testing all $25,124,511$ connected bipartite graphs with $m=19$ and all smaller instances.

A related question (discussed in [47]) is: What is the minimum difference between edge and vertex counts in a connected non-1-planar graph? For planar graphs, one can show (see [47]) that every connected graph with $m\le n+2$ is planar, while non-planar $K_{3,3}$ has $m=n+3$. For 1-planarity, such a condition is unknown. Existing non-1-planar graphs, such as $K_{4,5}$ and $K_{3,7}$ [16], indicate that the difference can be $m-n=11$. The two examples we found (Figures 5(a) and 5(d)) reduce the bound to $10$. It is intriguing to fully resolve the question.

A particularly challenging variant of Problem 1 is to find the smallest 3-regular (cubic) graph that is not 1-planar. While it is easy to show (see e.g., [19]) that random (large) cubic graphs are not 1-planar, the smallest such instance is unknown.

In an attempt to answer the question, Eppstein [46] manually constructed 1-planar drawings of several graphs and suggested that either the Coxeter graph or the Tutte-Coxeter graph is not 1-planar. As pointed out in Table 2, the former is a 1-planar instance; see Figure 6. The latter is very likely non-1-planar, but we were unable to fully verify it, despite running several (parallel) SAT solvers for days. We did, however, verify 1-planarity of (i) all cubic graphs with up to $n=24$ vertices and of (ii) all cubic bipartite graphs with up to $n=30$ vertices. Note that there are around $150\times {10}^6$ such instances and the total computation took $\approx$$1.5$ machine-months (an equivalent of $\approx$$20$ ms per instance).

As another application of OOPS, we investigate the following question proposed by Zhang, Ouyang, and Huang [38] regarding claw-free $1$-planar graphs; recall that a claw is graph $K_{1,3}$.

In fact, the original version of the paper [38] suggests a candidate family, namely the cube of a cycle $C_n$. That is, a graph with vertex set $\{v_0,v_1,\mathrm{\dots },v_{n-1}\}$ in which an edge $(v_i,v_j)$ exists if $\min (|i-j|,n-|i-j|)\le 3$. Such graphs are (i) claw-free, since the neighborhood of any vertex is an interval on the cycle, so no vertex can have three pairwise non-adjacent neighbors, and (ii) $6$-connected (for $n\ge 7$), since to disconnect two vertices, $u$ and $v$, one needs to remove three consecutive vertices going clockwise from $u$ to $v$ and the same counter-clockwise. However, the status of 1-planarity of such graphs is open. Using OOPS, we verified that such graphs are indeed 1-planar whenever $n=8k$ for every $k>0$.