Boolean Pythagorean triples problem: Difference between revisions

Revision as of 07:28, 26 May 2023

Revision as of 14:45, 24 August 2024

Line 8:

==Solution==

Marijn Heule, Oliver Kullmann, and Victor W. Marek demonstrated that it is possible to partition the set ({1, \ldots, 7824}) into two subsets such that neither subset contains a Pythagorean triple. However, such a partition is not possible for the set ({1, \ldots, 7825}). This result was achieved by analyzing a vast number of possible colorings, which initially amounted to about (2^{7825}) combinations.The researchers reduced this to around a trillion cases, which were then tested using a SAT solver. The computational process required approximately 4 CPU-years over two days on the Stampede supercomputer at the Texas Advanced Computing Center. The resulting proof, initially 200 terabytes in size, was compressed to 68 gigabytes.The findings were published in the SAT 2016 conference paper "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer," which received the best paper award. The image included in the paper shows a possible coloring scheme for ({1, \ldots, 7824}) that avoids monochromatic Pythagorean triples.

[[Marijn Heule]], Oliver Kullmann and Victor W. Marek showed that such a coloring is only possible up to the number 7824. 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 {{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, expressed as [[Boolean satisfiability]] problems, were examined using a [[SAT 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|last1=Heule|first1=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,...,7824} 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]]

==Prize==