Approaching the Conway-99 problem using SAT solvers
This work highlights the limitations of SAT solvers for a specific combinatorial existence problem, but the result is negative and incremental.
The authors attempted to solve the Conway-99 problem (existence of a strongly regular graph with 99 vertices) using SAT solvers, but found that SAT solvers are incapable of solving it in reasonable time due to mathematical limitations.
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.