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

Conor Duggan, Zhengyu Li, Curtis Bright, Vijay Ganesh

AAAI 2024 pp. 23480-23481

doi:10.1609/AAAI.V38I21.30437 /aaai/2024/duggan2024aaai-sat/

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.

PDF AAAI Semantic Scholar

Cite

Text

Duggan et al. "A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)." AAAI Conference on Artificial Intelligence, 2024. doi:10.1609/AAAI.V38I21.30437

Markdown

[Duggan et al. "A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)." AAAI Conference on Artificial Intelligence, 2024.](https://mlanthology.org/aaai/2024/duggan2024aaai-sat/) doi:10.1609/AAAI.V38I21.30437

BibTeX

@inproceedings{duggan2024aaai-sat,
  title     = {{A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)}},
  author    = {Duggan, Conor and Li, Zhengyu and Bright, Curtis and Ganesh, Vijay},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2024},
  pages     = {23480-23481},
  doi       = {10.1609/AAAI.V38I21.30437},
  url       = {https://mlanthology.org/aaai/2024/duggan2024aaai-sat/}
}