Verified Certificates via SAT and Computer Algebra Systems for the Ramsey $R(3, 8)$ and $R(3, 9)$ Problems
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908578562965504 |
|---|---|
| author | Li, Zhengyu Duggan, Conor Bright, Curtis Ganesh, Vijay |
| author_facet | Li, Zhengyu Duggan, Conor Bright, Curtis Ganesh, Vijay |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_06055 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verified Certificates via SAT and Computer Algebra Systems for the Ramsey $R(3, 8)$ and $R(3, 9)$ Problems Li, Zhengyu Duggan, Conor Bright, Curtis Ganesh, Vijay Logic in Computer Science Discrete Mathematics Symbolic Computation Combinatorics 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. |
| title | Verified Certificates via SAT and Computer Algebra Systems for the Ramsey $R(3, 8)$ and $R(3, 9)$ Problems |
| topic | Logic in Computer Science Discrete Mathematics Symbolic Computation Combinatorics |
| url | https://arxiv.org/abs/2502.06055 |