A Forced-Structure Reduction and Verifiable Bounds for Conway's 99-Graph

Summary

This paper reports a systematic, fully reproducible attack on Conway’s 99-graph problem—whether a strongly regular graph with parameters srg(99, 14, 1, 2) exists—conducted by an autonomous AI research agent and scored under the CAISc 2026 Verifiable Problems track’s partial-credit metric. The track scores a submitted 99 × 99 symmetric 0/1 matrix by the fraction of constraints satisfied: 99 degree constraints (row sums 14), one λ constraint per edge, and one µ constraint per non-edge. As every unordered pair is an edge xor a non-edge, the denominator is fixed at 99 + (99 choose 2) = 4950, and a perfect score is a solution to the open problem.

The paper’s verifiable contributions are fourfold. First, an exhaustive proof that no circulant graph on Z/99 satisfies more than 3366/4950 = 68.0% of the constraints (33 of 49 difference-classes), with the same ceiling for the other abelian group of order 99, Z3 × Z3 × Z11. This is stated as Proposition 1: “Over all (49 choose 7) = 85,900,584 symmetric connection sets, the maximum number of satisfied difference-classes is 33; the best circulant scores 99 + 99 · 33 = 3366/4950 = 68.0%.” The proof is by complete enumeration with batched FFT autocorrelation (≈ 100 s on a laptop). An optimal set is S = ±1, ±2, ±4, ±15, ±27, ±36, ±45, with degree 99/99, λ 198/693, µ 3069/4158; the algebra concentrates non-edge common-neighbour counts at 2 (µ at 73.8%, versus ≈ 27% for a random regular graph).

Second, a forced-structure reduction: λ = 1 makes each neighbourhood a perfect matching and µ = 2 puts the outer vertices in bijection with non-matched neighbour-pairs, collapsing existence to a 12-regular graph on 84 vertices, encoded for CP-SAT and validated by recovering the unique srg(9, 4, 1, 2). The reduction is derived as follows: “Fix a vertex 0 with N(0) = 1,..., k. Since λ = 1, each neighbour shares exactly one common neighbour with 0, so the first subconstituent N(0) is a perfect matching [5]; fix it (WLOG) as (1, 2), (3, 4),.... Since µ = 2 on non-edges (0, outer), every outer vertex has exactly two neighbours in N(0); and since µ = 2 on inner non-edges and λ = 1 on inner edges, the outer vertices are in bijection with the non-matched pairs of N(0). Hence the inner–outer adjacency is entirely forced: the outer vertex labelled a, b is adjacent to exactly inner a and b.” The sole unknown is the outer–outer graph: (k−2)-regular on M = (k choose 2) − k/2 vertices, constrained by label-derived λ/µ conditions. For (99, 14, 1, 2) this is a 12-regular graph on 84 vertices. The pipeline is validated end-to-end: it recovers the unique srg(9, 4, 1, 2) in milliseconds, with and without symmetry breaking. The (99, 14, 1, 2) model has 379,987 Booleans and 761,221 constraints; in the authors’ runs it neither returns a graph nor exhausts (the expected outcome for an open problem), so it is released as a validated, maximally-pruned framework.

Third, a validated prescribed-automorphism orbit-existence framework (fixed-point-free and single-fixed-point actions, checked on srg(9, 4, 1, 2) and the Paley graph srg(13, 6, 2, 3)). The framework builds on the orbit-matrix method of Behbahani and Lam and the automorphism results of Cesarz and Woldar, which prove that Aut of any such graph is severely constrained: orders 9 and 11 are excluded; if 2 G then G 6; and if 7 G then G ≅ Z7. Order 7 is thus constrained but not ruled out: whether a Z7-symmetric srg(99, 14, 1, 2) exists is itself open. The encoding supports both the fixed-point-free case (semiregular p 99) and the single-fixed-point case (the fixed vertex joins full orbits, forced by 14 = 2 · 7 to exactly two of them). The encoding is validated end-to-end: it reconstructs and re-verifies srg(9, 4, 1, 2) (both a fixed-point-free Z3 and an order-2 action with one fixed point) and the Paley graph srg(13, 6, 2, 3) (order-3, one fixed point). For the genuinely open sub-cases, CP-SAT returns UNKNOWN even after a 48-hour run on 14 cores for the single-fixed-point Z7 model, and UNKNOWN within 1800 s for the fixed-point-free Z3 model (33 orbits). The authors record this as an honest negative methods finding: “even on an open sub-case where a specialised orbit-matrix enumeration would terminate, off-the-shelf CP-SAT does not, in our hands, decide the instance, and its persistence across a 96× longer budget points to a structural barrier in the general-purpose encoding rather than a mere time shortfall.”

Fourth, a best verified artifact at 69.43% (3437/4950), with evidence that this is a robust frontier (fourteen distinct methods, none exceeding it) entangled with the open question, since any provable bound below 4950 is a non-existence proof. The heuristic frontier is obtained by optimising the blend O(A) = real(A) − α SE(A), which keeps the true objective primary while −αSE supplies a descent direction across plateaus, inside an island-model evolutionary algorithm with degree-preserving crossover. Table 1 summarises the frontier: exhaustive circulant (Z/99) at 68.0%, Cayley search (Z3×Z3×Z11) at 68.0%, block CP-SAT (Z/11, Z/9, Z/3) at 68.0%, full MaxSAT (504,504 vars) at 68.0%, degree-preserving 2-opt SA at ≈ 56%, tabu/ILS at 69.3%, and min-conflicts; blended SA + island EA at 69.43%. The best artifact has degree 69/99, λ 374/708, µ 2994/4143. Every high-scoring solution sits near λ ≈ 53%, µ ≈ 72%, the circulant is a strict 2-opt local maximum, and large-neighbourhood CP-SAT re-optimisation of 14-vertex chunks yields only lateral moves. Restarting min-conflicts from the best artifact with elevated noise explored 1.57 × 10 6 accepted moves without satisfying a single additional constraint. The frontier is a strict local optimum, not a tuning artifact.

The paper also notes that first and second moments give no contradiction: for any 14-regular graph, the sum over i<j of Cij equals v(deg choose 2) = 99(14 choose 2) = 9009, while the targets sum to 693 · 1 + 4158 · 2 = 9009: exactly equal. The feasible spectrum fixes the sum of Cij squared, again matched by the targets. A practical corollary is that near degree 14 the λ- and µ-satisfaction are coupled: one cannot cheaply maximise µ alone, because the common-neighbour budget is tight, so a high partial score forces genuine near-strong-regularity.

The paper explicitly disclaims any resolution of existence: “We are explicit that we neither construct the graph nor prove non-existence; our contributions are verifiable bounds, a validated reduction, a reusable framework, and the documented trajectory.” The agent trajectory is reported per the track’s interest: the agent first encoded the problem for an SMT solver and stalled on the global connectivity/structure constraints; a corrective pivot to a CP-SAT solver gave order-of-magnitude speedups and unlocked the exhaustive circulant bound and the block models; pushed for rigour, the agent then derived and validated the forced-structure reduction, implemented the orbit-existence encoding, and, after a literature review establishing the open status and the automorphism results, re-scoped its claims to verifiable bounds and an explicit non-claim on existence. A final construction attempt prioritised the single most structurally-justified model (the open single-fixed-point Z7 orbit case) over undirected search, ran it to a 48-hour budget, and reported its inconclusive (UNKNOWN) outcome as such.

Limitations are stated: existence is unresolved; the 69.43% artifact is a partial score; the ≈ 69% frontier is a search-landscape observation (not a proven global bound); and general-purpose CP-SAT did not decide the prescribed-automorphism sub-cases, including the genuinely open single-fixed-point Z7 case, which stayed UNKNOWN even after a 48-hour, 14-core run. The circulant bound (Prop. 1) and the reduction validation are the rigorous, reproducible results. The paper concludes that crossing the partial-credit frontier toward the “high 90s” is not a separate engineering target but is entangled with the open problem: “a 95% near-SRG is as structurally delicate to find as the graph.”

Based on the paper, here are the specific improvements I can make to an AI system, and what the improved system can do:

1. Add a Verifiable-Claim Enforcement module

• What it does: Before any result is reported, the system must classify it as proven, empirical, or open. It must attach a certificate (e.g., exhaustive enumeration log, solver output, or explicit UNKNOWN status) to every claim. If a claim lacks a certificate, the system must downgrade it or refuse to state it.

• Why: The paper's core failure mode was over-claiming. The agent repeatedly had to be corrected toward certifiable statements. This module makes that correction automatic.

2. Add a Moment-Consistency Precheck

• What it does: Before launching any search, the system computes the first and second moments of the target constraints (e.g., sum of common-neighbour counts) and checks whether they match the feasible spectrum. If they match, the system flags that no cheap contradiction exists and that the problem is genuinely hard, preventing wasted effort on trivial impossibility arguments.

• Why: The paper shows that the 99-graph parameters pass all moment tests, which is why the problem resists easy attacks. The system should know this before searching, not after.

3. Add a Forced-Structure Reducer

• What it does: Given a strongly regular parameter set (v, k, λ, µ), the system automatically derives forced substructures (e.g., λ=1 ⇒ neighbourhood is a perfect matching; µ=2 ⇒ outer vertices are in bijection with non-matched neighbour-pairs). It then reduces the problem to a smaller, constrained graph (e.g., from 99 vertices to 84 vertices) and encodes that reduced problem for a solver.

• Why: This is the paper's most reusable contribution. The system should not just search the full space; it should first prune it using forced structure.

4. Add a Prescribed-Automorphism Orbit Encoder

• What it does: For a given automorphism order p, the system automatically constructs the block-circulant orbit model, handles fixed-point-free and single-fixed-point cases, and encodes the strong-regularity conditions as a single common + adjacency = 2 constraint per orbit-pair class.

• Why: This is a clean, validated framework that the system can reuse for any srg(v, k, λ, µ) with a prescribed automorphism, not just the 99-graph.

5. Add a Blended-Objective Local Search

• What it does: When the true objective (exact constraint satisfaction) is flat (no gradient), the system automatically switches to a blended objective O(A) = real(A) − α·SE(A), where SE is the squared error of common-neighbour counts. This gives a descent direction across plateaus.

• Why: The paper shows that exact-match scoring stalls local search; the blend is what allowed the system to reach 69.43%. This should be a default strategy, not a manual intervention.

6. Add a Negative-Result Logger

• What it does: When a solver returns UNKNOWN or times out, the system must log this as a negative finding (not a failure), record the budget, the solver, and the instance, and explicitly state that the result is inconclusive. It must not silently discard these outcomes.

• Why: The paper's honest reporting of the 48-hour UNKNOWN on the Z7 case is a model of scientific integrity. The system should be trained to do this automatically.

1. Prove or disprove circulant bounds for any srg(v, k, λ, µ) by exhaustive enumeration with FFT autocorrelation, in seconds to minutes on a laptop.

2. Automatically reduce any srg(v, k, 1, 2) to a smaller forced-structure graph and validate the reduction on known cases (e.g., srg(9, 4, 1, 2)) before attempting the open case.

3. Encode and solve prescribed-automorphism existence questions for any srg(v, k, λ, µ) with a given automorphism order, including fixed-point-free and single-fixed-point actions, and report SAT/UNSAT/UNKNOWN with full certificates.

4. Run a degree-preserving, blended-objective evolutionary search that reliably finds near-strongly-regular graphs and reports the best artifact with a verifiable score, without over-claiming.

5. Automatically detect when a problem is genuinely hard (moments match, no trivial obstruction) and adjust its strategy accordingly—e.g., switch from general-purpose SAT to specialised orbit-matrix or forced-structure methods.

6. Produce a paper-ready report where every claim is tagged as proven, empirical, or open, with attached certificates, and where all negative results are honestly logged.

In short: the improved system is a self-correcting, certificate-driven combinatorial search agent that prunes using forced structure, searches using blended objectives, and reports only what it can prove—exactly the behaviour the paper's authors had to manually enforce.

Conway's 99-graph problem asks whether a strongly regular graph with parameters srg(99,14,1,2) exists. We report a systematic, fully reproducible attack by an autonomous AI research agent, scored under the track's partial-credit metric. Our verifiable contributions are: (1) an exhaustive proof that no circulant graph on Z/99 satisfies more than 3366/4950=68.0% of the constraints (33 of 49 difference-classes), with the same ceiling for the other abelian group of order 99; (2) a forced-structure reduction: lambda=1 makes each neighbourhood a perfect matching and mu=2 puts the outer vertices in bijection with non-matched neighbour-pairs, collapsing existence to a 12-regular graph on 84 vertices, encoded for CP-SAT and validated by recovering the unique srg(9,4,1,2); (3) a validated prescribed-automorphism orbit-existence framework (fixed-point-free and single-fixed-point actions, checked on srg(9,4,1,2) and the Paley graph srg(13,6,2,3)), and (4) a best verified artifact at 69.43%, with evidence that this is a robust frontier (fourteen distinct methods, none exceeding it) entangled with the open question, since any provable bound below 4950 is a non-existence proof.