A SAT + Computer Algebra System Verification of the Ramsey Problems R(3,8) - R(3,9) - Master of Mathematics Thesis

Sep 15, 2026

Uploaded by Stanford

The Ramsey problem R(p,q) seeks the smallest n such that any graph on n vertices contains either a p-clique or an independent set of size q. This thesis provides the first certifiable proof that R(3,8)=28 by combining a Boolean satisfiability (SAT) solver with a computer algebra system (CAS). It also proves and verifies R(3,9)=36 using graph structure theory and a parallelisable SAT+CAS toolchain, extending prior non-verifiable computational results.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages48

Reading Time2 h 1 min

AccessFree to download

1 Introduction

2 Boolean Algebra, SAT Solvers and CASs

3 Cube and Conquer

4 Methodology

Constraints

Symmetry breaking constraints

Edge constraints

Degree constraints

Triangle constraints

Maximal clique free constraints

6 Comparison of R(3,8) Methods

7 The search for R(3,9)

8 PySMS

9 Ablation Study

10 Related work

11 Formal Verification and Result

12 Conclusion

A SAT + Computer Algebra System Verification of the Ramsey Problems R(3,8) and R(3,9) by Conor Duggan A thesis presented to the University of Waterloo in fulfillment of the research paper requirement for the degree of Master of Mathematics in Computational Mathematics Waterloo, Ontario, Canada, 2024 © Conor Duggan 2024 Author’s Declaration I hereby declare that I am the sole author of this thesis. This is a true copy of the thesis, including any required final revisions, as accepted by my examiners. I understand that my thesis may be made electronically available to the public. Abstract The Ramsey problem R(p, q) asks for the smallest n such that every graph on n vertices must contain either a p-clique or an independent set of size q. We provide the first certifiable proof that R(3 , 8) = 28, automatically generated by a combination of Boolean satisfiability (SAT) solverand a computer algebra system (CAS) . While the R(3 , 8) problem was first computationally solved by McKay and Min in 1992, it was not a verifiable proof. This SAT+CAS combination is significantly faster than a SAT-only approach. We prove and verify R(3 , 9) = 36 combining theory on the structure of graphs and a parallelisable SAT+CAS toolchain. The theory relating to R(3 , 9) was developed by Graver and Yackel in 1968 and expanded upon and finally proved by Grinstead and Roberts in 1982, again not a verifiable proof. The SAT+CAS method that we use for our proof is very general and can be applied to a wide variety of combinatorial problems. Acknowledgements The progression of mathematics and science is not a solo endeavour. My research thesis was only possible by cumulative contributions and valuable discussions. Foremost, I thank my supervisors Professor Vijay Ganesh and Professor Curtis Bright. Their direction and deep expertise over the course of almost two years was invaluable. Each maintain the highest standards in their work and I hope to have inherited some of their dedication to precision. I owe a massive debt of gratitude to Brian Li. His support, mathematical and in other areas, was invaluable. Discussions with him are always interesting and fruitful. On a similar note, I am grateful to the contributions of Daksh Segal, Piyush Jha and Jonathon Chung. Finally, to everyone who stimulated my interest in learning and in mathematics, family, friends, teachers or professors, I would not have started this journey without you. Dedication This is dedicated to my parents and to friends. Sometimes a walk with someone makes all the difference. Table of Contents Author’s Declaration ii Abstract iii Acknowledgements iv Dedication v List of Figures viii List of Tables ix 1 Introduction 1 2 Boolean Algebra, SAT Solvers and CASs 4 3 Cube and Conquer 6 4 Methodology 8 5 Constraints 11 Symmetry breaking constraints ........................... 12 Edge constraints ................................... 12 Degree constraints ................................. 14 Triangle constraints ................................. 14 Maximal clique free constraints ........................... 14 6 Comparison of R(3,8) Methods 16 7 The search for R(3,9) 18 8 PySMS 25 9 Ablation Study 27 10 Related work 29 11 Formal Verification and Result 32 12 Conclusion 35 References 36 List of Figures 1.1 A red/blue edge coloring on 8 vertices without a blue 3-clique or red 4-clique, showing R(3 , 4) > 8................................. 2 4.1 A flowchart of the orderly generation algorithm implemented as part of MathCheck’s SAT+CAS architecture........................... 9 4.2 Flowchart of pipeline without parallelisation from input parameters to verification. 10 7.1 Graph with a preferred vertex v, H1 (v) and H2 (v) . Note for p = 3, H1 (v) is an independent set.................................... 19 11.1 Solve time for the 10.1k cubes solved by SAT+CAS. Unsolved cubes were further cubed. Cube

FAQs

What does the Ramsey problem R(p,q) ask for?

It asks for the smallest n such that every graph on n vertices contains either a p-clique or an independent set of size q.

How is R(3,8)=28 proven in this thesis?

It is proven using a certifiable SAT+CAS combination, generating a proof automatically via SAT solving supported by computer algebra system reasoning.

How does the approach for R(3,9)=36 differ from the R(3,8) case?

R(3,9)=36 is established by combining structural graph theory with a parallelisable SAT+CAS toolchain, addressing prior results that were computationally solved but not verifiably proven.

Sep 15, 2026

Uploaded by Stanford