AAAI 2024technical2 citations
A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)
Conor Duggan, Zhengyu Li, Curtis Bright, Vijay Ganesh
Abstract
The Ramsey problem R(3,8) asks for the smallest n such that every red/blue coloring of the complete graph on n vertices must contain either a blue triangle or a red 8-clique. We provide the first certifiable proof that R(3,8) = 28, automatically generated by a combination of Boolean satisfiability (SAT) solver and a computer algebra system (CAS). This SAT+CAS combination is significantly faster than a SAT-only approach. While the R(3,8) problem was first computationally solved by McKay and Min in 1992, it was 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.
BibTeX
@article{Duggan_Li_Bright_Ganesh_2024, title={A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)}, volume={38}, url={https://ojs.aaai.org/index.php/AAAI/article/view/30437}, DOI={10.1609/aaai.v38i21.30437}, abstractNote={The Ramsey problem R(3,8) asks for the smallest n such that every red/blue coloring of the complete graph on n vertices must contain either a blue triangle or a red 8-clique. We provide the first certifiable proof that R(3,8) = 28, automatically generated by a combination of Boolean satisfiability (SAT) solver and a computer algebra system (CAS). This SAT+CAS combination is significantly faster than a SAT-only approach. While the R(3,8) problem was first computationally solved by McKay and Min in 1992, it was 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.}, number={21}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Duggan, Conor and Li, Zhengyu and Bright, Curtis and Ganesh, Vijay}, year={2024}, month={Mar.}, pages={23480-23481} }