Marijn J.H. Heule

I moved to Carnegie Mellon University.

This page is no longer maintained. Visit the link above for the new webpage.

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.

In the Media

Selected articles on the ``largest math proof ever", check out Everything's Bigger in Texas for a complete list.

Appearences in Dutch media:

Publications

• 2019

  Marijn J. H. Heule, Manuel Kauers, and Martina Seidl (2019).
  Local Search for Fast Matrix Multiplication.
  To appear in SAT 2019. [arXiv].

  Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere (2019).
  Strong Extension-Free Proof Systems.
  Journal of Automated Reasoning. [pdf (recommended), link]

  Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere (2019).
  Encoding Redundancy for Satisfaction-Driven Clause Learning.
  In Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2019, pp. 41-58.
  Lecture Notes in Computer Science 11427, Springer. Best paper nomination. [pdf, link]

  Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere (2019).
  Clausal Proofs of Mutilated Chessboards.
  To appear in NASA Formal Methods (NFM) 2019. [pdf (preprint)]

• 2018

  Marijn J. H. Heule (2018).
  Schur Number Five.
  Proceedings of AAAI-18, pp. 6598-6606. [link, arXiv]

  Marijn J. H. Heule, Oliver Kullmann, and Armin Biere (2018).
  Cube and Conquer for Satisfiability.
  Handbook of Parallel Constraint Reasoning, Chapter 2, pp. 31-59. [link]

  Marijn J. H. Heule and Oliver Kullmann (2018).
  The Science of Brute Force.
  Best Writing on Mathematics 2018, pp. 46-66. [link]

  Marijn J. H. Heule and Armin Biere (2018).
  What a Difference a Variable Makes.
  In Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2018, pp. 75-92.
  Lecture Notes in Computer Science 10806, Springer. [pdf, doi]

  Benjamin Kiesl, Adrian Rebola-Pardo, and Marijn J.H. Heule (2018).
  Extended Resolution Simulates DRAT.
  In International Joint Conference on Automated Reasoning - IJCAR 2018, pp. 516-531.
  Lecture Notes in Computer Science 10900, Springer. Best paper award. [pdf]

  Marijn J. H. Heule (2018).
  Brute Trust.
  Nieuw Archief voor Wiskunde, 5th series, 19 (3): 226-227. [pdf]

  Armin Biere and Marijn J. H. Heule (2018).
  The Effect of Scrambling CNFs.
  Accepted for Pragmatics of Satisfiability. [pdf]

  Marijn J. H. Heule (2018).
  Computing Small Unit-Distance Graphs with Chromatic Number 5.
  Geombinatorics XXVIII(1): 32-50. [arXiv]

  Marijn J. H. Heule (2018).
  Optimal Symmetry Breaking for Graph Problems.
  Accepted for Mathematics in Computer Science.

• 2017

  Marijn J.H. Heule and Oliver Kullmann (2017).
  The Science of Brute Force.
  Communications of the ACM 60(8), 70-79. [link]

  Marijn J. H. Heule (2017).
  Avoiding Triples in Arithmetic Progression.
  Journal of Combinatorics 8(3): 391-422. [pdf]

  Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2017).
  Short Proofs Without New Variables.
  In Automated Deduction - CADE-26, pp. 130-147. Lecture Notes in Computer Science 10395, Springer. Best paper award. [pdf, doi, slides]

  Luís Cruz-Filipe, Marijn J.H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Peter Schneider-Kamp (2017).
  Efficient Certified RAT Verification.
  In Automated Deduction - CADE-26, pp. 220-236. Lecture Notes in Computer Science 10395, Springer. [pdf, doi]

  Marijn J.H. Heule, Oliver Kullmann, and Victor W. Marek (2017).
  Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method.
  Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17), pp. 4864-4868. [pdf, slides]

  Benjamin Kiesl, Marijn J.H. Heule, and Armin Biere (2017).
  A Little Blocked Literal Goes a Long Way.
  In Theory and Applications of Satisfiability Testing - SAT-2017, pp. 281-297.
  Lecture Notes in Computer Science 10491, Springer. [pdf, doi, slides]

  Marijn J.H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere (2017).
  PRuning Through Satisfaction.
  In Haifa Verification Conference - HVC 2017, pp. 179-194. Lecture Notes in Computer Science 10629, Springer. Best paper award [pdf, doi, slides]

  Katalin Fazekas, Marijn J.H. Heule, Martina Seidl, and Armin Biere (2017).
  Skolem Function Composition for Quantified Boolean Formulas.
  In Tests and Proofs - TAP 2017, pp. 129-138. Lecture Notes in Computer Science 10375, Springer. [pdf, doi]

  Marijn J.H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Nathan D. Wetzler (2017).
  Efficient, Verified Checking of Propositional Proofs.
  In Interactive Theorem Proving - ITP 2017, pp. 269-284.
  Lecture Notes in Computer Science 10499, Springer. [pdf, doi]

  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 and Benjamin Kiesl (2017).
  The Potential of Interference-Based Proof Systems.
  In ARCADE 2017, pp. 51-54. EPiC Series in Computing 51. [pdf, slides]

  J S. Moore and Marijn J.H. Heule (2017).
  Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions.
  In ARCADE 2017, pp. 42-45. EPiC Series in Computing 51. [pdf, slides]

  Marijn J.H. Heule (2017).
  Everything's Bigger in Texas: ``The Largest Math Proof Ever''.
  3rd Global Conference on Artificial Intelligence, pp. 1-5. EPiC Series in Computing 50. [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]

  Keenan Breik, Lakshmi Prakash, Chris Thachuk, Marijn J.H. Heule, and David Soloveichik (2017).
  Computing properties of stable configurations of thermodynamic binding networks. [arXiv]

• 2016

  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]

• 2015

  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. [link]

  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]

• 2014

  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]

• 2013

  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]

• 2012

  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. Best paper award. [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]

• 2011

  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]

• 2010

  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]

• 2009

  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. Best paper award. [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]

• 2008

  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]

• 2007

  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]

• 2006

  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]

• 2005

  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]

Talks

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

• 2016

  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]

Software