Biplanar graphs with independence number two are 9-colorable
Stefan Szeider
math.CO
Sep 23, 2026 · v1
cs.LO
TL;DR
Lean 4 with Mathlib checks the computational proof: completeness of a SAT-modulo-symmetries enumeration and every LRAT refutation, assuming three planarity facts.
Abstract
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.
Problem
Determining the largest chromatic number of biplanar graphs (union of two planar graphs), known to lie in {9,...,12}. Gethner and Sulanke asked whether a 19-vertex biplanar graph with independence number 2 (triangle-free complement) exists, which would force chromatic number at least 10.
Approach
A hypothetical counterexample is embedded in the union of two sphere triangulations. SAT modulo symmetries enumerates 3271 candidate graphs passing a necessary filter for the complement of such a union, and a SAT solver refutes each via an exact-union encoding with lazily added link and separator cuts. A Gallai–Edmonds matching argument reduces the general statement to this computation plus one 18-vertex case. The entire computational part—enumeration completeness via symmetry-breaking clauses, every LRAT refutation, the encoding soundness, and reduction arithmetic—is verified in Lean 4 using Mathlib, assuming three classical planarity facts.
Results
Every biplanar graph with independence number at most 2 is 9-colorable, so no such 19-vertex (or 18-vertex) graph exists, closing the independence-number-2 route to a 10-chromatic example. A 10-chromatic biplanar graph must have independence number at least 3.
| k | 1 | 1 | 2 | 2 | 3 |
|---|
| r | 1 | 6 | 0 | 4 | 1 |
| n | 18 | 13 | 18 | 14 | 16 |
| L(n) | 57 | 12 | 57 | 19 | 36 |
| M | 59 | 7 | 54 | 10 | 21 |
Component cases: edge lower bound L(n) versus computed upper bound M
