Marijn Heule

Marijn Heule is an Associate Professor in the Computer Science Department at Carnegie Mellon University. He received his PhD from Delft University of Technology in the Netherlands. His academic career has been focused on advancing the theory and practice of satisfiability (SAT) solving and its applications.

Dr. Heule's research primarily centers on solving hard combinatorial problems in formal verification, number theory, and extremal combinatorics. His work has made significant contributions to both theoretical foundations and practical implementations of SAT solvers. He has developed award-winning SAT solvers, and his preprocessing techniques are incorporated into state-of-the-art SAT solvers used worldwide. His current research focuses on two major challenges: exploiting high-performance computing for SAT solving and validating results from SAT solvers and related tools.

Dr. Heule pioneered the "cube-and-conquer" paradigm, a novel parallel SAT solving approach that enables linear time speedups on many hard problems. His first publication on this topic won the best paper award at HVC 2011. He also designed a new proof format with a corresponding fast proof checker for SAT and QBF solvers. This proof logging format has been mandatory for SAT Competitions since 2013, significantly increasing confidence in tool correctness. His work on the Boolean Pythagorean Triples problem, which produced a 200 TB proof that was validated, demonstrated that proof logging and verification is feasible even for the most complex problems.

Dr. Heule is one of the editors of the 900+ page "Handbook of Satisfiability," which has become a standard reference in the SAT community. He serves as an Associate Editor of the Journal on Satisfiability, Boolean Modeling and Computation and previously co-chaired the SAT 2015 conference in Austin.

• Best paper award at HVC 2011 for cube-and-conquer publication
• Multiple best paper awards/nominations at major conferences including IJCAR, SAT, TACAS
• Work featured in New York Times, Quanta Magazine, Nature, and other major media outlets

Dr. Heule has advised several PhD students including Emre Yolcu, Joseph Reeves, Bernardo Subercaseaux, Cayden Codel, James Gallicchio, and Amar Shah. He has developed important software tools including DRAT-trim (a proof checking utility), QRAT-trim, and implementations of the cube-and-conquer paradigm that have become standard in the SAT solving community.