Marijn J. H. Heule

Publication Activity (10 Years)

Years Active: 2015-2024
Publications (10 Years): 91

Top Topics

Boolean Formula

Top Venues

J. Autom. Reason.

Publications

Thomas Garrison, Marijn J. H. Heule, Bernardo Subercaseaux
PackIt! Gamified Rectangle Packing. CoRR (2024)
Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
TaSSAT: Transfer and Share SAT. TACAS (1) (2024)
Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule
Formal Verification of the Empty Hexagon Number. CoRR (2024)
Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
From Clauses to Klauses [inline-graphic not available: see fulltext]. CAV (1) (2024)
Marijn J. H. Heule, Manfred Scheucher
Happy Ending: An Empty Hexagon in Every Set of 30 Points. TACAS (1) (2024)
Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn J. H. Heule, Bruno Dutertre
Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving. SAT (2024)
Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane. CICM (2024)
Marijn J. H. Heule, Manfred Scheucher
Happy Ending: An Empty Hexagon in Every Set of 30 Points. CoRR (2024)
Thomas Garrison, Marijn J. H. Heule, Bernardo Subercaseaux
PackIt!: Gamified Rectangle Packing. FUN (2024)
Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule
SAT-Inspired Eliminations for Superposition. ACM Trans. Comput. Log. 24 (1) (2023)
Bernardo Subercaseaux, Marijn J. H. Heule
The Packing Chromatic Number of the Infinite Square Grid is 15. TACAS (1) (2023)
Runming Li, Keerthana Gurushankar, Marijn J. H. Heule, Kristin Yvonne Rozier
What's in a Name? Linear Temporal Logic Literally Represents Time Lines. VISSOFT (2023)
Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins
Minimizing Pentagons in the Plane through Automated Reasoning. CoRR (2023)
Emre Yolcu, Marijn J. H. Heule
Exponential Separations Using Guarded Extension Variables. ITCS (2023)
Bernardo Subercaseaux, Marijn J. H. Heule
The Packing Chromatic Number of the Infinite Square Grid is 15. CoRR (2023)
Joseph E. Reeves, Benjamin Kiesl-Reiter, Marijn J. H. Heule
Propositional Proof Skeletons. TACAS (1) (2023)
Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers. TACAS (1) (2023)
Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML. Int. J. Softw. Tools Technol. Transf. 25 (2) (2023)
Marijn J. H. Heule, Inês Lynce, Stefan Szeider, André Schidler
SAT Encodings and Beyond (Dagstuhl Seminar 23261). Dagstuhl Reports 13 (6) (2023)
Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule
Verified Encodings for SAT Solvers. FMCAD (2023)
Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
Certified Knowledge Compilation with Application to Verified Model Counting. SAT (2023)
Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
A Linear Weight Transfer Rule for Local Search. NFM (2023)
Andrew Haberlandt, Harrison Green, Marijn J. H. Heule
Effective Auxiliary Variables via Structured Reencoding. SAT (2023)
Emre Yolcu, Scott Aaronson, Marijn J. H. Heule
An Automated Approach to the Collatz Conjecture. J. Autom. Reason. 67 (2) (2023)
Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
A Linear Weight Transfer Rule for Local Search. CoRR (2023)
Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule
The SAT Museum. POS@SAT (2023)
Randal E. Bryant, Marijn J. H. Heule
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. ACM Trans. Comput. Log. 24 (4) (2023)
Marijn J. H. Heule
Without Loss of Satisfaction. ICTAC (2023)
Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
Preprocessing of Propagation Redundant Clauses. J. Autom. Reason. 67 (3) (2023)
Andrew Haberlandt, Harrison Green, Marijn J. H. Heule
Effective Auxiliary Variables via Structured Reencoding. CoRR (2023)
Leroy Chew, Marijn J. H. Heule
Relating Existing Powerful Proof Systems for QBF. SAT (2022)
Evan Lohn, Chris Lambert, Marijn J. H. Heule
Compact Symmetry Breaking for Tournaments. FMCAD (2022)
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
A Flexible Proof Format for SAT Solver-Elaborator Communication. Log. Methods Comput. Sci. 18 (2) (2022)
Marijn J. H. Heule, Anthony Karahalios, Willem-Jan van Hoeve
From Cliques to Colorings and Back Again. CP (2022)
Bernardo Subercaseaux, Marijn J. H. Heule
The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. SAT (2022)
Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
Preprocessing of Propagation Redundant Clauses. IJCAR (2022)
Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
Moving Definition Variables in Quantified Boolean Formulas. TACAS (1) (2022)
Isaac Grosof, Naifeng Zhang, Marijn J. H. Heule
Towards the shortest DRAT proof of the Pigeonhole Principle. CoRR (2022)
Randal E. Bryant, Armin Biere, Marijn J. H. Heule
Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) (2022)
Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen
Migrating Solver State. SAT (2022)
Emre Yolcu, Marijn J. H. Heule
Exponential separations using guarded extension variables. CoRR (2022)
Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J. H. Heule, Armin Biere
XOR Local Search for Boolean Brent Equations. SAT (2021)
Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule
SAT-Inspired Eliminations for Superposition. FMCAD (2021)
Emre Yolcu, Scott Aaronson, Marijn J. H. Heule
An Automated Approach to the Collatz Conjecture. CoRR (2021)
Marijn J. H. Heule, Manuel Kauers, Martina Seidl
New ways to multiply 3 × 3-matrices. J. Symb. Comput. 104 (2021)
Randal E. Bryant, Marijn J. H. Heule
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. CoRR (2021)
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
A Flexible Proof Format for SAT Solver-Elaborator Communication. TACAS (1) (2021)
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
A Flexible Proof Format for SAT Solver-Elaborator Communication. CoRR (2021)
Zhenjun Liu, Leroy Chew, Marijn J. H. Heule
Avoiding Monochromatic Rectangles Using Shift Patterns. SOCS (2021)
Randal E. Bryant, Marijn J. H. Heule
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. CADE (2021)
Marijn J. H. Heule
Chinese Remainder Encoding for Hamiltonian Cycles. SAT (2021)
Emre Yolcu, Scott Aaronson, Marijn J. H. Heule
An Automated Approach to the Collatz Conjecture. CADE (2021)
Randal E. Bryant, Marijn J. H. Heule
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. TACAS (1) (2021)
Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen
cake_lpr: Verified Propagation Redundancy Checking in CakeML. TACAS (2) (2021)
Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, Armin Biere
Simulating Strong Practical Proof Systems with Extended Resolution. J. Autom. Reason. 64 (7) (2020)
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Strong Extension-Free Proof Systems. J. Autom. Reason. 64 (3) (2020)
Leroy Chew, Marijn J. H. Heule
Sorting Parity Encodings by Reusing Variables. SAT (2020)
Emre Yolcu, Xinyu Wu, Marijn J. H. Heule
Mycielski Graphs and PR Proofs. SAT (2020)
Joseph Sweeney, Marijn J. H. Heule, Lawrence T. Pileggi
Modeling Techniques for Logic Locking. CoRR (2020)
Joseph Sweeney, Marijn J. H. Heule, Lawrence T. Pileggi
Modeling Techniques for Logic Locking. ICCAD (2020)
Marijn J. H. Heule, Manuel Kauers, Martina Seidl
Local Search for Fast Matrix Multiplication. CoRR (2019)
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Encoding Redundancy for Satisfaction-Driven Clause Learning. TACAS (1) (2019)
Marijn J. H. Heule, Manuel Kauers, Martina Seidl
New ways to multiply 3 x 3-matrices. CoRR (2019)
Marijn J. H. Heule
Optimal Symmetry Breaking for Graph Problems. Math. Comput. Sci. 13 (4) (2019)
Benjamin Kiesl, Marijn J. H. Heule, Armin Biere
Truth Assignments as Conditional Autarkies. ATVA (2019)
Marijn J. H. Heule, Manuel Kauers, Martina Seidl
Local Search for Fast Matrix Multiplication. SAT (2019)
Marijn J. H. Heule, Matti Järvisalo, Martin Suda
SAT Competition 2018. J. Satisf. Boolean Model. Comput. 11 (1) (2019)
Marijn J. H. Heule
Trimming Graphs Using Clausal Proof Optimization. CP (2019)
Marijn J. H. Heule
Trimming Graphs Using Clausal Proof Optimization. CoRR (2019)
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Clausal Proofs of Mutilated Chessboards. NFM (2019)
Marijn J. H. Heule, Armin Biere
What a Difference a Variable Makes. TACAS (2) (2018)
Marijn J. H. Heule
Schur Number Five. AAAI (2018)
Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule
Extended Resolution Simulates DRAT. IJCAR (2018)
Benjamin Kiesl, Marijn J. H. Heule, Martina Seidl
A Little Blocked Literal Goes a Long Way. SAT (2017)
Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek
Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method. IJCAI (2017)
Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
Short Proofs Without New Variables. CADE (2017)
Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule, Isil Dillig
Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions. TACAS (2) (2017)
Tomás Balyo, Marijn J. H. Heule, Matti Järvisalo
SAT Competition 2016: Recent Developments. AAAI (2017)
J. Strother Moore, Marijn J. H. Heule
Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. ARCADE@CADE (2017)
Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, Armin Biere
PRuning Through Satisfaction. Haifa Verification Conference (2017)
Marijn J. H. Heule, Oliver Kullmann
The science of brute force. Commun. ACM 60 (8) (2017)
Marijn J. H. Heule, Martina Seidl, Armin Biere
Solution Validation and Extraction for QBF Preprocessing. J. Autom. Reason. 58 (1) (2017)
Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
Efficient Certified RAT Verification. CADE (2017)
Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere
Skolem Function Continuation for Quantified Boolean Formulas. TAP@STAF (2017)
Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule, Isil Dillig
Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions (Extended Version). CoRR (2017)
Marijn J. H. Heule
Schur Number Five. CoRR (2017)
Marijn J. H. Heule, Rezwana Reaz, Hrishikesh B. Acharya, Mohamed G. Gouda
Analysis of Computing Policies Using SAT Solvers (Short Paper). SSS (2016)
Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. CoRR (2016)
Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. SAT (2016)
Marijn J. H. Heule
The Quest for Perfect and Compact Symmetry Breaking for Graph Problems. SYNASC (2016)
Marijn J. H. Heule
The DRAT format and DRAT-trim checker. CoRR (2016)
Marijn J. H. Heule, Armin Biere
Compositional Propositional Proofs. LPAR (2015)