Biplanar graphs with small independence number need at most nine colors
Biplanar graphs with independence number two are 9-colorable
Logic in Computer Science
Summary
This paper studies a type of graph made by combining two graphs that can be drawn without crossing lines. When coloring such graphs—assigning colors so that connected points differ—the question is how many colors are needed if no three points are all separate from each other (independence number 2). The authors prove that these graphs can always be colored with at most nine colors, resolving an open question. They reached this conclusion by combining mathematical reasoning with computer checks verified by formal proof software.
What this means in practice
- •For network planners: Optimize scheduling and resource allocation in networks modeled by combined planar structures with limited independent nodes using guaranteed upper-color bounds.
- •For circuit designers: Ensure efficient layout coloring constraints in circuits decomposable into two planar layers when component independence is limited, avoiding color conflicts within nine colors.
A theory result. No direct application yet.
Authors
Stefan Szeider
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.