Approaching the Conway-99 problem using SAT solvers

TL;DR

This paper investigates the feasibility of using SAT solvers to find or prove the non-existence of a specific strongly regular graph with 99 vertices, highlighting current limitations and underlying mathematical challenges.

Contribution

It encodes the Conway-99 problem into SAT instances and evaluates the performance and limitations of SAT solvers on this problem.

Findings

SAT solvers struggle to solve the Conway-99 problem within reasonable time

The study reveals fundamental mathematical reasons behind SAT solvers' limitations

Experimental results show the complexity of encoding strongly regular graphs into SAT

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.