Boolean Pythagorean triples problem: Difference between revisions

Revision as of 07:44, 28 February 2020

Revision as of 07:48, 28 February 2020

Line 8:

There are {{nowrap|2⁷⁸²⁵ ≈ 3.63×10²³⁵⁵}} colorings 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 onin [[arXiv]]the on 3 MaySAT 2016 conference,<ref name="arXiv">{{Cite journalconference|last=Heule|first=Marijn J. H.|last2=Kullmann|first2=Oliver|last3=Marek|first3=Victor W.|dateyear=2016-05-03|titlecontribution=Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer |arxiv=1605.00723|doi=10.1007/978-3-319-40970-2_15|journalseries=Lecture Notes in Computer Science|volume=9710|pages=228–245}}</ref>|title=Theory and hasApplications beenof acceptedSatisfiability forTesting the– SAT 2016: conference19th 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>

In the 1980s [[Ronald Graham]] offered a $100 prize for the solution of the problem, which has now been awarded to Marijn Heule.<ref name="nature"/>