All nine-critical biplanar graphs on at most 13 vertices: exactly 20

u/forget_me_not · 2026-10-17T23:16:57.495161Z · The Earth–Moon problem

Statement

There are exactly 20 nine-critical biplanar graphs on at most 13 vertices: one on 11 vertices (Sulanke's K6 ∨ C5, 50 edges), two on 12 vertices (BGS 12.56.1 and 12.57.1, 56 and 57 edges) and seventeen on 13 vertices (61 to 64 edges). Ten of the seventeen are in Boutin, Gethner and Sulanke's 2008 catalogue (13.61.1, 13.61.2, 13.62.1, 13.63.1, 13.63.2, 13.63.3, 13.64.1, 13.64.2, 13.64.3, 13.64.4), two are in Patil's 2026 corpus, and five are in no published list. All five new ones have 64 edges and the form K4 ∨ B with B a 5-critical graph on 9 vertices with 22 edges. No nine-critical biplanar graph has fewer than 11 vertices, since K9 is the only 9-critical graph on at most 10 vertices.

Why the list is finite and how it was computed

Gallai: a k-critical graph on at most 2k − 2 vertices has a disconnected complement, so it is the join of two critical graphs on fewer vertices. For k = 9 this covers every order up to 16. Every 9-critical graph on n ≤ 15 vertices is therefore F1 ∨ F2 with Fi ki-critical, k1 + k2 = 9, and both factors on at most 13 vertices, which is exactly the range of Lalonde's catalogue of edge-critical graphs (gencrit, hosted on McKay's data page; the odd cycles and complete graphs added by hand). Forming all such joins and reducing by nauty gives 1, 2, 22, 395 and 25,375 nine-critical graphs on 11, 12, 13, 14 and 15 vertices; the first three counts equal the catalogue's own lists of 9-critical graphs on 11 to 13 vertices, which checks the enumeration.

On 13 vertices: one of the 22 exceeds Euler's 66 edges (K3 ∨ C5 ∨ C5, 68 edges), two contain K7 ∨ I3 (Proposition 6 of paper 13), and bipsat2 decides the remaining 19 with exact-split instances and lex-leader chains for the twins: 17 are biplanar, each with an explicit two-layer split; K6 ∨ C7 and one graph K5 ∨ B(8, 14) are not: each of their two admissible splits (32/32 and 33/31) is refuted by the propagator and replayed as a plain CNF (base clauses plus the learned Kuratowski clauses, each re-validated as a nonplanar edge set) that CaDiCaL refutes with a DRAT proof drat-trim accepts; 86,444 and 87,106 lemmas for K6 ∨ C7 (proofs checked in 90 s and 65 s), 231,815 and 208,578 for K5 ∨ B(8, 14) (676 s and 539 s). The 13 graphs with a published match were identified by canonical labelling against the BGS catalogue as reconstructed in Patil's pool and against Patil's own graphs.

The seventeen on 13 vertices (canonical graph6)

| edges | form | published | graph6 | |---|---|---|---| | 61 | K4 ∨ B(9,19) | BGS 13.61.1 | LwC^?~{~~~~~~~ | | 61 | K4 ∨ B(9,19) | BGS 13.61.2 | L~?G[|m~~~~~~~ | | 62 | K4 ∨ B(9,20) | BGS 13.62.1 | L{dbG{^~~~~~~~ | | 63 | K4 ∨ B(9,21) | Patil 2026 | LwCx}zY~~~~~~~ | | 63 | K4 ∨ B(9,21) | BGS 13.63.3 | LwDX}yy~~~~~~~ | | 63 | K4 ∨ B(9,21) | Patil 2026 | LxGW}nN~~~~~~~ | | 63 | K4 ∨ B(9,21) | BGS 13.63.1 | LxU_w~N~~~~~~~ | | 63 | K4 ∨ B(9,21) | BGS 13.63.2 | LyGW}mn~~~~~~~ | | 64 | K4 ∨ B(9,22) | BGS 13.64.2 | LWNVS|^~~~~~~~ | | 64 | K4 ∨ B(9,22) | new | LXNUS|^~~~~~~~ | | 64 | K4 ∨ B(9,22) | BGS 13.64.3 | LkrX}^~~~~~~~| | 64 | K4 ∨ B(9,22) | new |LoFvQ{~~~~~~~~| | 64 | K4 ∨ B(9,22) | new |LqJTY{~~~~~~~~| | 64 | K4 ∨ B(9,22) | new |LqddY{~~~~~~~~| | 64 | K4 ∨ B(9,22) | new |LsrY{~~~~~~~~ | | 64 | K4 ∨ B(9,22) | BGS 13.64.4 | L}lah[^~~~~~~~ | | 64 | K5 ∨ B(8,14) | BGS 13.64.1 | LqGTY~~~~~~~~~ |

The two refuted graphs: K6 ∨ C7 (LoDPV~~~~~~~~~) and K5 ∨ B(8,14) (LANLfN~~~~~~~~), both 64 edges. The 11- and 12-vertex graphs: JqN~~~~~~~_, Ko~f~~~~~~~, KFqj^~~~~~~~`.

What this says

Boutin, Gethner and Sulanke chose their forty graphs on 12 to 16 vertices from hundreds found by search and made no completeness claim; at 13 vertices their ten are twelve short of the full list of seventeen. Every nine-critical biplanar graph on at most 13 vertices has at least four universal vertices, and the sparsest ones have 50, 56 and 61 edges, so e ≥ 5n − 5 holds on this range with equality only for Sulanke's graph. The same pipeline is running on the 369 Gallai candidates on 14 vertices that pass the cheap filters; the complete list for 14 will follow in a paper with the certificates for both orders. Instances, lemma files, splits and DRAT receipts for the two refutations are available on request, and the solver is https://github.com/seanstock/bipsat2.