avatar

Marijn J.H. Heule
Associate Professor at Carnegie Mellon University

Short Bio

I am an Associate Professor in the Computer Science Department at Carnegie Mellon University and received my PhD at Delft University of Technology in the Netherlands. 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.

Contact Information

Gates-Hillman Complex 9107
School of Computer Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213-3891

email (work): marijn@cmu.edu
email (personal): marijn@heule.nl
homepage: http://www.cs.cmu.edu/~mheule

Citations


source: Google Scholar Citations

Teaching

Fall 2020: 15-816 Advanced Topics in Logic: Automated Reasoning and Satisfiability

Spring 2020: 15-210 Parallel and Sequential Datastructures and Algorithms

Fall 2019: 15-816 Advanced Topics in Logic: Automated Reasoning and Satisfiability

In the Media

Recent articles in Quanta Magazine on computer search for proofs

Quanta Magazine
August 19, 2020
Computer Search Settles 90-Year-Old Math Problem [online]
Quanta Magazine
August 26, 2020
Computer Scientists Attempt to Corner the Collatz Conjecture [online]

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.

Appearence on YouTube:

Numberphile
May 17, 2018
The Problem with 7825
Viewed 1,050,626 times (August 15, 2020).

Publications

  • 2020

    Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere (2020).
    Strong Extension-Free Proof Systems.
    Journal of Automated Reasoning 64: 533-554. [pdf (recommended), doi]

    Benjamin Kiesl, Adrian Rebola-Pardo, Marijn J.H. Heule, and Armin Biere (2020).
    Simulating Strong Practical Proof Systems with Extended Resolution.
    Accepted for the Journal of Automated Reasoning. [pdf, doi]

    Joshua Brakensiek, Marijn J. H. Heule, John Mackey, and David E. Narvaez (2020).
    The Resolution of Keller's Conjecture.
    In International Joint Conference on Automated Reasoning - IJCAR 2020, pp. 48-65.
    Lecture Notes in Artificial Intelligence 12166, Springer. Best paper award [homepage, pdf, doi, slides]

    Sean A. Weaver and Marijn J. H. Heule (2020).
    Constructing Minimal Perfect Hash Functions Using SAT Technology.
    Association for the Advancement of Artificial Intelligence - AAAI 2020, pp. 1668-1675. [arXiv, pdf, doi]

    Emre Yolcu, Xinyu Wu, and Marijn J. H. Heule (2020).
    Mycielski graphs and PR proofs.
    In Theory and Practice of Satisfiability Testing - SAT 2020, pp. 201-217.
    Lecture Notes in Computer Science 12178, Spinger. Best student paper award [pdf, doi]

    Peter Oostema, Ruben Martins, and Marijn J. H. Heule (2020).
    Coloring Unit-Distance Strips using SAT.
    In Logic for Programming, Artificial Intelligence and Reasoning - LPAR-23, pp. 373-389.
    EPiC Series in Computing 73, EasyChair. [pdf, doi]

    Joseph Sweeney, Marijn J. H. Heule, and Lawrence Pileggi (2020).
    Sensitivity Analysis of Locked Circuits.
    In Logic for Programming, Artificial Intelligence and Reasoning - LPAR-23, pp. 483-497.
    EPiC Series in Computing 73, EasyChair. [pdf, doi]

    Joseph Sweeney, Marijn J. H. Heule, and Lawrence Pileggi (2020).
    Modeling Techniques for Logic Locking.
    To appear int International Conference On Computer Aided Design - ICCAD 2020.

    Leroy Chew and Marijn J. H. Heule (2020).
    Sorting Parity Encodings by Reusing Variables.
    In Theory and Practice of Satisfiability Testing - SAT 2020, pp. 1-10.
    Lecture Notes in Computer Science 12178, Spinger. [pdf, doi]

  • 2019

    Marijn J. H. Heule (2019).
    Trimming Graphs Using Clausal Proof Optimization.
    In Constraint Programming - CP 2019, pp. 251-267.
    Lecture Notes in Computer Science 11802, Springer. [arXiv, link, slides]

    Benjamin Kiesl, Marijn J. H. Heule, and Armin Biere (2019).
    Truth Assignments as Conditional Autarkies.
    Automated Technology for Verification and Analysis - ATVA 2019, pp. 48-64.
    Lecture Notes in Computer Science 11781, Springer. [pdf (preprint), doi]

    Marijn J. H. Heule, Manuel Kauers, and Martina Seidl (2019).
    Local Search for Fast Matrix Multiplication.
    In Theory and Applications of Satisfiability Testing – SAT 2019, pp. 155-163.
    Lecture Notes in Computer Science 11628, Springer. [arXiv, doi, slides]

    Marijn J. H. Heule, Manuel Kauers, and Martina Seidl (2019).
    A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications.
    ACM Communications in Computer Algebra 53(3). [pdf, doi, poster]

    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, slides]

    Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere (2019).
    Clausal Proofs of Mutilated Chessboards.
    In NASA Formal Methods (NFM), pp. 204-210.
    Lecture Notes in Computer Science 11460, Springer. [pdf (preprint), doi, slides]

    Marijn J. H. Heule, Matti Järvisalo, and Martin Suda (2019).
    SAT Competition 2018.
    Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 11(1): 133-154. [link (open access)]

    Marijn J. H. Heule, Manuel Kauers, and Martina Seidl (2019).
    New ways to multiply 3 x 3-matrices.
    Under submission. [arXiv]

    Marijn J. H. Heule (2019).
    Optimal Symmetry Breaking for Graph Problems.
    Mathematics in Computer Science 13(4), 533-548. [pdf, doi]

    Keenan Breik, Chris Thachuk, Marijn J. H. Heule, and David Soloveichik (2019).
    Computing properties of stable configurations of thermodynamic binding networks.
    Theoretical Computer Science 785: 17-29. [doi]

  • 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]

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

    Christiaan Hartman, Marijn J. H. Heule, Kees Kwekkeboom, and Alain Noels (2013).
    Symmetry in Gardens of Eden.
    In The Electronic Journal of Combinatorics 20: P16. [link]

    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

DRAT-trim
DRAT-trim is a satisfiability proof checking and trimming utility designed to validate proofs for all known satisfiability solving and preprocessing techniques. DRAT-trim can also emit trimmed formulas, optimized proofs, and TraceCheck+ dependency graphs.
QRAT-trim
QRAT-trim is a proof checking utility for quantified Boolean formulas and is based on the QRAT proof system. The tool also supports the conversion of QRAT proofs into Skolem functions.
Cube-and-Conquer
The cube-and-conquer parallel SAT solving paradigm combines look-ahead techniques for splitting with conflict-driven clause-learning techniques.
March
The March SAT solver (latest version march_br) is based on the lookahead architecture. It is the latest version in the march family of solvers, which won many medals at various SAT competitions. See the SAT 2004 paper for details.
DRUP-trim
DRUP-trim is a proof checking utility based on the reverse unit propagation redundancy property. The tool was used to validate the results of SAT Competition 2013.