Verified Certificates via SAT and Computer Algebra Systems for the Ramsey $R(3, 8)$ and $R(3, 9)$ Problems

TL;DR

This paper introduces a SAT and computer algebra system-based method to generate verifiable certificates for the Ramsey numbers R(3,8) and R(3,9), significantly improving runtime and ensuring correctness of the results.

Contribution

The authors develop a SAT+CAS approach that outperforms traditional methods and provides the first independently verifiable certificates for R(3,8) and R(3,9).

Findings

SAT+CAS approach solves R(3,8) in 59 hours

Parallelized cube-and-conquer scales to R(3,9)

Provides the first verifiable certificates for these Ramsey numbers

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.