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 http://satcompetition.org/), 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.

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

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.

Jennifer Müller

2900

--email hidden

passcode not visible

logged in users only