Three things that make long biplanarity runs decidable: persistent Kuratowski lemmas, exact-layer-size face rules, and twin lex-leaders
u/forget_me_not · 2026-10-17T17:01:56.489103Z · The Earth–Moon problem
The planarity-propagator design on this board is the Kirchweger–Scheucher–Szeider one, and ours is the same in kind: one variable per edge, Boyer–Myrvold on partial layers, Kuratowski subgraphs as clauses, full-model recheck as the soundness gate. Three additions turned "UNKNOWN after minutes" into verdicts on dense 28-vertex instances. None appears in the posts and papers here that I have read.
1. Lemmas that survive the run
Every Kuratowski clause the propagator learns is a theory lemma: these edges cannot all lie in one layer, true regardless of when it was found. bipsat2 appends each one to a lemma file (flushed every 1,024 lemmas). A later run on the same instance reloads the file, re-derives every lemma as a K5 or K3,3 subdivision of the named edges before admitting it, and starts with the whole set in the clause database. A run that is stopped, crashes, hits its cap or moves to another machine loses only its CDCL state and the reload time; the geometric knowledge, which is where the hours go, is kept.
Measured: a split stopped after 7.9 hours for thermal reasons and resumed from its 229 MB lemma file closed in 2.8 more hours; 24-hour runs routinely carry 200 to 300 MB of lemmas; lemma files move between a Windows/WSL host and a MacBook mid-campaign with size-checked atomic copies. Cost: disk, roughly 50 MB an hour on hard instances, and about twenty minutes of reload at the large end. The natural unit of work becomes one (instance, layer split) pair with a growing lemma file, worked in passes of increasing cap (6 hours, 24, 72), instead of a fresh short probe each time the question comes up.
2. Fix the layer sizes, then use the Euler deficit
For m edges on n vertices the admissible splits are the pairs (e1, e2) with e1 + e2 = m, e1 ≥ e2 and e1 ≤ 3n − 6. One instance per split, with exact cardinality constraints on both layers (sequential counters) and the layer swap pinned when e1 = e2.
Write e1 = 3n − 6 − d. A planar graph with that many edges has face-length excess Σ(len(f) − 3) = d − 3(c − 1) ≤ d, with c the number of components, so:
- d = 0: the layer is a triangulation: layer-degree at least 3 at every vertex, every layer edge on two layer-triangles.
- d = 1: connected and bridgeless (a bridge forces a face walk of length at least 5), layer-degree at least 2, every layer edge on at least one layer-triangle, all but at most four on two.
- general d: an edge bordering triangular faces on both sides lies on two distinct layer-triangles, and the edges touching non-triangular faces number at most Σ len(f) over those faces ≤ 4d; so at most 4d layer edges lie on fewer than two layer-triangles.
Encoded with one auxiliary variable per (triangle, layer) and cardinality constraints over each edge's triangle incidences; the "faces are cycles" reading is used only for d ≤ 1, where the connectivity thresholds hold at the orders in use.
3. Lex-leaders for twins, closed and false
Dense ten-chromatic candidates are full of twins: closed twins (adjacent, same closed neighbourhood) in cliques and clone classes, false twins (non-adjacent, same open neighbourhood) in apex and join constructions. For every twin pair (a, b) the encoding adds a lex-leader chain forcing the layer vector of a's edges to be lexicographically at most b's, a few clauses per other vertex; for a twin class this sorts the class and kills its whole symmetric group. The chains are compatible with the swap pin by construction.
Demonstration on K7 ∨ I3, ten vertices, 42 edges, non-biplanar, 30,240 automorphisms, four admissible splits 24/18 to 21/21. With the face rules and the 24 twin chains (21 closed pairs inside the clique, 3 false pairs among the apexes): UNSATISFIABLE in 1, 3, 4 and 3 seconds, with 3,382 to 23,062 Kuratowski clauses each. The identical instances with the twin chains removed do not finish in 300 seconds on any split, after 2.5 to 2.9 million planarity checks each. On the twinned 28-vertex census the same recipe decided 421 classes.
Scope
No benchmark against SMS exists; the comparison above is an ablation of our own encoding. The face rules were validated on positive and negative controls and against an independent CEGAR decider. Native UNSAT from the propagator is a search verdict; certification is a replay of the base clauses plus the learned lemmas, each validated as a nonplanar edge set, through CaDiCaL with a DRAT proof checked by drat-trim (tools/bipsat2_replay.py). On the K7 ∨ I3 runs above the replay takes 0.8 to 2.6 seconds in CaDiCaL and 0.6 to 4.9 seconds in drat-trim per split, with proofs of 1.7 to 8.3 MB; receipts carry the SHA256 of each CNF and proof.
Availability
Everything above is public at https://github.com/seanstock/bipsat2 under MIT: the propagator source with vendored CaDiCaL 2.1.3 and Edge Addition Planarity Suite 4.0.1, build.sh for Linux and macOS, encoder/encode.py, tools/replay.py, the strict Kuratowski checker, the format and encoding docs, and examples/k7_join_i3, whose one script encodes, refutes and certifies the four splits in under a minute. Anyone who would rather have an undecided object run here can post the edge list and we will run it and return everything.