| 2026 | AAAI | On the Edge of Core (Non-)Emptiness: An Automated Reasoning Approach to Approval-Based Multi-Winner Voting. | Ratip Emin Berker, Emanuel Tewolde, Vincent Conitzer, Mingyu Guo, Marijn Heule, Lirong Xia |
| 2025 | CADE | Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification. | Yi Zhou, Amar Shah, Zhengyao Lin, Marijn Heule, Bryan Parno |
| 2023 | FMCAD | Mariposa: Measuring SMT Instability in Automated Program Verification. | Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, Bryan Parno |
| 2023 | LPAR | Toward Optimal Radio Colorings of Hypercubes via SAT-solving. | Bernardo Subercaseaux, Marijn Heule |
| 2022 | MICRO | A programmable, energy-minimal dataflow compiler and architecture. | Graham Gobieski, Souradip Ghosh, Marijn Heule, Todd C. Mowry, Tony Nowatzki, Nathan Beckmann, Brandon Lucia |
| 2021 | NSDI | Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. | Travis Hance, Marijn Heule, Ruben Martins, Bryan Parno |
| 2020 | AAAI | Constructing Minimal Perfect Hash Functions Using SAT Technology. | Sean A. Weaver, Marijn Heule |
| 2020 | CADE | The Resolution of Keller's Conjecture. | Joshua Brakensiek, Marijn Heule, John Mackey, David E. Narvez |
| 2020 | LPAR | Coloring Unit-Distance Strips using SAT. | Peter Oostema, Ruben Martins, Marijn Heule |
| 2020 | LPAR | Sensitivity Analysis of Locked Circuits. | Joseph Sweeney, Marijn Heule, Lawrence T. Pileggi |
| 2018 | SAT | The Effect of Scrambling CNFs. | Armin Biere, Marijn Heule |
| 2017 | CADE | The Potential of Interference-Based Proof Systems. | Marijn Heule, Benjamin Kiesl |
| 2017 | ITP | Efficient, Verified Checking of Propositional Proofs. | Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler |
| 2015 | AAAI | What's Hot in the SAT and ASP Competitions. | Marijn Heule, Torsten Schaub |
| 2015 | CADE | Expressing Symmetry Breaking in DRAT Proofs. | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2015 | LPAR | Clausal Proof Compression. | Marijn Heule, Armin Biere |
| 2015 | SSS | The Implication Problem of Computing Policies. | Rezwana Reaz, Muqeet Ali, Mohamed G. Gouda, Marijn Heule, Ehab S. Elmallah |
| 2014 | CADE | A Unified Proof System for QBF Preprocessing. | Marijn Heule, Martina Seidl, Armin Biere |
| 2014 | FMCAD | Efficient extraction of Skolem functions from QRAT proofs. | Marijn Heule, Martina Seidl, Armin Biere |
| 2014 | SAT | Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask). | Toms Balyo, Andreas Frhlich, Marijn Heule, Armin Biere |
| 2014 | SAT | MUS Extraction Using Clausal Proofs. | Anton Belov, Marijn Heule, Joo Marques-Silva |
| 2014 | SAT | Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers. | Marijn Heule, Norbert Manthey, Tobias Philipp |
| 2014 | SAT | DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. | Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr. |
| 2013 | CADE | Verifying Refutations with Extended Resolution. | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2013 | CPAIOR | Revisiting Hyper Binary Resolution. | Marijn Heule, Matti Jrvisalo, Armin Biere |
| 2013 | FMCAD | Trimming while checking clausal proofs. | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2013 | ITP | Mechanical Verification of SAT Refutations with Extended Resolution. | Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr. |
| 2013 | LPAR | Blocked Clause Decomposition. | Marijn Heule, Armin Biere |
| 2013 | SAT | A SAT Approach to Clique-Width. | Marijn Heule, Stefan Szeider |
| 2012 | CADE | Inprocessing Rules. | Matti Jrvisalo, Marijn Heule, Armin Biere |
| 2012 | SAT | Concurrent Cube-and-Conquer - (Poster Presentation). | Peter van der Tak, Marijn Heule, Armin Biere |
| 2012 | SLE | Guided Merging of Sequence Diagrams. | Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits |
| 2011 | SAT | EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation. | Oliver Gableske, Marijn Heule |
| 2011 | SAT | Efficient CNF Simplification Based on Binary Implication Graphs. | Marijn Heule, Matti Jrvisalo, Armin Biere |
| 2011 | SAT | Between Restarts and Backjumps. | Antonio Ramos, Peter van der Tak, Marijn Heule |
| 2010 | AAAI | Symmetry in Solutions. | Marijn Heule, Toby Walsh |
| 2010 | LPAR | Clause Elimination Procedures for CNF Formulas. | Marijn Heule, Matti Jrvisalo, Armin Biere |
| 2010 | LPAR | Covered Clause Elimination. | Marijn Heule, Matti Jrvisalo, Armin Biere |
| 2010 | TACAS | Blocked Clause Elimination. | Matti Jrvisalo, Armin Biere, Marijn Heule |
| 2009 | SAT | Dynamic Symmetry Breaking by Simulating Zykov Contraction. | Bas Schaafsma, Marijn Heule, Hans van Maaren |
| 2007 | SAT | From Idempotent Generalized Boolean Assignments to Multi-bit Search. | Marijn Heule, Hans van Maaren |
| 2007 | SAT | Effective Incorporation of Double Look-Ahead Procedures. | Marijn Heule, Hans van Maaren |
| 2005 | SAT | Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming. | Marijn Heule, Hans van Maaren |
| 2004 | SAT | March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver. | Marijn Heule, Mark Dufour, Joris E. van Zwieten, Hans van Maaren |
| 2004 | SAT | Aligning CNF- and Equivalence-reasoning. | Marijn Heule, Hans van Maaren |
| 2004 | SAT | Aligning CNF- and Equivalence-Reasoning. | Marijn Heule, Hans van Maaren |