OOPS: Optimized One-Planarity Solver via SAT

Abstract

We present OOPS (Optimized One-Planarity Solver), a practical heuristic
for recognizing 1-planar graphs and several important subclasses. A graph
is 1-planar if it can be drawn in the plane such that each edge is crossed at most
once---a natural generalization of planar graphs that has received increasing
attention in graph drawing and beyond-planar graph theory. Although testing planarity can be done in linear time,
recognizing 1-planar graphs is NP-complete, making effective practical algorithms especially valuable.

The core idea of our approach is to reduce the recognition of 1-planarity to a propositional satisfiability (SAT) instance,
enabling the use of modern SAT solvers to efficiently explore the search space. Despite the inherent complexity
of the problem, our method is substantially faster in practice than naïve or brute-force algorithms.
In addition to demonstrating the empirical performance of our solver on synthetic and real-world
instances, we show how OOPS can be used as a discovery tool in theoretical graph theory. Specifically,
we employ OOPS to investigate two research problems concerning 1-planarity of specific graph families.
Our implementation of the algorithm is publicly available to support further exploration in the field.