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. My resume offers
more details.
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
Selected articles on the ``largest math proof ever", check out Everything's Bigger in Texas for a complete list.
Appearences in Dutch media:
Marijn J. H. Heule and Oliver Kullmann (2017).
The Science of Brute Force.
Accepted for Communications of the ACM.
Marijn J. H. Heule (2017).
Avoiding Triples in Arithmetic Progression.
Accepted for Journal of Combinatorics.
Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere (2017).
Short Proofs without New Variables.
Accepted for CADE 2017.
[pdf]
Luís Cruz-Filipe, Marijn J.H. Heule, Warren Hunt, Matt Kaufmann, and Peter Schneider-Kamp (2017).
Efficient Certified RAT Verification.
Accepted for CADE 2017.
[pdf]
Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek (2017).
Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method.
To appear in IJCAI 2017.
[pdf]
Katalin Fazekas, Marijn J.H. Heule, Martina Seidl, and Armin Biere (2017).
Skolem Function Composition for Quantified Boolean Formulas.
Accepted for TAP 2017.
[pdf]
Marijn J.H. Heule, Warren Hunt, Matt Kaufmann, and Nathan Wetzler (2017).
Efficient, Verified Checking of Propositional Proofs.
Accepted for ITP 2017.
[pdf]
Tomas Balyo, Marijn J.H. Heule, and Matti Järvisalo (2017).
SAT Competition 2016: Recent Developments.
Proceedings of AAAI 2017, pp. 5061-5063.
[pdf]
Valentin Wüstholz, Oswaldo Olivo, Marijn J.H. Heule, and Işıl Dillig (2017).
Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions.
In Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2017, pp. 3-20.
Lecture Notes in Computer Science 10206, Springer. Best paper award.
[pdf, arXiv]
Marijn J.H. Heule, Oliver Kullmann, and Victor W. Marek (2016).
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer.
In Theory and Applications of Satisfiability Testing – SAT 2016, pp. 228-245.
Lecture Notes in Computer Science 9710, Springer. Best paper award.
[pdf, doi,
slides]
Files and tools of the ``largest math proof ever" are available at
Everything's Bigger in Texas.
Cuong Kim Chau and Marijn J.H. Heule (2016).
Computing Maximum Unavoidable Subgraphs Using SAT Solvers.
In Theory and Applications of Satisfiability Testing – SAT 2016, pp. 196-211.
Lecture Notes in Computer Science 9710, Springer.
[pdf,
doi]
Marijn J.H. Heule, Martina Seidl, and Armin Biere (2016).
Solution Validation and Extraction for QBF Preprocessing
Journal of Automated Reasoning 58(1), 97-125.
[pdf, doi]
Marijn J.H. Heule (2016).
The Quest for Perfect and Compact Symmetry Breaking for Graph Problems.
Accepted for SYNASC 2016.
[pdf, slides]
Marijn J.H. Heule, Rezwana Reaz, H. B. Acharya, and Mohamed G. Gouda (2016).
Analysis of Computing Policies Using SAT Solvers (Short Paper).
In 18th International Symposium on Stabilization, Safety, and Security of Distributed Systems – SSS 2016 pp. 1-5.
Lecture Notes in Computer Science 10083, Springer.
[pdf]
Marijn J.H. Heule and Sean Weaver (2015).
Proceedings of Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference,
Austin, TX, USA, September 24-27, 2015.
Lecture Notes in Computer Science 9340, Springer. ISBN 978-3-319-24317-7.
Marijn J.H. Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere (2015).
Clause Elimination for SAT and QSAT.
Journal of Artificial Intelligence Research (JAIR) 53: 127-168.
[pdf]
Marijn J.H. Heule and Stefan Szeider (2015).
A SAT Approach to Clique-Width.
ACM Transactions on Computational Logic (TOCL) 16(3): 24 [pdf]
Marijn J.H. Heule, Warren Hunt, Jr., and Nathan Wetzler (2015).
Expressing Symmetry Breaking in DRAT Proofs.
In Automated Deduction - CADE-25, pp. 591-606. Lecture Notes in Computer Science 9195, Springer.
[pdf, slides]
Marijn J.H. Heule and Armin Biere (2015).
Compositional Propositional Proofs.
In LPAR-20, pp. 444-459. Lecture Notes in Computer Science 9450, Springer.
[pdf, slides]
Marijn J.H. Heule, Martina Seidl, and Armin Biere (2015).
Blocked Literals are Universal.
In NASA Formal Methods - NFM 2015, pp. 436-442. Lecture Notes in Computer Science 9058, Springer.
[pdf, slides]
Marijn J.H. Heule and Torsten Schaub (2015).
What's Hot in the SAT and ASP Competitions.
In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI 2015), pp. 4322-4323. AAAI Press.
[pdf]
Marijn J.H. Heule and Armin Biere (2015).
Proofs for Satisfiability Problems.
Chapter 1 of All about Proofs, Proofs for all.
[pdf, slides]
Marijn J.H. Heule and Armin Biere (2015).
Clausal Proof Compression.
Accepted for the 11th International Workshop on the Implementation of Logics.
[pdf]
Rezwana Reaz, Muqeet Ali, Mohamed G. Gouda, Marijn J.H. Heule, and Ehab S. Elmallah (2015).
The Implication Problem of Computing Policies.
In Stabilization, Safety, and Security of Distributed Systems, pp. 109-123.
Lecture Notes in Computer Science 9212, Springer.
[pdf]
Marijn J.H. Heule, Matina Seidl and Armin Biere (2014).
Efficient Extraction of Skolem Functions from QRAT Proofs.
In Formal Methods in Computer-Aided Design 2014, pp. 107-114.
[pdf]
Marijn J.H. Heule, Matina Seidl and Armin Biere (2014).
A Unified Proof System for QBF Preprocessing.
In 7th International Joint Conference on Artifical Reasoning, IJCAR 2014, pp. 91-106.
Lecture Notes in Computer Science Volume 8562, Springer.
[pdf]
Anton Belov, Marijn J.H. Heule and Joao Marques-Silva (2014).
MUS Extraction Using Clausal Proofs.
In Theory and Applications of Satisfiability Testing – SAT 2014, pp. 48-57.
Lecture Notes in Computer Science 8561, Springer.
[pdf]
Marijn J.H. Heule, Warren A. Hunt and Nathan Wetzler (2014).
Bridging the gap between easy generation and efficient verification of unsatisfiability proofs.
Software Testing, Verification and Reliability 24(8):593-607.
[pdf]
Tomas Balyo, Andreas Fröhlich, Marijn J.H. Heule and Armin Biere (2014).
Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask).
In Theory and Applications of Satisfiability Testing – SAT 2014, pp. 317-332.
Lecture Notes in Computer Science 8561, Springer.
[pdf]
Nathan Wetzler, Marijn J.H. Heule and Warren A. Hunt (2014).
DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs.
In Theory and Applications of Satisfiability Testing – SAT 2014, pp. 422-429.
Lecture Notes in Computer Science 8561, Springer.
[pdf]
Marijn J.H. Heule and Sicco Verwer (2013).
Software model synthesis using satisfiability solvers.
Empirical Software Engineering 18(4): 825-856.
[doi]
Marijn J.H. Heule, Warren A. Hunt, Jr. and Nathan Wetzler (2013).
Trimming while checking clausal proofs.
In Formal Methods in Computer-Aided Design 2013, pp. 181-188.
[pdf]
Marijn J.H. Heule, Warren Hunt, Jr., and Nathan Wetzler (2013).
Verifying Refutations with Extended Resolution.
In Automated Deduction - CADE-24, pp. 345-359. Lecture Notes in Computer Science 7898, Springer.
[pdf]
Nathan Wetzler, Marijn J.H. Heule and Warren A. Hunt, Jr. (2013).
Mechanical Verification of SAT Refutations with Extended Resolution.
In Interactive Theorem Proving 2013, pp. 229–244. Lecture Notes in Computer Science 7998, Springer.
[pdf]
Marijn J.H. Heule, Matti Järvisalo and Armin Biere (2013).
Revisiting Hyper Binary Resolution.
In CPAIOR 2013, pp. 77-93. Lecture Notes in Computer Science 7874, Springer.
[pdf]
Marijn J.H. Heule and Armin Biere (2013).
Blocked Clause Decomposition.
In Logic for Programming, Artificial Intelligence, and Reasoning 2013, pp. 423-438.
Lecture Notes in Computer Science 8312, Springer.
[pdf]
Marijn J.H. Heule and Stefan Szeider (2013).
A SAT Approach to Clique-Width.
In Theory and Applications of Satisfiability Testing – SAT 2013, pp. 318-334.
Lecture Notes in Computer Science 7962, Springer.
[pdf]
Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn J.H. Heule, Gerti Kappel, Martina Seidl and Hans Tompits (2013).
Guided merging of sequence diagrams.
In Software Language Engineering, pp. 164-183.
Lecture Notes in Computer Science 7745, Springer.
[doi]
Norbert Manthey, Marijn J.H. Heule, and Armin Biere (2012).
Automated Reencoding of Boolean Formulas.
In Haifa Verification Conference 2012, pp. 102-117. Lecture Notes in Computer Science 7857, Springer.
[doi]
Peter van der Tak, Marijn J.H. Heule, and Armin Biere (2012).
Concurrent Cube-and-Conquer.
In Pragmatics of SAT.
Peter van der Tak, Marijn J.H. Heule, and Armin Biere (2012).
Concurrent Cube-and-Conquer: Poster Presentation.
In Theory and Applications of Satisfiability Testing – SAT 2012, pp. 475-476.
Lecture Notes in Computer Science 7317, Springer.
[doi]
Matti Järvisalo, Marijn J.H. Heule, and Armin Biere (2012).
Inprocessing Rules.
In 6th International Joint Conference, IJCAR, pp. 355-370.
Lecture Notes in Computer Science 7364, Springer.
[doi]
Matti Järvisalo, Armin Biere, and Marijn J.H. Heule (2012).
Simulating Circuit-Level Simplifications on CNF.
Journal of Automated Reasoning 49(4):583-619.
[doi]
Marijn J.H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere (2012).
Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.
In Haifa Verification Conference 2011, pp. 50-65. Lecture Notes in Computer Science 7261, Springer.
[pdf]
Peter van der Tak, Antonio Ramos, and Marijn J.H. Heule (2011).
Reusing the Assignment Trail in CDCL Solvers.
Journal on Satisfiability, Boolean Modeling and Computation 7:133-138.
[pdf]
Oliver Gableske and Marijn J.H. Heule (2011).
EagleUP: Solving Random 3-SAT using SLS with Unit Propagation.
In Pragmatics of SAT 2011.
[pdf]
Oliver Gableske and Marijn J.H. Heule (2011).
EagleUP: Solving Random 3-SAT using SLS with Unit Propagation.
In SAT 2011, pp. 367-368. Lecture Notes in Computer Science 6695, Springer.
[pdf]
Antonio Ramos, Peter van der Tak, and Marijn J.H. Heule (2011).
Between Restarts and Backjumps.
In K.A. Sakallah and L. Simon (Eds.), SAT 2011, pp. 216-229. Lecture Notes in Computer Science, Springer.
[pdf]
Marijn J.H. Heule, Matti Järvisalo, and Armin Biere (2011).
Efficient CNF Simplification based on Binary Implication Graphs.
In K.A. Sakallah and L. Simon (Eds.), SAT 2011, pp. 201-215. Lecture Notes in Computer Science 6695, Springer.
[pdf]
Shai Haim and Marijn Heule (2010).
Towards Ultra Rapid Restarts.
Technical Report, UNSW and TU Delft.
[pdf]
Marijn J.H. Heule, Matti Järvisalo, and Armin Biere (2010).
Covered Clause Elimination.
In Short paper proceedings of LPAR-17, 17th International Conference on Logic for Programming,
Artificial Intelligence and Reasoning, Yogyakarta, Indonesia, October 10th - 15th, 2010. EasyChair Proceedings.
[pdf]
Marijn J.H. Heule, Matti Jarvisalo, and Armin Biere (2010).
Blocked Clause Elimination and its Extentions.
Technical Report, Proceedings of Guangzhou Symposium on Satisfiability In Logic-Based Modeling.
[pdf]
Sid Mijnders, Boris de Wilde, and Marijn J.H. Heule (2010).
Symbiosis of Search and Heuristics for Random 3-SAT.
In David Mitchell and Eugenia Ternovska (Eds.),
Proceedings of the Third International Workshop on Logic and Search (LaSh 2010).
[pdf]
Marijn J.H. Heule and Toby Walsh (2010).
Internal Symmetry.
In Pierre Flener and Justin Pearson (Eds.), The 10th International Workshop on Symmetry in Constraint
Satisfaction Problems (SymCon'10), pp. 19-33.
[pdf]
Marijn J.H. Heule, Matti Järvisalo, and Armin Biere (2010).
Clause Elimination Procedures for CNF Formula.
[pdf]
Marijn J.H. Heule and Sicco Verwer (2010).
Exact DFA Identification Using SAT Solvers.
In José M. Sempere and Pedro García (Eds.), Grammatical Inference: Theoretical Results
and Applications 10th International Colloquium, ICGI 2010, pp. 66-79. Lecture Notes in Computer Science 6339, Springer.
[pdf]
Marijn J.H. Heule and Toby Walsh (2010).
Symmetry within Solutions.
In Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence (AAAI 2010), pp. 77-82. AAAI Press.
[pdf]
Matti Järvisalo, Armin Biere, and Marijn J.H. Heule (2010).
Blocked Clause Elimination.
In J. Esparza and R. Majumdar (Eds.), TACAS 2010, pp. 129-144. Lecture Notes in Computer Science 6015, Springer.
[pdf]
Marijn J.H. Heule and Sicco Verwer (2009).
Using a satisfiability solver to identify deterministic finite state automata.
In Toon Calders and Karl Tuyls and Mykola Pechenizkiy (Eds.), BNAIC 2009, pp. 91-98, October 29-30, 2009, Eindhoven.
BNAIC.
[pdf]
Bas Schaafsma, Marijn J.H. Heule, and Hans van Maaren (2009).
Dynamic Symmetry Breaking by Simulating Zykov Contraction.
In Oliver Kullmann (Eds.), Theory and Applications of Satisfiability Testing -- SAT 2009, pp. 223-236,
June 30 - July 3, 2009, Swansea. LNCS 5584, Springer.
[pdf]
Marijn J.H. Heule and Hans van Maaren (2009).
Look-Ahead Based SAT Solvers.
In Armin Biere and Marijn J.H. Heule and Hans van Maaren and Toby Walsh (Eds.),
Chapter 5 of Handbook os Satisfiability, pp. 155-184. IOS Press.
[pdf, doi]
Armin Biere, Marijn J.H. Heule, Hans van Maaren, and Toby Walsh (2009).
Handbook of Satisfiability.
Frontiers in Artificial Intelligence and Applications, volume 85. IOS Press.
[link]
Marijn J.H. Heule (2008).
SmArT solving: Tools and techniques for satisfiability solvers.
PhD Thesis, TU Delft.
[pdf]
Marijn J.H. Heule (2008).
Solving edge-matching problems with satisfiability solvers.
In Proceedings of the Second International Workshop on Logic and Search (LaSh 2008), pp. 88-102. University of Leuven.
[pdf]
Marijn J.H. Heule and Hans van Maaren (2008).
Whose side are you on? Finding solutions in a biased search-tree.
Journal on Satisfiability, Boolean Modeling and Computation 4:117-148.
[pdf]
Marijn J.H. Heule and Hans van Maaren (2008).
Parallel SAT Solving using Bit-level Operations.
Journal on Satisfiability, Boolean Modeling and Computation 4:99-116.
[pdf]
Henriette Bier, Adriaan de Jong, Gijs van der Hoorn, Niels Brouwers, Marijn J.H. Heule, and Hans van Maaren (2007).
Prototypes for Automated Architectural 3D-Layout.
In T.G. Wyeld and S. Kenderdine and M. Docherty (Eds.),
Proceedings of the 13th International Conference on Virtual Systems and Multimedia, pp. 203-214.
Lecture Notes in Computer Science 4820, Springer.
[pdf]
Hans van Maaren, Linda van Norden, and Marijn J.H. Heule (2008).
Sums of squares based approximation algorithms for MAX-SAT.
Discrete Applied Mathematics 156(10):1754-1779.
[doi]
Marijn J.H. Heule and Hans van Maaren (2007).
From Idempotent Generalized Boolean Assignments to Multi-bit Search.
In Joao Marques-Silva and Karem A. Sakallah (Eds.),
Theory and Applications of Satisfiability Testing - SAT 2007, pp. 134-147.
Lecture Notes in Computer Science 4501, Springer.
[pdf]
Marijn J.H. Heule and Hans van Maaren (2007).
Effective Incorporation of Double Look-Ahead Procedures.
In Joao Marques-Silva and Karem A. Sakallah (Eds.),
Theory and Applications of Satisfiability Testing - SAT 2007, pp. 258-271.
Lecture Notes in Computer Science 4501, Springer.
[pdf]
Marijn J.H. Heule and Leon J.M. Rothkrantz (2007).
Solving Games: Dependance of applicable solving procedures.
Science of Computer Programming 67(1):105-124.
[pdf]
Paul R. Herwig, Marijn J.H. Heule, Martijn van Lambalgen, and Hand van Maaren (2007).
A New Method to Construct Lower Bounds for Van der Waerden Numbers.
The Electronic Journal of Combinatorics 14:1-18.
[pdf]
Marijn J.H. Heule and Hans van Maaren (2006).
Whose side are you on? Finding solutions in a biased search-tree.
Technical Report, Proceedings of Guangzhou Symposium on Satisfiability In Logic-Based Modeling.
[pdf]
Marijn J.H. Heule and Hans van Maaren (2006).
March_dl: Adding Adaptive Heuristics and a New Branching Strategy.
Journal on Satisfiability, Boolean Modeling and Computation 2:47-59.
[pdf]
Marijn J.H. Heule, Joris E. van Zwieten, Mark Dufour and Hans van Maaren (2005).
March_eq: Implementing Additional Reasoning into an Efficient Lookahead Sat Solver.
In Holger H. Hoos and David G. Mitchell (Eds.), SAT 2004, pp. 345-359.
Lecture Notes in Computer Science 3542, Springer.
[pdf]
Marijn J.H. Heule and Hans van Maaren (2005).
Aligning CNF- and Equivalence- Reasoning.
In Holger H. Hoos and David G. Mitchell (Eds.), SAT 2004, pp. 145-156.
Lecture Notes in Computer Science 3542, Springer.
[pdf]
Marijn J.H. Heule and Hans van Maaren (2005).
Observed Lower Bounds for Random 3-Sat Phase Transition Density using Linear Programming.
In Fahiem Bacchus and Toby Walsh (Eds.), SAT 2005, pp. 122-134.
Lecture Notes in Computer Science 3569, Springer.
[pdf]
Selected invited talks and tutorials. Slides of conference talks can be found under publications.
Invisted talk at the Logic and Search Workshop in New York on October 17, 2016.
Everything's Bigger in Texas - The Largest Math Proof Ever. [slides]
Dagstuhl talk in Wadern, Germany on September 20, 2016.
Practical Proof Systems for SAT and QBF. [slides]
Talk during research visit to Rice University on August 24, 2016.
Everything's Bigger in Texas - The Largest Math Proof Ever. [slides]
Talk at the Fields Institute in Toronto, Canada on August 18, 2016.
Applications of SAT solving to Mathematics: Proofs and Heuristics. [slides]
Talk during research visit to the Max Planck Institute in Saarbruecken, Germany on July 27, 2016.
Everything's Bigger in Texas - The Largest Math Proof Ever. [slides]
Tutorial at the Industry Day of SAT 2016 in Bordeaux, France on July 9, 2016.
Proofs of Unsatisfiability. [slides]
Talk during research visit to Johannes Kepler University in Linz, Austria on June 22, 2016.
Everything's Bigger in Texas - The Largest Math Proof Ever. [slides]
An invited talk at the 50 Years of the Hales-Jewett Theorem conference in Bellingham, Washington on May 6, 2016.
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. [slides]