最小的三次非1-平面图
Smallest Cubic Non-1-Planar Graphs
AI总结：
本文证明最小的三次非1-平面图有30个顶点，并借助SAT求解器与k-灵活性方法，避免了穷举四十亿个图的计算。
AI中文摘要：
如果一个图存在一种画法使得每条边至多被交叉一次，则该图是1-平面的。我们证明了最小的三次非1-平面图有30个顶点。这样的图有两个：围长为8的Tutte-Coxeter图和围长为7的我们称之为Byte图的图。所有少于30个顶点的次三次图都是1-平面的。我们的证明是计算机辅助的，但直接测试所有相关图是不切实际的。为了确立这两个图的非1-平面性，我们扩展了一个基于SAT的求解器，加入了一个基于分离环的定制子句传播器和一个基于图自同构的案例分割，使得独立的案例可以并行求解。为了证明所有更小的次三次图都是1-平面的，我们引入了k-灵活性的概念：每个至多k条指定边的集合在某个1-平面画法中可以不交叉。我们利用这一性质从更小的k-灵活图的画法重构更大图的1-平面画法。这用对远少于四十亿个三次图的计算取代了对超过四十亿个三次图的穷举测试。
英文摘要：
A graph is 1-planar if it has a drawing in which every edge is crossed at most once. We show that the smallest cubic non-1-planar graphs have $30$ vertices. Two such graphs are the Tutte-Coxeter graph of girth eight and a graph of girth seven that we call the Byte graph. Every subcubic graph with fewer than $30$ vertices is 1-planar. Our proof is computer-assisted, but directly testing all relevant graphs is impractical. To establish non-1-planarity of the two graphs, we extend a SAT-based solver with a custom clause propagator based on separating cycles and a case split based on graph automorphisms, allowing independent cases to be solved in parallel. To show that all smaller subcubic graphs are 1-planar, we introduce the concept of $k$-flexibility: every set of at most $k$ prescribed edges can remain uncrossed in some 1-planar drawing. We use this property to reconstruct 1-planar drawings of larger graphs from drawings of smaller $k$-flexible graphs. This replaces exhaustive testing of more than forty billion cubic graphs with computations on far fewer graphs of smaller order.
