Content deleted Content added
Citation bot (talk | contribs) Add: s2cid, issue, authors 1-1. Removed proxy/dead URL that duplicated identifier. Removed parameters. Some additions/deletions were parameter name changes. | Use this bot. Report bugs. | Suggested by SemperIocundus | #UCB_webform 1156/2500 |
→Solution: those, expressed as Boolean satisfiability problems, were examined using a SAT solver... |
||
Line 12:
}}
There are {{nowrap|2<sup>7825</sup> ≈ 3.63×10<sup>2355</sup>}} 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 [[
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.
| |||