Boolean Pythagorean triples problem: Difference between revisions

Revision as of 20:35, 22 July 2016

Revision as of 05:56, 23 July 2016

Line 8:

There are 2⁷⁸²⁵ colorings for the numbers up to 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 two days of computer execution time 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 on arXiv on 3 May 2016,<ref name="arXiv">{{Cite arXiv|last=Heule|first=Marijn J. H.|last2=Kullmann|first2=Oliver|last3=Marek|first3=Victor W.|date=2016-05-03|title=Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer |arxiv=1605.00723 }}</ref>, and has been accepted for the SAT 2016 conference, 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.