Marijn Heule

ACL2 Seminar, April 5, 2016

Solving and Verifying the Boolean Pythagorean Triples Problem via
Cube-and-Conquer

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.