Schur Number Five

AAAI 2018 pp. 6598-6606

doi:10.1609/AAAI.V32I1.12209 /aaai/2018/heule2018aaai-schur/

Abstract

We present the solution of a century-old problem known as Schur Number Five: What is the largest (natural) number n such that there exists a five-coloring of the positive numbers up to n without a monochromatic solution of the equation a + b = c? We obtained the solution, n = 160, by encoding the problem into propositional logic and applying massively parallel satisfiability solving techniques on the resulting formula. We also constructed and validated a proof of the solution to increase trust in the correctness of the multi-CPU-year computations. The proof is two petabytes in size and was certified using a formally verified proof checker, demonstrating that any result by satisfiability solvers---no matter how large---can now be validated using highly trustworthy systems.

PDF AAAI Semantic Scholar

Cite

Text

Heule. "Schur Number Five." AAAI Conference on Artificial Intelligence, 2018. doi:10.1609/AAAI.V32I1.12209

Markdown

[Heule. "Schur Number Five." AAAI Conference on Artificial Intelligence, 2018.](https://mlanthology.org/aaai/2018/heule2018aaai-schur/) doi:10.1609/AAAI.V32I1.12209

BibTeX

@inproceedings{heule2018aaai-schur,
  title     = {{Schur Number Five}},
  author    = {Heule, Marijn J. H.},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2018},
  pages     = {6598-6606},
  doi       = {10.1609/AAAI.V32I1.12209},
  url       = {https://mlanthology.org/aaai/2018/heule2018aaai-schur/}
}