Boolean Pythagorean triples problem: Difference between revisions

Revision as of 16:18, 6 June 2016

Revision as of 16:19, 18 July 2016

Line 3:

This problem is from [[Ramsey theory]] and asks if it is possible to color each of the positive integers either red or blue so that no Pythagorean triple of integers ''a'', ''b'', ''c'', satisfying <math>a^2+b^2=c^2</math> are all the same color. For example, a coloring with ''a'' and ''b'' red and ''c'' blue is an admissible coloring, but all three blue would not be.

TheMarijn proofHeule, shows Oliver Kullmann and Victor Marek investigated the probelm and showed that such a coloring is impossible. Up to the number 7824 it is possible to color the numbers such that all Pythagorean triples are admissible, but the proof shows that no such coloring can be extended to also color the number 7825. The actual statement of the theorem proved is

{{math theorem| The set {1, . . . , 7824} can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for {1, . . . , 7825}.<ref name="arXiv"/>}}

There are 2⁷⁸²⁵ colorings for the numbers up to 7825. These possible colorings were logically narrowed down to just under a trillion 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 200 terabytes of data which were compressed to 68 gigabytes.

In the 1980s [[Ronald Graham]] offered a $100 prize for the solution of the problem, which has now been awarded to Marijn Heule. 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 an won the best paper award in that conference<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.

== References ==

<references />