March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver. - Marijn Heule; Mark Dufour; Joris E. van Zwieten; Hans van Maaren (SAT (Selected Papers, 2004)

Aligning CNF- and Equivalence-reasoning. - Marijn Heule; Hans van Maaren (SAT, 2004)

Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming. - Marijn Heule; Hans van Maaren (SAT, 2005)

March_dl: Adding Adaptive Heuristics and a New Branching Strategy. - Marijn Heule; Hans van Maaren (J. Satisf. Boolean Model. Comput., 2006)

From Idempotent Generalized Boolean Assignments to Multi-bit Search. - Marijn Heule; Hans van Maaren (SAT, 2007)

Effective Incorporation of Double Look-Ahead Procedures. - Marijn Heule; Hans van Maaren (SAT, 2007)

Prototypes for Automated Architectural 3D-Layout. - Henriette Bier; Adriaan de Jong; Gijs van der Hoorn; Niels Brouwers; Marijn Heule; Hans van Maaren (VSMM, 2007)

A New Method to Construct Lower Bounds for Van der Waerden Numbers. - P. R. Herwig; M. J. H. Heule; P. M. van Lambalgen; Hans van Maaren (Electron. J. Comb., 2007)

Solving games: Dependence of applicable solving procedures. - M. J. H. Heule; Léon J. M. Rothkrantz (Sci. Comput. Program., 2007)

Sums of squares based approximation algorithms for MAX-SAT. - Hans van Maaren; Linda van Norden; M. J. H. Heule (Discret. Appl. Math., 2008)

Parallel SAT Solving using Bit-level Operations. - Marijn Heule; Hans van Maaren (J. Satisf. Boolean Model. Comput., 2008)

Whose side are you on? Finding solutions in a biased search-tree. - Marijn Heule; Hans van Maaren (J. Satisf. Boolean Model. Comput., 2008)

SmArT solving: tools and techniques for satisfiability solvers. - M. J. H. Heule (2008)

Dynamic Symmetry Breaking by Simulating Zykov Contraction. - Bas Schaafsma; Marijn Heule; Hans van Maaren (SAT, 2009)

Look-Ahead Based SAT Solvers. - Marijn Heule; Hans van Maaren (Handbook of Satisfiability, 2009)

Symmetry in Solutions. - Marijn Heule; Toby Walsh (AAAI, 2010)

Exact DFA Identification Using SAT Solvers. - Marijn Heule; Sicco Verwer (ICGI, 2010)

Clause Elimination Procedures for CNF Formulas. - Marijn Heule; Matti Järvisalo; Armin Biere (LPAR (Yogyakarta), 2010)

Covered Clause Elimination. - Marijn Heule; Matti Järvisalo; Armin Biere (LPAR short papers(Yogyakarta), 2010)

Blocked Clause Elimination. - Matti Järvisalo; Armin Biere; Marijn Heule (TACAS, 2010)

Symmetry within Solutions - Marijn Heule; Toby Walsh (CoRR, 2010)

Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. - Marijn Heule; Oliver Kullmann; Siert Wieringa; Armin Biere (Haifa Verification Conference, 2011)

EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation. - Oliver Gableske; Marijn Heule (SAT, 2011)

Efficient CNF Simplification Based on Binary Implication Graphs. - Marijn Heule; Matti Järvisalo; Armin Biere (SAT, 2011)

Between Restarts and Backjumps. - Antonio Ramos; Peter van der Tak; Marijn Heule (SAT, 2011)

Reusing the Assignment Trail in CDCL Solvers. - Peter van der Tak; Antonio Ramos; Marijn Heule (J. Satisf. Boolean Model. Comput., 2011)

Introduction to Mathematics of Satisfiability, Victor W. Marek, Chapman & Hall/CRC, 2009. Hardback, ISBN-13: 978-143980167-3, $89.95. - Marijn Heule (Theory Pract. Log. Program., 2011)

Inprocessing Rules. - Matti Järvisalo; Marijn Heule; Armin Biere (IJCAR, 2012)

Automated Reencoding of Boolean Formulas. - Norbert Manthey; Marijn Heule; Armin Biere (Haifa Verification Conference, 2012)

Concurrent Cube-and-Conquer - (Poster Presentation). - Peter van der Tak; Marijn Heule; Armin Biere (SAT, 2012)

Guided Merging of Sequence Diagrams. - Magdalena Widl; Armin Biere; Petra Brosch; Uwe Egly; Marijn Heule; Gerti Kappel; Martina Seidl; Hans Tompits (SLE, 2012)

Simulating Circuit-Level Simplifications on CNF. - Matti Järvisalo; Armin Biere; Marijn Heule (J. Autom. Reason., 2012)

Verifying Refutations with Extended Resolution. - Marijn Heule; Warren A. Hunt Jr.; Nathan Wetzler (CADE, 2013)

Revisiting Hyper Binary Resolution. - Marijn Heule; Matti Järvisalo; Armin Biere (CPAIOR, 2013)

Trimming while checking clausal proofs. - Marijn Heule; Warren A. Hunt Jr.; Nathan Wetzler (FMCAD, 2013)

Mechanical Verification of SAT Refutations with Extended Resolution. - Nathan Wetzler; Marijn Heule; Warren A. Hunt Jr. (ITP, 2013)

Blocked Clause Decomposition. - Marijn Heule; Armin Biere (LPAR, 2013)

Symmetry in Gardens of Eden. - Christiaan Hartman; Marijn Heule; Kees Kwekkeboom; Alain Noels (Electron. J. Comb., 2013)

Software model synthesis using satisfiability solvers. - Marijn Heule; Sicco Verwer (Empir. Softw. Eng., 2013)

A Unified Proof System for QBF Preprocessing. - Marijn Heule; Martina Seidl; Armin Biere (IJCAR, 2014)

Efficient extraction of Skolem functions from QRAT proofs. - Marijn Heule; Martina Seidl; Armin Biere (FMCAD, 2014)

Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask). - Tomás Balyo; Andreas Fröhlich; Marijn Heule; Armin Biere (SAT, 2014)

MUS Extraction Using Clausal Proofs. - Anton Belov; Marijn Heule; João Marques-Silva 001 (SAT, 2014)

Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers. - Marijn Heule; Norbert Manthey; Tobias Philipp (POS@SAT, 2014)

DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. - Nathan Wetzler; Marijn Heule; Warren A. Hunt Jr. (SAT, 2014)

Towards Ultra Rapid Restarts. - Shai Haim; Marijn Heule (CoRR, 2014)

Symbiosis of Search and Heuristics for Random 3-SAT. - Sid Mijnders; Boris de Wilde; Marijn Heule (CoRR, 2014)

Concurrent Cube-and-Conquer. - Peter van der Tak; Marijn Heule; Armin Biere (CoRR, 2014)

Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. - Marijn Heule; Warren A. Hunt Jr.; Nathan Wetzler (Softw. Test. Verification Reliab., 2014)

What's Hot in the SAT and ASP Competitions. - Marijn Heule; Torsten Schaub (AAAI, 2015)

Expressing Symmetry Breaking in DRAT Proofs. - Marijn Heule; Warren A. Hunt Jr.; Nathan Wetzler (CADE, 2015)

Compositional Propositional Proofs. - Marijn J. H. Heule; Armin Biere (LPAR, 2015)

Clausal Proof Compression. - Marijn Heule; Armin Biere (IWIL@LPAR, 2015)

Blocked Literals Are Universal. - Marijn Heule; Martina Seidl; Armin Biere (NFM, 2015)

The Implication Problem of Computing Policies. - Rezwana Reaz; Muqeet Ali; Mohamed G. Gouda; Marijn Heule; Ehab S. Elmallah (SSS, 2015)

Clause Elimination for SAT and QSAT. - Marijn Heule; Matti Järvisalo; Florian Lonsing; Martina Seidl; Armin Biere (J. Artif. Intell. Res., 2015)

A SAT Approach to Clique-Width. - Marijn Heule; Stefan Szeider (ACM Trans. Comput. Log., 2015)

Computing Maximum Unavoidable Subgraphs Using SAT Solvers. - C. K. Cuong; M. J. H. Heule (SAT, 2016)

Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. - Marijn J. H. Heule; Oliver Kullmann; Victor W. Marek (SAT, 2016)

Analysis of Computing Policies Using SAT Solvers (Short Paper). - Marijn J. H. Heule; Rezwana Reaz; Hrishikesh B. Acharya; Mohamed G. Gouda (SSS, 2016)

The Quest for Perfect and Compact Symmetry Breaking for Graph Problems. - Marijn J. H. Heule (SYNASC, 2016)

The DRAT format and DRAT-trim checker. - Marijn J. H. Heule (CoRR, 2016)

SAT Competition 2016: Recent Developments. - Tomás Balyo; Marijn J. H. Heule; Matti Järvisalo (AAAI, 2017)

Efficient Certified RAT Verification. - Luís Cruz-Filipe; Marijn J. H. Heule; Warren A. Hunt Jr.; Matt Kaufmann; Peter Schneider-Kamp (CADE, 2017)

The Potential of Interference-Based Proof Systems. - Marijn Heule; Benjamin Kiesl (ARCADE@CADE, 2017)

Short Proofs Without New Variables. - Marijn J. H. Heule; Benjamin Kiesl; Armin Biere (CADE, 2017)

Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. - J Strother Moore; Marijn J. H. Heule (ARCADE@CADE, 2017)

Everything's Bigger in Texas: "The Largest Math Proof Ever". - Marijn Heule (GCAI, 2017)

PRuning Through Satisfaction. - Marijn J. H. Heule; Benjamin Kiesl; Martina Seidl; Armin Biere (Haifa Verification Conference, 2017)

Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method. - Marijn J. H. Heule; Oliver Kullmann; Victor W. Marek (IJCAI, 2017)

Efficient, Verified Checking of Propositional Proofs. - Marijn Heule; Warren A. Hunt Jr.; Matt Kaufmann; Nathan Wetzler (ITP, 2017)

A Little Blocked Literal Goes a Long Way. - Benjamin Kiesl; Marijn J. H. Heule; Martina Seidl (SAT, 2017)

Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions. - Valentin Wüstholz; Oswaldo Olivo; Marijn J. H. Heule; Isil Dillig (TACAS (2), 2017)

Skolem Function Continuation for Quantified Boolean Formulas. - Katalin Fazekas; Marijn J. H. Heule; Martina Seidl; Armin Biere (TAP@STAF, 2017)

The science of brute force. - Marijn J. H. Heule; Oliver Kullmann (Commun. ACM, 2017)

Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions (Extended Version). - Valentin Wüstholz; Oswaldo Olivo; Marijn J. H. Heule; Isil Dillig (CoRR, 2017)

Computing properties of stable configurations of thermodynamic binding networks. - Keenan Breik; Lakshmi Prakash; Chris Thachuk; Marijn Heule; David Soloveichik (CoRR, 2017)

Solution Validation and Extraction for QBF Preprocessing. - Marijn J. H. Heule; Martina Seidl; Armin Biere (J. Autom. Reason., 2017)

Cube-and-Conquer for Satisfiability. - Marijn J. H. Heule; Oliver Kullmann; Armin Biere (Handbook of Parallel Constraint Reasoning, 2018)

Schur Number Five. - Marijn J. H. Heule (AAAI, 2018)

Extended Resolution Simulates DRAT. - Benjamin Kiesl; Adrián Rebola-Pardo; Marijn J. H. Heule (IJCAR, 2018)

The Effect of Scrambling CNFs. - Armin Biere; Marijn Heule (POS@SAT, 2018)

What a Difference a Variable Makes. - Marijn J. H. Heule; Armin Biere (TACAS (2), 2018)

Truth Assignments as Conditional Autarkies. - Benjamin Kiesl; Marijn J. H. Heule; Armin Biere (ATVA, 2019)

Trimming Graphs Using Clausal Proof Optimization. - Marijn J. H. Heule (CP, 2019)

Clausal Proofs of Mutilated Chessboards. - Marijn J. H. Heule; Benjamin Kiesl; Armin Biere (NFM, 2019)

Local Search for Fast Matrix Multiplication. - Marijn J. H. Heule; Manuel Kauers; Martina Seidl (SAT, 2019)

Encoding Redundancy for Satisfaction-Driven Clause Learning. - Marijn J. H. Heule; Benjamin Kiesl; Armin Biere (TACAS (1), 2019)

A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications. - Marijn Heule; Manuel Kauers; Martina Seidl (ACM Commun. Comput. Algebra, 2019)

New ways to multiply 3 x 3-matrices. - Marijn J. H. Heule; Manuel Kauers; Martina Seidl (CoRR, 2019)

The Resolution of Keller's Conjecture. - Joshua Brakensiek; Marijn Heule; John Mackey (CoRR, 2019)

SAT Competition 2018. - Marijn J. H. Heule; Matti Järvisalo; Martin Suda 001 (J. Satisf. Boolean Model. Comput., 2019)

Optimal Symmetry Breaking for Graph Problems. - Marijn J. H. Heule (Math. Comput. Sci., 2019)

Computing properties of stable configurations of thermodynamic binding networks. - Keenan Breik; Chris Thachuk; Marijn Heule; David Soloveichik (Theor. Comput. Sci., 2019)

Constructing Minimal Perfect Hash Functions Using SAT Technology. - Sean A. Weaver; Marijn Heule (AAAI, 2020)

Modeling Techniques for Logic Locking. - Joseph Sweeney; Marijn J. H. Heule; Lawrence T. Pileggi (ICCAD, 2020)

Coloring Unit-Distance Strips using SAT. - Peter Oostema; Ruben Martins; Marijn Heule (LPAR, 2020)

Sensitivity Analysis of Locked Circuits. - Joseph Sweeney; Marijn Heule; Lawrence T. Pileggi (LPAR, 2020)

Sorting Parity Encodings by Reusing Variables. - Leroy Chew; Marijn J. H. Heule (SAT, 2020)

Mycielski Graphs and PR Proofs. - Emre Yolcu; Xinyu Wu; Marijn J. H. Heule (SAT, 2020)

Strong Extension-Free Proof Systems. - Marijn J. H. Heule; Benjamin Kiesl; Armin Biere (J. Autom. Reason., 2020)

Simulating Strong Practical Proof Systems with Extended Resolution. - Benjamin Kiesl; Adrián Rebola-Pardo; Marijn J. H. Heule; Armin Biere (J. Autom. Reason., 2020)

The Resolution of Keller's Conjecture - Computation Logs. - Joshua Brakensiek; Marijn Heule; John Mackey; David E. Narváez (Zenodo, 2020)

Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. - Randal E. Bryant; Marijn J. H. Heule (CADE, 2021)

Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. - Travis Hance; Marijn Heule; Ruben Martins; Bryan Parno (NSDI, 2021)

Chinese Remainder Encoding for Hamiltonian Cycles. - Marijn J. H. Heule (SAT, 2021)

XOR Local Search for Boolean Brent Equations. - Wojciech Nawrocki; Zhenjun Liu; Andreas Fröhlich; Marijn J. H. Heule; Armin Biere (SAT, 2021)

Avoiding Monochromatic Rectangles Using Shift Patterns. - Zhenjun Liu; Leroy Chew; Marijn J. H. Heule (SOCS, 2021)

cake_lpr: Verified Propagation Redundancy Checking in CakeML. - Yong Kiam Tan; Marijn J. H. Heule; Magnus O. Myreen (TACAS (2), 2021)

SAT Competition 2020. - Nils Froleyks; Marijn Heule; Markus Iser; Matti Järvisalo; Martin Suda 001 (Artif. Intell., 2021)

New ways to multiply 3 × 3-matrices. - Marijn J. H. Heule; Manuel Kauers; Martina Seidl (J. Symb. Comput., 2021)

Proofs of Unsatisfiability. - Marijn J. H. Heule (Handbook of Satisfiability, 2021)

Look-Ahead Based SAT Solvers. - Marijn J. H. Heule; Hans van Maaren (Handbook of Satisfiability, 2021)

SAT-Inspired Eliminations for Superposition. - Petar Vukmirovic; Jasmin Blanchette; Marijn J. H. Heule (Zenodo, 2021)

SAT-Inspired Eliminations for Superposition. - Petar Vukmirovic; Jasmin Blanchette; Marijn J. H. Heule (Zenodo, 2021)

From Cliques to Colorings and Back Again. - Marijn J. H. Heule; Anthony Karahalios; Willem-Jan van Hoeve (CP, 2022)

Compact Symmetry Breaking for Tournaments. - Evan Lohn; Chris Lambert; Marijn J. H. Heule (FMCAD, 2022)

A programmable, energy-minimal dataflow compiler and architecture. - Graham Gobieski; Souradip Ghosh; Marijn Heule; Todd C. Mowry; Tony Nowatzki; Nathan Beckmann; Brandon Lucia (MICRO, 2022)

Migrating Solver State. - Armin Biere; Md. Solimul Chowdhury; Marijn J. H. Heule; Benjamin Kiesl; Michael W. Whalen (SAT, 2022)

Relating Existing Powerful Proof Systems for QBF. - Leroy Chew; Marijn J. H. Heule (SAT, 2022)

The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. - Bernardo Subercaseaux; Marijn J. H. Heule (SAT, 2022)

Clausal Proofs for Pseudo-Boolean Reasoning. - Randal E. Bryant; Armin Biere; Marijn J. H. Heule (TACAS (1), 2022)

Moving Definition Variables in Quantified Boolean Formulas. - Joseph E. Reeves; Marijn J. H. Heule; Randal E. Bryant (TACAS (1), 2022)

Towards the shortest DRAT proof of the Pigeonhole Principle. - Isaac Grosof; Naifeng Zhang; Marijn J. H. Heule (CoRR, 2022)

Tighter Bounds on Directed Ramsey Number R(7). - David Neiman; John Mackey; Marijn Heule (Graphs Comb., 2022)

The Resolution of Keller's Conjecture. - Joshua Brakensiek; Marijn Heule; John Mackey; David E. Narváez (J. Autom. Reason., 2022)

A Flexible Proof Format for SAT Solver-Elaborator Communication. - Seulkee Baek; Mario Carneiro; Marijn J. H. Heule (Log. Methods Comput. Sci., 2022)

Verified Encodings for SAT Solvers. - Cayden R. Codel; Jeremy Avigad; Marijn J. H. Heule (FMCAD, 2023)

Mariposa: Measuring SMT Instability in Automated Program Verification. - Yi Zhou 025; Jay Bosamiya; Yoshiki Takashima; Jessica Li; Marijn Heule; Bryan Parno (FMCAD, 2023)

Without Loss of Satisfaction. - Marijn J. H. Heule (ICTAC, 2023)

Exponential Separations Using Guarded Extension Variables. - Emre Yolcu; Marijn J. H. Heule (ITCS, 2023)

Toward Optimal Radio Colorings of Hypercubes via SAT-solving. - Bernardo Subercaseaux; Marijn Heule (LPAR, 2023)

A Linear Weight Transfer Rule for Local Search. - Md. Solimul Chowdhury; Cayden R. Codel; Marijn J. H. Heule (NFM, 2023)

The SAT Museum. - Armin Biere; Mathias Fleury; Nils Froleyks; Marijn J. H. Heule (POS@SAT, 2023)

Certified Knowledge Compilation with Application to Verified Model Counting. - Randal E. Bryant; Wojciech Nawrocki; Jeremy Avigad; Marijn J. H. Heule (SAT, 2023)

Effective Auxiliary Variables via Structured Reencoding. - Andrew Haberlandt; Harrison Green; Marijn J. H. Heule (SAT, 2023)

Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers. - Dawn Michaelson; Dominik Schreiber 001; Marijn J. H. Heule; Benjamin Kiesl-Reiter; Michael W. Whalen (TACAS (1), 2023)

Propositional Proof Skeletons. - Joseph E. Reeves; Benjamin Kiesl-Reiter; Marijn J. H. Heule (TACAS (1), 2023)

The Packing Chromatic Number of the Infinite Square Grid is 15. - Bernardo Subercaseaux; Marijn J. H. Heule (TACAS (1), 2023)

What's in a Name? Linear Temporal Logic Literally Represents Time Lines. - Runming Li; Keerthana Gurushankar; Marijn J. H. Heule; Kristin Yvonne Rozier (VISSOFT, 2023)

Minimizing Pentagons in the Plane through Automated Reasoning. - Bernardo Subercaseaux; John Mackey; Marijn J. H. Heule; Ruben Martins (CoRR, 2023)

SAT Encodings and Beyond (Dagstuhl Seminar 23261). - Marijn J. H. Heule; Inês Lynce; Stefan Szeider; André Schidler (Dagstuhl Reports, 2023)

SAT-Inspired Eliminations for Superposition. - Petar Vukmirovic; Jasmin Blanchette; Marijn J. H. Heule (ACM Trans. Comput. Log., 2023)

Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML. - Yong Kiam Tan; Marijn J. H. Heule; Magnus O. Myreen (Int. J. Softw. Tools Technol. Transf., 2023)

An Impossible Asylum. - Jeremy Avigad; Seulkee Baek; Alexander Bentkamp; Marijn Heule; Wojciech Nawrocki (Am. Math. Mon., 2023)

An Automated Approach to the Collatz Conjecture. - Emre Yolcu; Scott Aaronson; Marijn J. H. Heule (J. Autom. Reason., 2023)

Preprocessing of Propagation Redundant Clauses. - Joseph E. Reeves; Marijn J. H. Heule; Randal E. Bryant (J. Autom. Reason., 2023)

The SAT Museum POS'23 Artifact. - Armin Biere; Mathias Fleury; Nils Froleyks; Marijn Heule (Zenodo, 2023)

Artifact for TaSSAT: A Stochastic Local Search Solver for SAT. - Md. Solimul Chowdhury; Cayden R. Codel; Marijn Heule (Zenodo, 2023)

Generating Extended Resolution Proofs with a BDD-Based SAT Solver. - Randal E. Bryant; Marijn J. H. Heule (ACM Trans. Comput. Log., 2023)

From Clauses to Klauses [inline-graphic not available: see fulltext]. - Joseph E. Reeves; Marijn J. H. Heule; Randal E. Bryant (CAV (1), 2024)

Verified Substitution Redundancy Checking. - Cayden R. Codel; Jeremy Avigad; Marijn J. H. Heule (FMCAD, 2024)

Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs. - Karthik V. Nukala; Soumyaditya Choudhuri; Randal E. Bryant; Marijn J. H. Heule (FMCAD, 2024)

Context Pruning for More Robust SMT-based Program Verification. - Yi Zhou 025; Jay Bosamiya; Jessica Li; Marijn J. H. Heule; Bryan Parno (FMCAD, 2024)

PackIt!: Gamified Rectangle Packing. - Thomas Garrison; Marijn J. H. Heule; Bernardo Subercaseaux (FUN, 2024)

Formal Verification of the Empty Hexagon Number. - Bernardo Subercaseaux; Wojciech Nawrocki; James Gallicchio; Cayden R. Codel; Mario Carneiro; Marijn J. H. Heule (ITP, 2024)

Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane. - Bernardo Subercaseaux; John Mackey; Marijn J. H. Heule; Ruben Martins (CICM, 2024)

Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving. - Jiong Yang 002; Yaroslav A. Kharkov; Yunong Shi; Marijn J. H. Heule; Bruno Dutertre (SAT, 2024)

TaSSAT: Transfer and Share SAT. - Md. Solimul Chowdhury; Cayden R. Codel; Marijn J. H. Heule (TACAS (1), 2024)

Happy Ending: An Empty Hexagon in Every Set of 30 Points. - Marijn J. H. Heule; Manfred Scheucher (TACAS (1), 2024)

EmptyHexagonLean. - Bernardo Subercaseaux; Wojciech Nawrocki; James Gallicchio; Cayden R. Codel; Mario Carneiro; Marijn J. H. Heule (DROPS Artifacts, 2024)

The Impact of Literal Sorting on Cardinality Constraint Encodings. - Joseph E. Reeves; João Filipe; Min-Chien Hsu; Ruben Martins; Marijn J. H. Heule (AAAI, 2025)

Unfolding Boxes with Local Constraints. - Long Qian; Eric Wang; Bernardo Subercaseaux; Marijn J. H. Heule (CADE, 2025)

Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification. - Yi Zhou 025; Amar Shah; Zhengyao Lin; Marijn Heule; Bryan Parno (CADE, 2025)

Problem Partitioning via Proof Prefixes. - Zachary Battleman; Joseph E. Reeves; Marijn J. H. Heule (SAT, 2025)

Certifying Projected Knowledge Compilation. - Randal E. Bryant; Yong Kiam Tan; Marijn J. H. Heule (SAT, 2025)

Reencoding Unique Literal Clauses. - Aeacus Sheng; Joseph E. Reeves; Marijn J. H. Heule (SAT, 2025)

Certified Knowledge Compilation with Application to Formally Verified Model Counting. - Randal E. Bryant; Wojciech Nawrocki; Jeremy Avigad; Marijn J. H. Heule (J. Artif. Intell. Res., 2025)

Automated Symmetric Constructions in Discrete Geometry. - Bernardo Subercaseaux; Ethan Mackey; Long Qian; Marijn J. H. Heule (CoRR, 2025)

Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers. - Dawn Michaelson; Dominik Schreiber 001; Marijn J. H. Heule; Benjamin Kiesl-Reiter; Michael W. Whalen (J. Autom. Reason., 2025)