Speaker: Marijn J.H. Heule

Title: Everything's Bigger in Texas: The Largest Math Proof Ever

Abstract:
Many search problems, from artificial intelligence to combinatorics,
explore large search spaces to determine the presence or absence of a
certain object.  These problems are hard due to combinatorial
explosion, and have traditionally been called infeasible.  The
brute-force method, which at least implicitly explores all
possibilities, is a general approach to search systematically through
such spaces. Brute force has long been regarded as suitable only for
simple problems.  This has changed in the last two decades, due to the
progress in satisfiability (SAT) solving, which renders brute force
into a powerful approach to deal with many problems easily and
automatically.

We illustrate the strength of SAT via the Boolean Pythagorean Triples
problem, which has been a long-standing open problem in Ramsey Theory:
Can the set N = {1, 2, 3, ...} of natural numbers be partitioned into
two parts, such that neither part contains a triple (a, b, c) with a^2
+ b^2 = c^2 ?  A prize for the solution was offered by Ron Graham
decades ago.  We show that such a partition is possible for the set of
integers in [1,7824], but that it is not possible for the set of
integers in [1,M] for any M > 7824.  Of course, it is completely
infeasible to attempt proving this directly by examining all 2^M
possible partitions of [1,M] when M = 7825.

We solve this problem by using the cube-and-conquer paradigm, a
parallel satisfiability solving method that achieves linear time
speedups on many hard problems.  An important role is played by
dedicated look-ahead heuristics, which allowed us to solve the problem
on a cluster with 800 cores in about two days.  Due to the general
interest in this mathematical problem, our result requires a formal
proof.  Exploiting recent progress in unsatisfiability proof checking,
we produced and verified a clausal proof of the smallest
counterexample, which is almost 200 terabytes in size.  These
techniques show great promise for attacking a variety of challenging
problems arising in combinatorics and computer science.