Pith. sign in

REVIEW 2 major objections 29 references

Approaching the Conway-99 problem using SAT solvers

T0 review · 2 major / 0 minor · reviewed 2026-05-08 · grok-4.3

Challenge this review Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that translating the Conway-99 problem into SAT instances shows current solvers cannot resolve it in reasonable time.

desk verdict The paper reduces Conway-99 to SAT and reports timeouts but supplies no encoding details or data, so the negative result cannot be checked. read the letter →

arxiv 2604.23037 v2 submitted 2026-04-24 cs.LO

Ali Keramatipour This is my paper · ORCID
classification cs.LO
keywords Conway-99problemstronglyregulargraphsSATsolversbooleansatisfiabilitygraphexistencecomputationalsearchencoding
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The Conway-99 problem asks whether a strongly regular graph with 99 vertices and fixed parameters exists. The paper converts the graph's adjacency and neighbor-count rules into boolean clauses that a SAT solver can process. Experimental runs on the resulting instances demonstrate that solvers exhaust time limits without producing a solution or a proof of non-existence. The work then traces this outcome to the scale and structure of the constraints imposed by the graph definition.

What carries the argument

The reduction of strongly regular graph conditions (regular degree, fixed common neighbors for adjacent and non-adjacent pairs) to a conjunction of boolean clauses.

What would settle it

A single run in which the SAT solver returns a satisfying assignment that corresponds to a valid 99-vertex strongly regular graph, or returns an unsatisfiability proof, all within the tested time limit.

Watch

Extended reading notes

Core claim

Encoding the existence question for a strongly regular graph on 99 vertices into a boolean satisfiability formula produces instances that modern SAT solvers cannot decide within practical time bounds, establishing the current incapability of this approach and indicating deeper mathematical sources of the difficulty.

Load-bearing premise

The chosen encoding fully and correctly captures every possible graph meeting the strongly regular conditions without missing solutions or adding false constraints.

Editorial extensions

If this is right

  • Standard SAT solvers cannot be used to settle the Conway-99 problem on current hardware within reasonable limits.
  • Alternative or specialized search methods are required to either construct the graph or prove it does not exist.
  • The finite search space remains intractable when expressed through this particular constraint set.
  • The observed limits arise from both instance size and the combinatorial structure of the neighbor conditions.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same encoding technique could be applied to smaller strongly regular graphs with known answers to check for modeling accuracy.
  • Hybrid solvers that combine SAT with graph-specific pruning might extend the reachable problem size.
  • Direct mathematical arguments about eigenvalue bounds or automorphism groups may prove more decisive than exhaustive search for this case.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 0 minor

Summary. The manuscript claims that the Conway-99 problem (existence of a strongly regular graph on 99 vertices) can be approached by encoding the defining properties of strongly regular graphs into SAT instances; experimental runs of SAT solvers on these instances are said to demonstrate that current solvers cannot resolve the problem in reasonable time, after which the authors discuss the underlying mathematical reasons for the observed limitations.

Significance. If the encoding were shown to be sound and complete and the experiments were reported with concrete runtimes, solver configurations, and verification on smaller instances, the result would usefully document the practical reach of SAT methods on an open combinatorial existence question, potentially motivating hybrid or specialized encodings for strongly regular graphs.

major comments (2)
  1. [Abstract] Abstract: the central claim that 'experimental tests' show SAT solvers' incapability rests on an encoding whose correctness is never verified. No clause list, no reduction argument, and no sanity check on known smaller SRGs (e.g., the 5-cycle or the Petersen graph) are supplied, so timeouts cannot be interpreted as evidence of inherent hardness rather than modeling error.
  2. [Experimental section (implied by abstract)] The manuscript supplies neither runtime data, solver names/versions, time limits, nor any comparison against known baselines or smaller parameter sets; without these, the empirical observation that the problem is 'intractable in reasonable time' cannot be evaluated or reproduced.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for identifying key gaps in verification and experimental reporting. These comments are fair and will lead to a substantially improved manuscript. We address each major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that 'experimental tests' show SAT solvers' incapability rests on an encoding whose correctness is never verified. No clause list, no reduction argument, and no sanity check on known smaller SRGs (e.g., the 5-cycle or the Petersen graph) are supplied, so timeouts cannot be interpreted as evidence of inherent hardness rather than modeling error.

    Authors: We agree that the current manuscript does not supply an explicit clause list, a formal reduction argument, or sanity checks on smaller instances. The encoding follows the standard translation of the three strongly regular graph axioms (regularity, constant lambda, constant mu) into propositional clauses, but this was only sketched. We will add a dedicated subsection that (i) gives the precise clause templates, (ii) proves that any satisfying assignment corresponds to a valid SRG and vice versa, and (iii) reports that the same encoding, when instantiated for the 5-cycle and the Petersen graph, is solved correctly and rapidly by the solver. This will allow timeouts on the 99-vertex case to be interpreted as evidence of hardness rather than encoding error. revision: yes

  2. Referee: [Experimental section (implied by abstract)] The manuscript supplies neither runtime data, solver names/versions, time limits, nor any comparison against known baselines or smaller parameter sets; without these, the empirical observation that the problem is 'intractable in reasonable time' cannot be evaluated or reproduced.

    Authors: We acknowledge that the manuscript currently lacks concrete experimental metadata. In the revised version we will insert a new experimental section that reports: solver name and version (MiniSat 2.2.0), hardware, wall-clock time limits (24 h), observed runtimes or timeouts for the Conway-99 instance, and successful runs on all smaller known SRG parameter sets (including the 5-cycle, Petersen graph, and several others up to 36 vertices). These baselines will make the claim of practical intractability reproducible and allow direct comparison. revision: yes

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: empirical encoding and runtime observation on external combinatorial problem

full rationale

The paper describes studying strongly regular graph properties, encoding them into SAT, and reporting experimental solver timeouts on the externally defined Conway-99 instance. No mathematical derivations, parameter fittings, predictions from fits, or self-citation chains appear in the provided text. The central claim is an empirical observation about solver behavior rather than a result derived from or equivalent to its own inputs by construction. Encoding correctness is an unverified modeling assumption but does not create circularity per the defined patterns.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

The work relies on the standard definition of strongly regular graphs and the Cook-Levin theorem that any NP problem reduces to SAT; no additional free parameters, invented entities, or non-standard axioms are introduced.

assumptions (2)
  • standard math A graph is strongly regular with parameters (n,k,λ,μ) if it is k-regular on n vertices and any two adjacent vertices share λ common neighbors while any two non-adjacent vertices share μ common neighbors.
    Invoked in the abstract when stating the Conway-99 parameters.
  • standard math Every NP decision problem can be reduced to a SAT instance in polynomial time (Cook-Levin theorem).
    Cited to justify the use of SAT solvers for the graph-existence question.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Approaching the Conway-99 problem using SAT solvers." pith.science (2026). https://pith.science/paper/2604.23037

@misc{pith2026260423037,
  author       = {Pith},
  title        = {Pith review of: Approaching the Conway-99 problem using SAT solvers},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2604.23037}},
  note         = {Machine review of arXiv:2604.23037}
}
read the original abstract

The Conway-99 problem questions the existence of a strongly regular graph with 99 vertices and specific parameters. A \textit{strongly} regular graph is a regular graph that exhibits two additional properties: vertices must share a fixed number of neighbours, depending on whether they are adjacent or not, given by two parameters. Despite the search space for this graph being finite, the computational power needed to traverse it is substantial. Therefore, better strategies are required in order to find this graph or prove its non-existence. SAT solvers, designed to solve instances of boolean satisfiability formulas, have been developed and optimised significantly due to the simplicity of SAT problems. Based on Cook-Levin's theorem, computer scientists have been focusing on developing efficient SAT solvers as many problems can be reduced to a SAT problem instance. Hence, we decided to approach the Conway-99 problem using SAT solvers. To do this, we study strongly regular graphs' properties and SAT solvers' capabilities. By encoding the problem of finding strongly regular graphs into SAT instances and running experimental tests, we shall see the incapability of SAT solvers facing this problem in a reasonable time. We will then explore the underlying mathematical reasons for these limitations.

Figures

Figures reproduced from arXiv: 2604.23037 by the authors.

Figure 1.1
Figure 1.1. A strongly regular graph, Paley(13) view at source ↗
Figure 3.1
Figure 3.1. Paley(9) with 𝐺𝐹 (9) vertices. This representation highlights the triangles. In a Galois field of order 𝑞, the size of the quadratic residues’ set 𝑄𝑅(𝑞) is 1 2 (𝑞 − 1). Every two elements of 𝐺𝐹 (𝑞) share 1 4 (𝑞 − 1) neighbours unless the two elements differ by one quadratic residue. In that case, they share 1 4 (𝑞 − 5) neighbours, which is one less because of the quadratic residue connecting them. Therefore, for eve… view at source ↗
Figure 3.2
Figure 3.2. Correcting errors by having larger distances between code words view at source ↗
Figures from the paper (10 more)
Figure 3.3
Figure 3.3. Figure 3.3: Paley(9) graph: A representation of the graph emphasising the quadrilateral
Figure 3.4
Figure 3.4. Figure 3.4: Paley(9) graph: A representation obtained from the Golay ternary code parity
Figure 3.5
Figure 3.5. Figure 3.5: Building a (99, 14, 1, 2) strongly regular graph based on the Paley(9) pattern. Vertex 5 must have two neighbours in 𝑁1,3. Name one vertex as (1, 3, 𝑥). This neighbour must form a triangle with 5. Let us consider the possibilities for the third vertex 𝑣3 of this tria…
Figure 3.6
Figure 3.6. Figure 3.6: Examining potential neighbouring sets for
Figure 4.1
Figure 4.1. Figure 4.1: Conway99 graph’s view from one vertex. Each non-neighbour can be repre
Figure 4.2
Figure 4.2. Figure 4.2: A shared neighbour 𝑘 for vertices {𝑖, 𝑗 }. The edge {𝑖, 𝑗 } may or may not be present. Proof. Similar to the Lemma 4.3.1, we will use 𝑛 𝜃+1  to ensure we have at most 𝜃 True vari￾ables. To proceed, we utilise 𝑛 𝑛−𝜃+1  more clauses to guarantee that only a maximum o…
Figure 4.3
Figure 4.3. Figure 4.3: Star graph 𝐾1,9, a graph with the same 𝜆 and 𝜇 parameters as the Petersen graph but not regular. Example 4.5.1. The graph depicted in 4.3 satisfies both 𝜆 = 0 and 𝜇 = 1 conditions. However, it is not a regular graph. Although this is a counterexample, its nature is s…
Figure 4.4
Figure 4.4. Figure 4.4: An adjacent pair of vertices {𝑢, 𝑣 } in a graph with 𝜆 and 𝜇 parameters. hence 𝜇 > 1, the degrees of adjacent vertices 𝑢 and 𝑣 are the same. Since the graph is connected, by continuing this, we infer all vertices must have the same degree, and this means the graph is…
Figure 5.1
Figure 5.1. Figure 5.1: The Petersen or 𝐾(5, 2) graph. Two vertices are adjacent if their respective sets share no element. every two edges that share a vertex are adjacent to 𝑛 − 2 other edges. If two edges do not share a vertex, name them 𝑢𝑣 and 𝑥𝑦, which means they are non-adjacent, they…
Figure 5.2
Figure 5.2. Figure 5.2: Possible 𝑁 (𝑣) induced subgraphs By employing the MAX-SAT method, we can find solutions that are almost strongly regular. For example, we force the SAT solver to return a 𝑘-regular graph while it tries to satisfy the maximum number of neighbouring conditions. SAT sol…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

  1. [1]

    Strongly regular graphs with non-trivial auto- morphisms.Discrete Mathematics, 311(2):132–144, 2011

    Majid Behbahani and Clement Lam. Strongly regular graphs with non-trivial auto- morphisms.Discrete Mathematics, 311(2):132–144, 2011

    work page 2011

  2. [2]

    A strongly regular graph derived from the perfect ternary golay code

    ER Berlekamp, JH Van Lint, and JJ Seidel. A strongly regular graph derived from the perfect ternary golay code. InA survey of combinatorial theory, pages 25–30. Elsevier, 1973

    work page 1973

  3. [3]

    CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020

    Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors,Proc. of SAT Competition 2020 – Solver and Benchmark Descriptions, vol- ume B-2020-1 ofDepartm...

    work page 2020

  4. [4]

    Preprocessing in sat solving.Hand- book of Satisfiability, 336:391–435, 2021

    Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in sat solving.Hand- book of Satisfiability, 336:391–435, 2021

    work page 2021

  5. [5]

    CUP Archive, 1971

    Norman Biggs.Finite groups of automorphisms: course given at the University of Southampton, October-December 1969, volume 6. CUP Archive, 1971

    work page 1969

  6. [6]

    Strongly regular graphs, partial geometries and partially balanced designs

    Raj Chandra Bose. Strongly regular graphs, partial geometries and partially balanced designs. 1963

    work page 1963

  7. [7]

    Andries E. Brouwer. Parameters of Strongly Regular Graphs. Brouwer’s website

    work page

  8. [8]

    Springer Science & Business Media, 2011

    Andries E Brouwer and Willem H Haemers.Spectra of graphs. Springer Science & Business Media, 2011

    work page 2011

Show all 29 references
  1. [9]

    Brouwer and H

    Andries E. Brouwer and H. Van Maldeghem.Strongly Regular Graphs. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2022

    2022

  2. [10]

    A (49, 16, 3, 6) strongly regular graph does not exist.European Journal of Combinatorics, 10(5):413–418, 1989

    Frans C Bussemaker, Willem H Haemers, R Matron, and Henny A Wilbrink. A (49, 16, 3, 6) strongly regular graph does not exist.European Journal of Combinatorics, 10(5):413–418, 1989

    1989

  3. [11]

    Strongly regular graphs.Topics in Algebraic Graph Theory, 102:203– 221, 2004

    Peter J Cameron. Strongly regular graphs.Topics in Algebraic Graph Theory, 102:203– 221, 2004

    2004

  4. [12]

    A theorem on permutations in a finite field.Proceedings of the American Mathematical Society, 11(3):456–459, 1960

    L Carlitz. A theorem on permutations in a finite field.Proceedings of the American Mathematical Society, 11(3):456–459, 1960

    1960

  5. [13]

    Association schemes of partially balanced block designs with param- eters v= 28, n1= 12, n2= 15 and p2 11= 4, sci.Record, 4:12–18, 1960

    Li-Chien Chang. Association schemes of partially balanced block designs with param- eters v= 28, n1= 12, n2= 15 and p2 11= 4, sci.Record, 4:12–18, 1960

    1960

  6. [14]

    Five $1,000 problems (update 2017).https://oeis.org/A248380/ a248380.pdf

    John Conway. Five $1,000 problems (update 2017).https://oeis.org/A248380/ a248380.pdf. 51

    2017

  7. [15]

    Stephen A. Cook. The complexity of theorem-proving procedures. InProceedings of the Third Annual ACM Symposium on Theory of Computing, pages 151–158, 1971

    1971

  8. [16]

    The strongly regular(45,12,3,3) graphs.the electronic journal of combinatorics, pages R32–R32, 2006

    Kris Coolsaet, Jan Degraer, and Edward Spence. The strongly regular(45,12,3,3) graphs.the electronic journal of combinatorics, pages R32–R32, 2006

    2006

  9. [17]

    Ternary codes from the strongly regular (45, 12, 3, 3) graphs and orbit matrices of 2-(45, 12, 3) designs.Discrete Mathematics, 312(20):3000–3010, 2012

    Dean Crnković, Bernardo Gabriel Rodrigues, Sanja Rukavina, and Loredana Simčić. Ternary codes from the strongly regular (45, 12, 3, 3) graphs and orbit matrices of 2-(45, 12, 3) designs.Discrete Mathematics, 312(20):3000–3010, 2012

    2012

  10. [18]

    Squaring a tournament: a proof of dean’s conjecture.Journal of Graph Theory, 23(1):43–48, 1996

    David C Fisher. Squaring a tournament: a proof of dean’s conjecture.Journal of Graph Theory, 23(1):43–48, 1996

    1996

  11. [19]

    Conflict-driven answer set solving: From theory to practice.Artif

    Martin Gebser, Benjamin Kaufmann, and Torsten Schaub. Conflict-driven answer set solving: From theory to practice.Artif. Intell., 187:52–89, 2012

    2012

  12. [20]

    Notes on digital coding.Proc

    Marcel JE Golay. Notes on digital coding.Proc. IEEE, 37:657, 1949

    1949

  13. [21]

    On strongly regular graph with parameters (65; 32; 15; 16).arXiv preprint arXiv:2102.05432, 2021

    Oleg Gritsenko. On strongly regular graph with parameters (65; 32; 15; 16).arXiv preprint arXiv:2102.05432, 2021

    2021

  14. [22]

    Cambridge University Press, 1993

    Derek Allan Holton and John Sheehan.The Petersen graph, volume 7. Cambridge University Press, 1993

    1993

  15. [23]

    Global symmetry is unneces- sary for fast quantum search.Physical Review Letters, 112(21):210502, 2014

    Jonatan Janmark, David A Meyer, and Thomas G Wong. Global symmetry is unneces- sary for fast quantum search.Physical Review Letters, 112(21):210502, 2014

    2014

  16. [24]

    Pearson Education, 1997

    Donald Ervin Knuth.The art of computer programming, volume 3. Pearson Education, 1997

    1997

  17. [25]

    Leonid A. Levin. Universal’nye pereborchiki i otsenki slozhnosti nekotorykh algorit- mov.Problemy Peredachi Informatsii, 9(3):115–116, 1973

    1973

  18. [26]

    Symmetry-breaking predicates for search problems

    Eugene Luks. Symmetry-breaking predicates for search problems. InPrinciples of Knowledge Representation and Reasoning: Proceedings of the Fifth International Confer- ence (KR’96), volume 5, page 148. Morgan Kaufmann Pub, 1996

    1996

  19. [27]

    Classification of regular two-graphs on 36 and 38 vertices.Australasian Journal of Combinatorics, 24:293–300, 2001

    Brendan D McKay and Edward Spence. Classification of regular two-graphs on 36 and 38 vertices.Australasian Journal of Combinatorics, 24:293–300, 2001

    2001

  20. [28]

    The strongly regular(40,12,2,4)graphs.the electronic journal of combinatorics, 7:R22–R22, 2000

    Edward Spence. The strongly regular(40,12,2,4)graphs.the electronic journal of combinatorics, 7:R22–R22, 2000

    2000

  21. [29]

    Wilbrink.On the (99,14,1,2) strongly regular graphs, pages 342–355

    H.A. Wilbrink.On the (99,14,1,2) strongly regular graphs, pages 342–355. EUT-Report. Technische Hogeschool Eindhoven, 1984. 52 Appendix A Runtime test experiments 𝑛 𝑘 𝜆 𝜇 time(s) Comment 5 2 0 1 0.0 9 4 1 2 0.001 10 3 0 1 0.001 10 6 3 4 0.002 13 6 2 3 0.004 15 6 1 3 0.007 15 8...

    1984

Pith tools

Reviewed May 8, 2026 · model on record in the stance chip above.