Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer

2016/05/03 by Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek · 5 voices · 8 citations
#cs.DM #cs.LO

paper · pdf · doi:10.1007/978-3-319-40970-2_15

Abstract

The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = \1, 2, ...\ of natural numbers be divided into two parts, such that no part contains a triple (a,b,c) with a² + b² = c² ? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.

Cited by

• From the Finite to the Infinite: Sharper Asymptotic Bounds on Norin's Conjecture via SAT
• Learning Interestingness in Automated Mathematical Theory Formation
• Truth Without Comprehension: A BlueSky Agenda for Steering the Fourth Mathematical Crisis
• Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions
• Queen Domination by SAT Solving
• Recurrence for pretentious systems along generalized Pythagorean triples
• Solver-Aided Expansion of Loops to Avoid Generate-and-Test
• List of unsolved problems in mathematics [wikipedia]

Discussions

• Die Studie zeigt die Fähigkeiten von SAT-Solvern. Das boolesche pythagoreische Tripelproblem aus der Ramsey-Theorie galt lange als ungelöst. Die Autoren konnten es schließlich lösen. Der 200 Terabyte [bsky, 6 points, 0 comments]
• [pdf] Solving and Verifying the Boolean Pythagorean Triples Problem [hn, 2 points, 0 comments]
• Solving and Verifying the Boolean Pythagorean Triples Problem [hn, 2 points, 0 comments]
• Solving and Verifying the Bool Pythagorean Triples Problem via Cube-And-Conquer [hn, 2 points, 0 comments]
• This is a notorious paper discussing a huge automatically generated proof of a conjecture. Was it research? arxiv.org/abs/1605.00723 [bsky, 1 points, 1 comments]

Related

• Computing Pythagorean Triples
• Construction of primitive Pythagorean triples and Pythagorean triples with a common multiplier using gnomons
• abc triples
• A Direct Method To Generate Pythagorean Triples And Its Generalization To Pythagorean Quadruples And n-tuples
• Verified Certificates via SAT and Computer Algebra Systems for the Ramsey R(3, 8) and R(3, 9) Problems