Boolean Pythagorean triples problem: Difference between revisions

Revision as of 21:50, 21 March 2021

Revision as of 20:22, 25 March 2021

Line 14:

There are {{nowrap|2⁷⁸²⁵ ≈ 3.63×10²³⁵⁵}} possible coloring combinations for the numbers up to [[7825 (number)|7825]]. These possible colorings were logically and algorithmically narrowed down to around a trillion (still highly complex) cases, and those were examined using a [[Boolean satisfiability]] solver. Creating the proof took about 4 CPU-years of computation over a period of two days on the Stampede supercomputer at the [[Texas Advanced Computing Center]] and generated a 200 terabyte propositional proof, which was compressed to 68 gigabytes.

The paper describing the proof was published in the SAT 2016 conference,<ref name="arXiv">{{Cite conference|last=Heule|first=Marijn J. H.|last2=Kullmann|first2=Oliver|last3=Marek|first3=Victor W.|author3-link=Victor W. Marek|year=2016|contribution=Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer |arxiv=1605.00723|doi=10.1007/978-3-319-40970-2_15|series=Lecture Notes in Computer Science|volume=9710|pages=228–245|title=Theory and Applications of Satisfiability Testing – SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings|editor1-first=Nadia|editor1-last=Creignou|editor2-first=Daniel|editor2-last=Le Berre}}</ref> where it won the best paper award.<ref>[http://sat2016.labri.fr/ SAT 2016]</ref> The figure below shows a possible family of colorings for the set {1,...,7,8247824} with no monochromatic Pythagorean triple, and the white squares can be colored either red or blue while still satisfying this condition.

[[File:Ptn-7824-zoom-2.png|alt=|center|400x400px]]