Boolean Pythagorean triples problem

The Boolean Pythagorean triples problem is a problem relating to Pythagorean triples which was solved using a computer-assisted proof in May 2016.[1]

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 are all the same color. For example, in the Pythagorean triple 3, 4 and 5 (), if 3 and 4 are colored red, then 5 must be colored blue.

Marijn Heule, Oliver Kullmann and Victor Marek investigated the problem, 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

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}.[2]

There are 27825 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 about 4 years of CPU time over 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 on arXiv on 3 May 2016,[2] and has been accepted for the SAT 2016 conference, where it won the best paper award.[3]

In the 1980s Ronald Graham offered a $100 prize for the solution of the problem, which has now been awarded to Marijn Heule.[1]

References

  1. 1 2 Lamb, Evelyn (26 May 2016). "Two-hundred-terabyte maths proof is largest ever". Nature. 534: 17–18. PMID 27251254. doi:10.1038/nature.2016.19990.
  2. 1 2 Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016-05-03). "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer". arXiv:1605.00723 Freely accessible.
  3. ↑ SAT 2016
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.