Marijn J. H. Heule
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
70
Venues
20
Active years
2015–2026
Best venue rank
A*
Where they publish
Papers
70 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | IJCAR | Tao's Equational Proof Challenge Accepted. | Lydia Kondylidou, Jasmin Blanchette, Marijn J. H. Heule |
| 2026 | IJCAR | A General Approach for SMT Proof Skeletons. | Joseph E. Reeves, Haniel Barbosa, Andrew Reynolds, Marijn J. H. Heule |
| 2026 | ITP | An End-To-End Verification of Keller's Conjecture. | James Gallicchio, Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2026 | SAT | Simplify, Order, Break, Repeat. | Markus Anders, Cayden R. Codel, Marijn J. H. Heule |
| 2026 | SAT | Factoring Learned Clauses. | Florian Pollitt, Zachary Battleman, Mathias Fleury, Yakir Vizel, Marijn J. H. Heule, Armin Biere, Randal E. Bryant |
| 2026 | SAT | Automated Reencoding Meets Graph Theory. | Benjamin Przybocki, Bernardo Subercaseaux, Marijn J. H. Heule |
| 2026 | TACAS | Orbitopal Fixing in SAT. | Markus Anders, Cayden R. Codel, Marijn J. H. Heule |
| 2025 | AAAI | The Impact of Literal Sorting on Cardinality Constraint Encodings. | Joseph E. Reeves, Joo Filipe, Min-Chien Hsu, Ruben Martins, Marijn J. H. Heule |
| 2025 | CADE | Unfolding Boxes with Local Constraints. | Long Qian, Eric Wang, Bernardo Subercaseaux, Marijn J. H. Heule |
| 2025 | FMCAD | Learning Short Clauses via Conditional Autarkies. | Amar Shah, Twain Byrnes, Joseph E. Reeves, Marijn J. H. Heule |
| 2025 | SAT | Problem Partitioning via Proof Prefixes. | Zachary Battleman, Joseph E. Reeves, Marijn J. H. Heule |
| 2025 | SAT | Certifying Projected Knowledge Compilation. | Randal E. Bryant, Yong Kiam Tan, Marijn J. H. Heule |
| 2025 | SAT | Reencoding Unique Literal Clauses. | Aeacus Sheng, Joseph E. Reeves, Marijn J. H. Heule |
| 2024 | CAV | From Clauses to Klauses. | Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant |
| 2024 | FMCAD | Verified Substitution Redundancy Checking. | Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2024 | FMCAD | Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs. | Karthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J. H. Heule |
| 2024 | FMCAD | Context Pruning for More Robust SMT-based Program Verification. | Yi Zhou, Jay Bosamiya, Jessica Li, Marijn J. H. Heule, Bryan Parno |
| 2024 | FUN | PackIt!: Gamified Rectangle Packing. | Thomas Garrison, Marijn J. H. Heule, Bernardo Subercaseaux |
| 2024 | ITP | Formal Verification of the Empty Hexagon Number. | Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule |
| 2024 | SAT | Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving. | Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn J. H. Heule, Bruno Dutertre |
| 2024 | TACAS | TaSSAT: Transfer and Share SAT. | Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule |
| 2024 | TACAS | Happy Ending: An Empty Hexagon in Every Set of 30 Points. | Marijn J. H. Heule, Manfred Scheucher |
| 2023 | FMCAD | Verified Encodings for SAT Solvers. | Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2023 | ICTAC | Without Loss of Satisfaction. | Marijn J. H. Heule |
| 2023 | SAT | The SAT Museum. | Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule |
| 2023 | SAT | Certified Knowledge Compilation with Application to Verified Model Counting. | Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule |
| 2023 | SAT | Effective Auxiliary Variables via Structured Reencoding. | Andrew Haberlandt, Harrison Green, Marijn J. H. Heule |
| 2023 | TACAS | Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers. | Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen |
| 2023 | TACAS | Propositional Proof Skeletons. | Joseph E. Reeves, Benjamin Kiesl-Reiter, Marijn J. H. Heule |
| 2023 | TACAS | The Packing Chromatic Number of the Infinite Square Grid is 15. | Bernardo Subercaseaux, Marijn J. H. Heule |
| 2023 | VISSOFT | What's in a Name? Linear Temporal Logic Literally Represents Time Lines. | Runming Li, Keerthana Gurushankar, Marijn J. H. Heule, Kristin Yvonne Rozier |
| 2022 | CADE | Preprocessing of Propagation Redundant Clauses. | Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant |
| 2022 | CP | From Cliques to Colorings and Back Again. | Marijn J. H. Heule, Anthony Karahalios, Willem-Jan van Hoeve |
| 2022 | FMCAD | Compact Symmetry Breaking for Tournaments. | Evan Lohn, Chris Lambert, Marijn J. H. Heule |
| 2022 | SAT | Migrating Solver State. | Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen |
| 2022 | SAT | Relating Existing Powerful Proof Systems for QBF. | Leroy Chew, Marijn J. H. Heule |
| 2022 | SAT | The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. | Bernardo Subercaseaux, Marijn J. H. Heule |
| 2022 | TACAS | Clausal Proofs for Pseudo-Boolean Reasoning. | Randal E. Bryant, Armin Biere, Marijn J. H. Heule |
| 2022 | TACAS | Moving Definition Variables in Quantified Boolean Formulas. | Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant |
| 2021 | CADE | Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. | Randal E. Bryant, Marijn J. H. Heule |
| 2021 | CADE | An Automated Approach to the Collatz Conjecture. | Emre Yolcu, Scott Aaronson, Marijn J. H. Heule |
| 2021 | FMCAD | SAT-Inspired Eliminations for Superposition. | Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule |
| 2021 | SAT | Chinese Remainder Encoding for Hamiltonian Cycles. | Marijn J. H. Heule |
| 2021 | SAT | XOR Local Search for Boolean Brent Equations. | Wojciech Nawrocki, Zhenjun Liu, Andreas Frhlich, Marijn J. H. Heule, Armin Biere |
| 2021 | SoCS | Avoiding Monochromatic Rectangles Using Shift Patterns. | Zhenjun Liu, Leroy Chew, Marijn J. H. Heule |
| 2021 | TACAS | A Flexible Proof Format for SAT Solver-Elaborator Communication. | Seulkee Baek, Mario Carneiro, Marijn J. H. Heule |
| 2021 | TACAS | Generating Extended Resolution Proofs with a BDD-Based SAT Solver. | Randal E. Bryant, Marijn J. H. Heule |
| 2021 | TACAS | cake_lpr: Verified Propagation Redundancy Checking in CakeML. | Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen |
| 2020 | ICCAD | Modeling Techniques for Logic Locking. | Joseph Sweeney, Marijn J. H. Heule, Lawrence T. Pileggi |
| 2020 | SAT | Sorting Parity Encodings by Reusing Variables. | Leroy Chew, Marijn J. H. Heule |
| 2020 | SAT | Mycielski Graphs and PR Proofs. | Emre Yolcu, Xinyu Wu, Marijn J. H. Heule |
| 2019 | ATVA | Truth Assignments as Conditional Autarkies. | Benjamin Kiesl, Marijn J. H. Heule, Armin Biere |
| 2019 | CP | Trimming Graphs Using Clausal Proof Optimization. | Marijn J. H. Heule |
| 2019 | SAT | Local Search for Fast Matrix Multiplication. | Marijn J. H. Heule, Manuel Kauers, Martina Seidl |
| 2019 | TACAS | Encoding Redundancy for Satisfaction-Driven Clause Learning. | Marijn J. H. Heule, Benjamin Kiesl, Armin Biere |
| 2018 | AAAI | Schur Number Five. | Marijn J. H. Heule |
| 2018 | CADE | Extended Resolution Simulates DRAT. | Benjamin Kiesl, Adrin Rebola-Pardo, Marijn J. H. Heule |
| 2018 | TACAS | What a Difference a Variable Makes. | Marijn J. H. Heule, Armin Biere |
| 2017 | AAAI | SAT Competition 2016: Recent Developments. | Toms Balyo, Marijn J. H. Heule, Matti Jrvisalo |
| 2017 | CADE | Efficient Certified RAT Verification. | Lus Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp |
| 2017 | CADE | Short Proofs Without New Variables. | Marijn J. H. Heule, Benjamin Kiesl, Armin Biere |
| 2017 | CADE | Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. | J Strother Moore, Marijn J. H. Heule |
| 2017 | IJCAI | Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method. | Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek |
| 2017 | SAT | A Little Blocked Literal Goes a Long Way. | Benjamin Kiesl, Marijn J. H. Heule, Martina Seidl |
| 2017 | TACAS | Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions. | Valentin Wstholz, Oswaldo Olivo, Marijn J. H. Heule, Isil Dillig |
| 2017 | TAP | Skolem Function Continuation for Quantified Boolean Formulas. | Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere |
| 2016 | SAT | Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. | Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek |
| 2016 | SSS | Analysis of Computing Policies Using SAT Solvers (Short Paper). | Marijn J. H. Heule, Rezwana Reaz, Hrishikesh B. Acharya, Mohamed G. Gouda |
| 2016 | SYNASC | The Quest for Perfect and Compact Symmetry Breaking for Graph Problems. | Marijn J. H. Heule |
| 2015 | LPAR | Compositional Propositional Proofs. | Marijn J. H. Heule, Armin Biere |