发表机构
TU Wien（维也纳工业大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明独立数至多为2的双平面图均为9可染的，否定了格思纳和苏兰克关于19顶点反例的猜想，并通过SAT求解与Lean 4形式化验证完成证明。
AI 中文摘要
如果一个图是两个平面图在同一顶点集上的并集，则该图称为双平面图。已知双平面图的最大色数介于9和12之间。下界来自苏兰克图，其独立数为2，而一个具有独立数2的19顶点双平面图的色数至少为10。格思纳和苏兰克在2009年询问这样的图是否存在。我们证明它不存在，更一般地，每个独立数至多为2的双平面图都是9可染的。证明将一个假设的反例嵌入到两个球面三角剖分的并集中，利用SAT模对称性枚举了通过该并集补图必要过滤器的3271个图，并用SAT求解器证明它们都不是这样的补图；一个匹配论证将一般命题归结为这一计算以及一个18顶点上的进一步情形。证明的计算部分，包括枚举的完整性和每个反驳，都在Lean 4中进行了检查，假设了关于平面图的三个经典事实。Lean开发、SAT实例和枚举证书可在Zenodo上获取。
英文摘要
A graph is biplanar if it is the union of two planar graphs on the same vertex set. The largest chromatic number of a biplanar graph is known to lie between 9 and 12. The lower bound comes from Sulanke's graph, which has independence number 2, and a biplanar graph on 19 vertices with independence number 2 would have chromatic number at least 10. Gethner and Sulanke asked in 2009 whether such a graph exists. We show that it does not, and more generally that every biplanar graph with independence number at most 2 is 9-colorable. The proof embeds a hypothetical counterexample in the union of two sphere triangulations, enumerates with SAT modulo symmetries the 3271 graphs that pass a necessary filter for the complement of such a union, and shows with a SAT solver that none of them is such a complement; a matching argument reduces the general statement to this computation and one further case on 18 vertices. The computational part of the proof, including the completeness of the enumeration and every refutation, is checked in Lean 4, assuming three classical facts about planar graphs. The Lean development, the SAT instances, and the enumeration certificates are available on Zenodo.
