Research · Papers · Exact answers in open problems · MF-188
Uniqueness of (J4,J7;26)-graphs with minimum degree at least 9
(J4,J7;26)-graphs with δ >= 9 form a single isomorphism class: Schläfli complement minus one vertex (degrees 9^10 10^16, 125 edges)
Published 2026-09-06
For everyone
Plain summary
We classify a family of 26-node networks defined by three conditions: no four nodes form a triangle sharing an edge (a 4-node cluster missing one link), every group of seven nodes contains at least two links, and every node connects to at least nine neighbors. An exhaustive automated search shows that exactly one 26-node graph meets all three requirements: the 125-edge graph obtained by removing a single node from the complement of the 27-node Schläfli graph. Earlier work (MR91) proved a uniqueness result for 27-node graphs, but we haven't verified whether this 26-node case was already recorded there.
Result
Let G be an undirected graph on 26 vertices. If G contains no subgraph isomorphic to K_4 - e, every 7-vertex subset of G spans at least 2 edges, and δ(G) >= 9, then G is isomorphic to the Schläfli complement with one vertex deleted.
The isomorphism class is unique. The graph has 125 edges and degree sequence 9^10 10^16.
Setting and definitions
- A (J4,J7;n)-graph is a simple undirected graph on n vertices containing no subgraph isomorphic to K_4 - e such that every subset of 7 vertices spans at least 2 edges.
- The minimum degree δ(G) denotes min { deg(v) : v ∈ V(G) }.
- The vertex-deleted Schläfli complement is the graph obtained by removing one vertex from the complement of the 27-vertex Schläfli graph.
Method
Complete SAT Modulo Symmetries (SMS) enumeration:
- Symmetry breaking: lex-leader formulation on the graph adjacency matrix.
- The 26-vertex encoding generated 2,770,729 variables and 5,433,116 clauses.
- The SMS solver found one satisfying model (the vertex-deleted Schläfli complement) and proved UNSAT after 161 seconds.
- Pipeline validation against Goedgebeur and Van Overberghe, Table 3:
- (J4,J6;15) = 20,266 graphs,
- (J4,J6;16) = 4 graphs,
- (J4,J6;17) = 0 graphs,
all matched identically in runtimes between 11 and 17 seconds.
Discussion
This exhausts the space of (J4,J7;26)-graphs with δ >= 9. Whether (J4,J7;26)-graphs with δ < 9 exist is unrecorded in the register.
MR91 proved uniqueness for the extremal graph at order 27. Whether MR91 records the 26-vertex statement with δ >= 9 remains UNVERIFIED.
For everyone — the takeaway
What this means
Ramsey theory studies the point at which structure becomes unavoidable in graphs. Identifying extremal boundary graphs shows where these structural transitions occur. Pinning down this unique 26-node network completes a step in classifying Ramsey-critical graphs and confirms that symmetry-breaking SAT solvers can resolve these combinatorial searches completely.
Attribution and prior art
Prior art: MR91 proved uniqueness at order 27, but whether the 26-vertex statement appears in that paper remains unverified. Sources: Goedgebeur, Van Overberghe 2021
Register references
- Entry ID: MF-188
- Artifact receipts:
lanes/ramsey-k4e-k8/BANK-CANDIDATES.md(RAM-06, RAM-07); boxfrontier/ramsey/sms/ - Prior art: MR91; Goedgebeur and Van Overberghe, Table 3
Every artifact named above is bundled in, or hashed by, this paper's evidence pack below.
Evidence pack
Everything needed to check this entry against its receipts: the register text, a manifest with a SHA-256 hash for every named receipt, and 1 of 1 receipt files bundled (11 KB). Anything not bundled is still hashed in the manifest and lives in the compute-box working trees.
Changelog
Last reviewed 2026-09-06
- 2026-09-06Published on this site.