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

TL;DR

This paper solves the longstanding boolean Pythagorean Triples problem by employing a hybrid SAT solving approach, producing a massive formal proof that confirms the impossibility of partitioning natural numbers without containing a Pythagorean triple.

Contribution

It introduces a novel application of the Cube-and-Conquer SAT solving paradigm to a major open problem in Ramsey Theory, providing a formal, verifiable proof of the impossibility.

Findings

The problem was solved using a cluster with 800 cores in about 2 days.

Produced a 200-terabyte DRAT proof and a 68-gigabyte compressed certificate.

Confirmed the impossibility of partitioning natural numbers without Pythagorean triples.

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^2 + b^2 = c^2$ ? 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.