avatar

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

Short Bio

I am a Research Scientist 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.

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