Verified Certificates via SAT and Computer Algebra Systems for the Ramsey $R(3, 8)$ and $R(3, 9)$ Problems
Zhengyu Li, Conor Duggan, Curtis Bright, Vijay Ganesh
TL;DR
The paper addresses the challenge of certifying Ramsey-number computations by integrating SAT solvers with computer algebra systems via the Math-Check framework to produce verifiable certificates. It demonstrates substantial performance gains over SAT-only methods and delivers independently checkable certificates for $R(3,8)=28$ and $R(3,9)=36$ (with symmetry for $R(8,3)$ and $R(9,3)$) using both sequential and parallel cube-and-conquer strategies. By combining theory with SAT+CAS techniques and rigorous verification (DRAT-trim with CAS-witnesses), the approach provides trustworthy results for hard Ramsey instances that were previously uncertified. The work highlights the practical and methodological significance of certifiable, scalable computation in Ramsey theory and outlines directions for fully formalizing encodings and proofs in proof assistants.
Abstract
The Ramsey problem $R(3, k)$ seeks to determine the smallest value of $n$ such that any red/blue edge coloring of the complete graph on $n$ vertices must either contain a blue triangle (3-clique) or a red clique of size $k$. Despite its significance, many previous computational results for the Ramsey $R(3, k)$ problem such as $R(3, 8)$ and $R(3, 9)$ lack formal verification. To address this issue, we use the software MathCheck to generate certificates for Ramsey problems $R(3, 8)$ and $R(3, 9)$ (and symmetrically $R(8, 3)$ and $R(9, 3)$) by integrating a Boolean satisfiability (SAT) solver with a computer algebra system (CAS). Our SAT+CAS approach significantly outperforms traditional SAT-only methods, demonstrating an improvement of several orders of magnitude in runtime. For instance, our SAT+CAS approach solves $R(3, 8)$ (resp., $R(8, 3)$) sequentially in 59 hours (resp., in 11 hours), while a SAT-only approach using state-of-the-art CaDiCaL solver times out after 7 days. Additionally, in order to be able to scale to harder Ramsey problems $R(3, 9)$ and $R(9, 3)$ we further optimized our SAT+CAS tool using a parallelized cube-and-conquer approach. Our results provide the first independently verifiable certificates for these Ramsey numbers, ensuring both correctness and completeness of the exhaustive search process of our SAT+CAS tool.