Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Everything’s Bigger in Texas: The Largest Math Proof Ever
Speaker:Marijn J.H. Heule
coming from:University of Texas, Austin
Speakers Bio:Dr. Marijn J.H. Heule is a Research Scientist at the University of Texas at Austin. He received his PhD at Delft University of Technology in the Netherlands in 2008. His research focuses on solving hard combinatorial problems in areas such as formal verification, number theory, and combinatorics. Most of his contributions are related to theory and practice of satisfiability (SAT) solving. He has developed award-winning SAT solvers (see, and his preprocessing techniques are used in most state-of-the-art SAT solvers.

More recently, Dr. Heule has concentrated on two major challenges for SAT solving: 1) exploiting the potential of high-performance computing; and 2) validating the results of SAT solvers and related tools. Dr. Heule developed a new parallel SAT solving paradigm, called cube-and-conquer, which enables linear time speedups on many hard problems. His first publication on cube-and-conquer won the best paper award at HVC 2011. Treengeling, a solver by Armin Biere based on that paradigm, solved most benchmarks during SAT Competition 2013.

The increasing complexity of SAT solvers and related tools makes it more likely that these tools contain bugs. Dr. Heule has designed a new proof format and implemented a fast, corresponding proof checker for SAT and QBF solvers. Proof-logging in his format has been mandatory for the SAT Competitions since 2013, thereby increasing the confidence that tools produce correct results.

Dr. Heule has published over 40 technical peer-reviewed papers. Dr. Heule is one of the editors of the Handbook of Satisfiability. This 900+ page handbook has become a standard for the SAT community, and it is a tremendous resource for future scientists. Dr. Heule is an Associate Editor of the Journal on Satisfiability, Boolean Modeling and Computation and was a co-chair of the International Conference on Theory and Applications of Satisfiability Testing in 2015 in Austin.
Event Type:Talk
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 27 July 2016
Duration:60 Minutes
Building:E1 4
The Boolean Pythagorean Triples problem 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, for example. 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. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the proof for checking. These techniques show great promise for attacking a variety of challenging problems arising in combinatorics and computer science.
Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
Jennifer Müller/MPI-INF, 07/13/2016 05:42 PM
Last modified:
Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Jennifer Müller, 07/18/2016 09:44 AM
  • Jennifer Müller, 07/13/2016 05:47 PM -- Created document.