Marijn J.H. Heule

I moved to Carnegie Mellon University.

This page is no longer maintained. Visit the link above for the new webpage.

Short Bio

I am a Research Assistant Professor at the University of Texas at Austin and received my PhD at Delft University of Technology in the Netherlands in 2008. My research focuses on solving hard-combinatorial problems in areas such as formal verification, number theory, and extreme combinatorics. Most of my contributions are related to theory and practice of satisfiability (SAT) solving. I have developed award-winning SAT solvers, and my preprocessing techniques are used in state-of-the-art SAT solvers.

My current research focusses 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. I have been developing a novel parallel SAT solving paradigm, called cube-and-conquer, which enables linear time speedups on many hard problems. The first publication on cube-and-conquer won the best paper award at HVC 2011.

The increasing complexity of SAT solvers and related tools makes it more likely that these tools contain bugs. I designed a new proof format and implemented a fast, corresponding proof checker for SAT and QBF solvers. Proof-logging in this format has been mandatory for the SAT Competitions since 2013, thereby increasing the confidence that tools produce correct results. By constructing and validating a proof for the Boolean Pythagorean Triples problem (200 TB in size), I showed that proof logging and verification is even possible for the hardest problems.

I am 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. I am an Associate Editor of the Journal on Satisfiability, Boolean Modeling and Computation and was a co-chair of the SAT 2015 conference in Austin. My resume offers more details.

Contact Information

Gates Dell Complex, room 7.714
Department of Computer Science
2317 Speedway, M/S D9500
The University of Texas
Austin, TX 78712-0233

email (work): marijn@cs.utexas.edu
email (personal): marijn@heule.nl
homepage: http://www.cs.utexas.edu/~marijn


source: Google Scholar Citations

In the Media

Selected articles on the ``largest math proof ever", check out Everything's Bigger in Texas for a complete list.

Volume 543: 17-18
Maths proof smashes size record [pdf, url]
Reddit offers a discussion on this article with 250+ comments
I Programmer
May 10, 2016
A Mathematical Proof Takes 200 Terabytes To State
This is the first article on the Pythagorean Triples proof
May 27/28, 2016
The world's most long-winded proof and Very Long Proofs
The first article has 75+ comments including messages by Timothy Gowers
Der Spiegel
May 30, 2016
Zahlenrätsel: Der längste Mathe-Beweis der Welt
The article includes 60+ comments
May 30, 2016
Computer generated math proof is largest ever at 200 terabytes
Slashdot offers a discussion on this article with 140+ comments

Appearences in Dutch media:

June 8, 2016
Nederlandse wetenschapper lost wiskundig probleem op
Dutch news show item on the Pythagorean triples proof including a Skype interview with Ronald Graham.
June 6, 2016
Bewijs dat nét op 200 laptops past
Interview in a Dutch newspaper on the ``largest math proof ever".
NRC Handelsblad
September 5, 2015
Op vleugels van vervulbaarheid
Article in a Dutch newspaper on computer-generated proofs for math problems.



Selected invited talks and tutorials. Slides of conference talks can be found under publications.


DRAT-trim is a satisfiability proof checking and trimming utility designed to validate proofs for all known satisfiability solving and preprocessing techniques. DRAT-trim can also emit trimmed formulas, optimized proofs, and TraceCheck+ dependency graphs.
QRAT-trim is a proof checking utility for quantified Boolean formulas and is based on the QRAT proof system. The tool also supports the conversion of QRAT proofs into Skolem functions.
The cube-and-conquer parallel SAT solving paradigm combines look-ahead techniques for splitting with conflict-driven clause-learning techniques.
The March SAT solver (latest version march_br) is based on the lookahead architecture. It is the latest version in the march family of solvers, which won many medals at various SAT competitions. See the SAT 2004 paper for details.
DRUP-trim is a proof checking utility based on the reverse unit propagation redundancy property. The tool was used to validate the results of SAT Competition 2013.