معرفی
Marijn J.H. Heule is an Associate Professor at the School of Computer Science, Carnegie Mellon University. He received his PhD from Delft University of Technology in the Netherlands. His research focuses on solving hard combinatorial problems through Satisfiability (SAT) solving, with applications in formal verification, number theory, and extremal combinatorics.
- Education:
- PhD in Computer Science, Delft University of Technology, Netherlands
Heule's work addresses fundamental challenges in SAT solving, including:
- Exploiting high-performance computing via the cube-and-conquer paradigm
- Validating results from SAT solvers using novel proof formats
His research has produced 15+ recent publications (2025-2021) on topics like automated reasoning, formal verification, and combinatorial proofs. Notable achievements include:
- Best Paper Award at HVC 2011 (Cube-and-Conquer)
- 200 TB proof for the Boolean Pythagorean Triples Problem
- Co-editor of the Handbook of Satisfiability
He has advised multiple PhD students including Emre Yolcu, Joseph Reeves, and Bernardo Subercaseaux. His tools like DRAT-trim and QRAT-trim have become standard in proof validation.





