avatar

Marijn J.H. Heule
Research Scientist at The University of Texas at Austin

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

Citations


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.

Nature
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
Azimuth
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
Phys.org
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:

EenVandaag
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.
Volkskrant
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.

Publications

Talks

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

Software

DRAT-trim
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
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.
Cube-and-Conquer
The cube-and-conquer parallel SAT solving paradigm combines look-ahead techniques for splitting with conflict-driven clause-learning techniques.
March
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
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.