Marijn J. H. Heule

116 papers A* 4A 27B 12C 3Misc 2Journal 42Unranked 21

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Automated Reencoding Meets Graph Theory. CoRR Benjamin Przybocki, Bernardo Subercaseaux, Marijn J. H. Heule
2026	—	`conf`	Orbitopal Fixing in SAT. TACAS (1) Markus Anders, Cayden R. Codel, Marijn J. H. Heule
2026	J	`jnl`	Orbitopal Fixing in SAT. CoRR Markus Anders, Cayden R. Codel, Marijn J. H. Heule
2025	J	`jnl`	Automated Symmetric Constructions in Discrete Geometry. CoRR Bernardo Subercaseaux, Ethan Mackey, Long Qian, Marijn J. H. Heule
2025	J	`jnl`	Certified Knowledge Compilation with Application to Formally Verified Model Counting. CoRR Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2025	J	`jnl`	Certified Knowledge Compilation with Application to Formally Verified Model Counting. J. Artif. Intell. Res. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2025	J	`jnl`	Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231). Dagstuhl Reports Nikolaj S. Bjørner, Marijn J. H. Heule, Daniela Kaufmann, Jakob Nordström, Wietze Koops
2025	A	`conf`	Certifying Projected Knowledge Compilation. SAT Randal E. Bryant, Yong Kiam Tan, Marijn J. H. Heule
2025	B	`conf`	Learning Short Clauses via Conditional Autarkies. FMCAD Amar Shah, Twain Byrnes, Joseph E. Reeves, Marijn J. H. Heule
2025	A	`conf`	Problem Partitioning via Proof Prefixes. SAT Zachary Battleman, Joseph E. Reeves, Marijn J. H. Heule
2025	J	`jnl`	Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers. J. Autom. Reason. Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen
2025	A	`conf`	Reencoding Unique Literal Clauses. SAT Aeacus Sheng, Joseph E. Reeves, Marijn J. H. Heule
2025	A*	`conf`	The Impact of Literal Sorting on Cardinality Constraint Encodings. AAAI Joseph E. Reeves, João Filipe, Min-Chien Hsu, Ruben Martins, Marijn J. H. Heule
2025	A	`conf`	Unfolding Boxes with Local Constraints. CADE Long Qian, Eric Wang, Bernardo Subercaseaux, Marijn J. H. Heule
2025	J	`jnl`	Unfolding Boxes with Local Constraints. CoRR Long Qian, Eric Wang, Bernardo Subercaseaux, Marijn J. H. Heule
2024	C	`conf`	Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane. CICM Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins
2024	—	`ed.`	Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I IJCAR (1) Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt
2024	—	`ed.`	Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II IJCAR (2) Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt
2024	B	`conf`	Context Pruning for More Robust SMT-based Program Verification. FMCAD Yi Zhou, Jay Bosamiya, Jessica Li, Marijn J. H. Heule, Bryan Parno
2024	B	`conf`	Formal Verification of the Empty Hexagon Number. ITP Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule
2024	J	`jnl`	Formal Verification of the Empty Hexagon Number. CoRR Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule
2024	—	`conf`	From Clauses to Klauses. CAV (1) Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
2024	—	`conf`	Happy Ending: An Empty Hexagon in Every Set of 30 Points. TACAS (1) Marijn J. H. Heule, Manfred Scheucher
2024	J	`jnl`	Happy Ending: An Empty Hexagon in Every Set of 30 Points. CoRR Marijn J. H. Heule, Manfred Scheucher
2024	J	`jnl`	PackIt! Gamified Rectangle Packing. CoRR Thomas Garrison, Marijn J. H. Heule, Bernardo Subercaseaux
2024	Misc	`conf`	PackIt!: Gamified Rectangle Packing. FUN Thomas Garrison, Marijn J. H. Heule, Bernardo Subercaseaux
2024	A	`conf`	Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving. SAT Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn J. H. Heule, Bruno Dutertre
2024	—	`conf`	TaSSAT: Transfer and Share SAT. TACAS (1) Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
2024	B	`conf`	Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs. FMCAD Karthik V. Nukala, Soumyaditya Choudhuri, Randal E. Bryant, Marijn J. H. Heule
2024	B	`conf`	Verified Substitution Redundancy Checking. FMCAD Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule
2023	—	`conf`	A Linear Weight Transfer Rule for Local Search. NFM Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
2023	J	`jnl`	A Linear Weight Transfer Rule for Local Search. CoRR Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
2023	J	`jnl`	An Automated Approach to the Collatz Conjecture. J. Autom. Reason. Emre Yolcu, Scott Aaronson, Marijn J. H. Heule
2023	A	`conf`	Certified Knowledge Compilation with Application to Verified Model Counting. SAT Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2023	A	`conf`	Effective Auxiliary Variables via Structured Reencoding. SAT Andrew Haberlandt, Harrison Green, Marijn J. H. Heule
2023	J	`jnl`	Effective Auxiliary Variables via Structured Reencoding. CoRR Andrew Haberlandt, Harrison Green, Marijn J. H. Heule
2023	A	`conf`	Exponential Separations Using Guarded Extension Variables. ITCS Emre Yolcu, Marijn J. H. Heule
2023	J	`jnl`	Generating Extended Resolution Proofs with a BDD-Based SAT Solver. ACM Trans. Comput. Log. Randal E. Bryant, Marijn J. H. Heule
2023	J	`jnl`	Minimizing Pentagons in the Plane through Automated Reasoning. CoRR Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins
2023	J	`jnl`	Preprocessing of Propagation Redundant Clauses. J. Autom. Reason. Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
2023	—	`conf`	Propositional Proof Skeletons. TACAS (1) Joseph E. Reeves, Benjamin Kiesl-Reiter, Marijn J. H. Heule
2023	J	`jnl`	SAT Encodings and Beyond (Dagstuhl Seminar 23261). Dagstuhl Reports Marijn J. H. Heule, Inês Lynce, Stefan Szeider, André Schidler
2023	J	`jnl`	SAT-Inspired Eliminations for Superposition. ACM Trans. Comput. Log. Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule
2023	—	`conf`	The Packing Chromatic Number of the Infinite Square Grid is 15. TACAS (1) Bernardo Subercaseaux, Marijn J. H. Heule
2023	J	`jnl`	The Packing Chromatic Number of the Infinite Square Grid is 15. CoRR Bernardo Subercaseaux, Marijn J. H. Heule
2023	—	`conf`	The SAT Museum. POS@SAT Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule
2023	—	`conf`	Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers. TACAS (1) Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen
2023	B	`conf`	Verified Encodings for SAT Solvers. FMCAD Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule
2023	J	`jnl`	Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML. Int. J. Softw. Tools Technol. Transf. Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen
2023	B	`conf`	What's in a Name? Linear Temporal Logic Literally Represents Time Lines. VISSOFT Runming Li, Keerthana Gurushankar, Marijn J. H. Heule, Kristin Yvonne Rozier
2023	C	`conf`	Without Loss of Satisfaction. ICTAC Marijn J. H. Heule
2022	J	`jnl`	A Flexible Proof Format for SAT Solver-Elaborator Communication. Log. Methods Comput. Sci. Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
2022	—	`conf`	Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) Randal E. Bryant, Armin Biere, Marijn J. H. Heule
2022	B	`conf`	Compact Symmetry Breaking for Tournaments. FMCAD Evan Lohn, Chris Lambert, Marijn J. H. Heule
2022	J	`jnl`	Exponential separations using guarded extension variables. CoRR Emre Yolcu, Marijn J. H. Heule
2022	A	`conf`	From Cliques to Colorings and Back Again. CP Marijn J. H. Heule, Anthony Karahalios, Willem-Jan van Hoeve
2022	A	`conf`	Migrating Solver State. SAT Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen
2022	—	`conf`	Moving Definition Variables in Quantified Boolean Formulas. TACAS (1) Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
2022	A	`conf`	Preprocessing of Propagation Redundant Clauses. IJCAR Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant
2022	A	`conf`	Relating Existing Powerful Proof Systems for QBF. SAT Leroy Chew, Marijn J. H. Heule
2022	A	`conf`	The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. SAT Bernardo Subercaseaux, Marijn J. H. Heule
2022	J	`jnl`	Towards the shortest DRAT proof of the Pigeonhole Principle. CoRR Isaac Grosof, Naifeng Zhang, Marijn J. H. Heule
2021	—	`conf`	A Flexible Proof Format for SAT Solver-Elaborator Communication. TACAS (1) Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
2021	J	`jnl`	A Flexible Proof Format for SAT Solver-Elaborator Communication. CoRR Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
2021	A	`conf`	An Automated Approach to the Collatz Conjecture. CADE Emre Yolcu, Scott Aaronson, Marijn J. H. Heule
2021	J	`jnl`	An Automated Approach to the Collatz Conjecture. CoRR Emre Yolcu, Scott Aaronson, Marijn J. H. Heule
2021	B	`conf`	Avoiding Monochromatic Rectangles Using Shift Patterns. SOCS Zhenjun Liu, Leroy Chew, Marijn J. H. Heule
2021	A	`conf`	Chinese Remainder Encoding for Hamiltonian Cycles. SAT Marijn J. H. Heule
2021	A	`conf`	Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. CADE Randal E. Bryant, Marijn J. H. Heule
2021	—	`conf`	Generating Extended Resolution Proofs with a BDD-Based SAT Solver. TACAS (1) Randal E. Bryant, Marijn J. H. Heule
2021	J	`jnl`	Generating Extended Resolution Proofs with a BDD-Based SAT Solver. CoRR Randal E. Bryant, Marijn J. H. Heule
2021	—	`ch.`	Look-Ahead Based SAT Solvers. Handbook of Satisfiability Marijn J. H. Heule, Hans van Maaren
2021	J	`jnl`	New ways to multiply 3 × 3-matrices. J. Symb. Comput. Marijn J. H. Heule, Manuel Kauers, Martina Seidl
2021	—	`ch.`	Proofs of Unsatisfiability. Handbook of Satisfiability Marijn J. H. Heule
2021	B	`conf`	SAT-Inspired Eliminations for Superposition. FMCAD Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule
2021	A	`conf`	XOR Local Search for Boolean Brent Equations. SAT Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J. H. Heule, Armin Biere
2021	—	`conf`	cake_lpr: Verified Propagation Redundancy Checking in CakeML. TACAS (2) Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen
2020	A	`conf`	Modeling Techniques for Logic Locking. ICCAD Joseph Sweeney, Marijn J. H. Heule, Lawrence T. Pileggi
2020	J	`jnl`	Modeling Techniques for Logic Locking. CoRR Joseph Sweeney, Marijn J. H. Heule, Lawrence T. Pileggi
2020	A	`conf`	Mycielski Graphs and PR Proofs. SAT Emre Yolcu, Xinyu Wu, Marijn J. H. Heule
2020	J	`jnl`	Simulating Strong Practical Proof Systems with Extended Resolution. J. Autom. Reason. Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, Armin Biere
2020	A	`conf`	Sorting Parity Encodings by Reusing Variables. SAT Leroy Chew, Marijn J. H. Heule
2020	J	`jnl`	Strong Extension-Free Proof Systems. J. Autom. Reason. Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
2019	—	`conf`	Clausal Proofs of Mutilated Chessboards. NFM Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
2019	—	`conf`	Encoding Redundancy for Satisfaction-Driven Clause Learning. TACAS (1) Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
2019	A	`conf`	Local Search for Fast Matrix Multiplication. SAT Marijn J. H. Heule, Manuel Kauers, Martina Seidl
2019	J	`jnl`	Local Search for Fast Matrix Multiplication. CoRR Marijn J. H. Heule, Manuel Kauers, Martina Seidl
2019	J	`jnl`	New ways to multiply 3 x 3-matrices. CoRR Marijn J. H. Heule, Manuel Kauers, Martina Seidl
2019	J	`jnl`	Optimal Symmetry Breaking for Graph Problems. Math. Comput. Sci. Marijn J. H. Heule
2019	J	`jnl`	SAT Competition 2018. J. Satisf. Boolean Model. Comput. Marijn J. H. Heule, Matti Järvisalo, Martin Suda
2019	A	`conf`	Trimming Graphs Using Clausal Proof Optimization. CP Marijn J. H. Heule
2019	J	`jnl`	Trimming Graphs Using Clausal Proof Optimization. CoRR Marijn J. H. Heule
2019	B	`conf`	Truth Assignments as Conditional Autarkies. ATVA Benjamin Kiesl, Marijn J. H. Heule, Armin Biere
2018	—	`ch.`	Cube-and-Conquer for Satisfiability. Handbook of Parallel Constraint Reasoning Marijn J. H. Heule, Oliver Kullmann, Armin Biere
2018	A	`conf`	Extended Resolution Simulates DRAT. IJCAR Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule
2018	A*	`conf`	Schur Number Five. AAAI Marijn J. H. Heule
2018	—	`conf`	What a Difference a Variable Makes. TACAS (2) Marijn J. H. Heule, Armin Biere
2017	A	`conf`	A Little Blocked Literal Goes a Long Way. SAT Benjamin Kiesl, Marijn J. H. Heule, Martina Seidl
2017	A	`conf`	Efficient Certified RAT Verification. CADE Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
2017	—	`conf`	Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. ARCADE@CADE J Strother Moore, Marijn J. H. Heule
2017	—	`conf`	PRuning Through Satisfaction. Haifa Verification Conference Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, Armin Biere
2017	A*	`conf`	SAT Competition 2016: Recent Developments. AAAI Tomás Balyo, Marijn J. H. Heule, Matti Järvisalo
2017	J	`jnl`	Schur Number Five. CoRR Marijn J. H. Heule
2017	A	`conf`	Short Proofs Without New Variables. CADE Marijn J. H. Heule, Benjamin Kiesl, Armin Biere
2017	—	`conf`	Skolem Function Continuation for Quantified Boolean Formulas. TAP@STAF Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere
2017	J	`jnl`	Solution Validation and Extraction for QBF Preprocessing. J. Autom. Reason. Marijn J. H. Heule, Martina Seidl, Armin Biere
2017	A*	`conf`	Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method. IJCAI Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek
2017	—	`conf`	Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions. TACAS (2) Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule, Isil Dillig
2017	J	`jnl`	Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions (Extended Version). CoRR Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule, Isil Dillig
2017	J	`jnl`	The science of brute force. Commun. ACM Marijn J. H. Heule, Oliver Kullmann
2016	C	`conf`	Analysis of Computing Policies Using SAT Solvers (Short Paper). SSS Marijn J. H. Heule, Rezwana Reaz, Hrishikesh B. Acharya, Mohamed G. Gouda
2016	A	`conf`	Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. SAT Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek
2016	J	`jnl`	Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. CoRR Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek
2016	J	`jnl`	The DRAT format and DRAT-trim checker. CoRR Marijn J. H. Heule
2016	Misc	`conf`	The Quest for Perfect and Compact Symmetry Breaking for Graph Problems. SYNASC Marijn J. H. Heule
2015	B	`conf`	Compositional Propositional Proofs. LPAR Marijn J. H. Heule, Armin Biere