A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)

Authors

  • Conor Duggan University of Waterloo
  • Zhengyu Li Georgia Institute of Technology
  • Curtis Bright University of Windsor
  • Vijay Ganesh Georgia Institute of Technology

DOI:

https://doi.org/10.1609/aaai.v38i21.30437

Keywords:

Automated Reasoning, Logic, Constraint Satisfaction, Machine Learning

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.

Published

2024-03-24

How to Cite

Duggan, C., Li, Z., Bright, C., & Ganesh, V. (2024). A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract). Proceedings of the AAAI Conference on Artificial Intelligence, 38(21), 23480-23481. https://doi.org/10.1609/aaai.v38i21.30437