独立数が2以下の二重平面グラフは9色で塗れる
Biplanar graphs with independence number two are 9-colorable
この論文をやさしく読む
ひとことで言うと
独立数が2以下の二重平面グラフには、必ず9色以内の彩色があると証明した。
何に役立つ？
グラフ彩色の上限を調べる理論研究や、計算機を使う証明の検証方法に役立つ。直接の実用例は要旨にない。
この研究の面白いところ
2009年に提起された頂点数19の問題を解き、SATでの列挙・反証をLean 4でも検証している。
どこまで分かった？
主張は独立数2以下の二重平面グラフに関するもの。形式検証は平面グラフの3つの古典的事実を仮定している。二重平面グラフ全体の最大彩色数は決めていない。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
同じ頂点集合上にある2つの平面グラフの和で表せるグラフを、二重平面グラフという。二重平面グラフの彩色数の最大値は、9以上12以下であることが知られている。下限は独立数2のSulankeのグラフから得られる。また、独立数2で頂点数19の二重平面グラフが存在すれば、その彩色数は少なくとも10となる。GethnerとSulankeは2009年に、そのようなグラフが存在するかを問うた。本研究では存在しないことを示し、さらに一般に、独立数が2以下の二重平面グラフはすべて9色で彩色できることを示す。証明では、反例と仮定したグラフを2つの球面三角形分割の和に埋め込み、そのような和の補グラフになるための必要条件を通過する3271個のグラフを、対称性を除いてSATで列挙する。そしてSATソルバーを使い、どれもそのような補グラフではないことを示す。マッチングに関する議論により、一般的な主張はこの計算と、頂点数18の場合のもう1つのケースに帰着する。列挙の完全性と各否定の検証を含む証明の計算部分は、平面グラフについての3つの古典的事実を仮定してLean 4で検証している。Leanによる形式化、SATの問題例、列挙の証明書はZenodoで公開されている。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-23（UTC）
- 最新改訂
- 2026-09-23 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-23 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
arXiv ID: 2609.28102 ／ 要約の誤りについて