default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMarijn Heule
Marijn J. H. Heule – M. J. H. Heule
Person information
- affiliation: Carnegie Mellon University, Pittsburgh, PA, USA
- affiliation (former): University of Texas at Austin, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
Books and Theses
- 2008
[b1]M. J. H. Heule:
SmArT solving: tools and techniques for satisfiability solvers. Delft University of Technology, Netherlands, 2008
Journal Articles
- 2023
- [j33]Emre Yolcu
, Scott Aaronson, Marijn J. H. Heule:
An Automated Approach to the Collatz Conjecture. J. Autom. Reason. 67(2): 15 (2023) - [j32]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Preprocessing of Propagation Redundant Clauses. J. Autom. Reason. 67(3): 31 (2023) - [j31]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): 167-184 (2023) - [j30]Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki:
An Impossible Asylum. Am. Math. Mon. 130(5): 446-453 (2023) - [j29]Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. ACM Trans. Comput. Log. 24(1): 7:1-7:25 (2023) - [j28]Randal E. Bryant, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. ACM Trans. Comput. Log. 24(4): 31:1-31:28 (2023) - 2022
- [j27]David Neiman, John Mackey, Marijn Heule:
Tighter Bounds on Directed Ramsey Number R(7). Graphs Comb. 38(5): 156 (2022) - [j26]Joshua Brakensiek, Marijn Heule, John Mackey, David E. Narváez:
The Resolution of Keller's Conjecture. J. Autom. Reason. 66(3): 277-300 (2022) - [j25]Seulkee Baek, Mario Carneiro, Marijn J. H. Heule:
A Flexible Proof Format for SAT Solver-Elaborator Communication. Log. Methods Comput. Sci. 18(2) (2022) - 2021
- [j24]Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda:
SAT Competition 2020. Artif. Intell. 301: 103572 (2021) - [j23]Marijn J. H. Heule, Manuel Kauers, Martina Seidl:
New ways to multiply 3 × 3-matrices. J. Symb. Comput. 104: 899-916 (2021) - 2020
- [j22]Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Strong Extension-Free Proof Systems. J. Autom. Reason. 64(3): 533-554 (2020) - [j21]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): 1247-1267 (2020) - 2019
- [j20]Marijn Heule, Manuel Kauers, Martina Seidl:
A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications. ACM Commun. Comput. Algebra 53(3): 118-121 (2019) - [j19]Marijn J. H. Heule, Matti Järvisalo, Martin Suda:
SAT Competition 2018. J. Satisf. Boolean Model. Comput. 11(1): 133-154 (2019) - [j18]Marijn J. H. Heule:
Optimal Symmetry Breaking for Graph Problems. Math. Comput. Sci. 13(4): 533-548 (2019) - [j17]Keenan Breik, Chris Thachuk, Marijn Heule, David Soloveichik:
Computing properties of stable configurations of thermodynamic binding networks. Theor. Comput. Sci. 785: 17-29 (2019) - 2017
- [j16]Marijn J. H. Heule, Oliver Kullmann:
The science of brute force. Commun. ACM 60(8): 70-79 (2017) - [j15]Marijn J. H. Heule, Martina Seidl, Armin Biere:
Solution Validation and Extraction for QBF Preprocessing. J. Autom. Reason. 58(1): 97-125 (2017) - 2015
- [j14]Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere:
Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. 53: 127-168 (2015) - [j13]Marijn Heule, Stefan Szeider:
A SAT Approach to Clique-Width. ACM Trans. Comput. Log. 16(3): 24:1-24:27 (2015) - 2014
- [j12]Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verification Reliab. 24(8): 593-607 (2014) - 2013
- [j11]Christiaan Hartman, Marijn Heule, Kees Kwekkeboom, Alain Noels:
Symmetry in Gardens of Eden. Electron. J. Comb. 20(3): 16 (2013) - [j10]Marijn Heule, Sicco Verwer:
Software model synthesis using satisfiability solvers. Empir. Softw. Eng. 18(4): 825-856 (2013) - 2012
- [j9]Matti Järvisalo, Armin Biere, Marijn Heule:
Simulating Circuit-Level Simplifications on CNF. J. Autom. Reason. 49(4): 583-619 (2012) - 2011
- [j8]Peter van der Tak, Antonio Ramos, Marijn Heule:
Reusing the Assignment Trail in CDCL Solvers. J. Satisf. Boolean Model. Comput. 7(4): 133-138 (2011) - [j7]Marijn Heule:
Introduction to Mathematics of Satisfiability, Victor W. Marek, Chapman & Hall/CRC, 2009. Hardback, ISBN-13: 978-143980167-3, $89.95. Theory Pract. Log. Program. 11(1): 126-130 (2011) - 2008
- [j6]Hans van Maaren, Linda van Norden, M. J. H. Heule:
Sums of squares based approximation algorithms for MAX-SAT. Discret. Appl. Math. 156(10): 1754-1779 (2008) - [j5]Marijn Heule, Hans van Maaren:
Parallel SAT Solving using Bit-level Operations. J. Satisf. Boolean Model. Comput. 4(2-4): 99-116 (2008) - [j4]Marijn Heule, Hans van Maaren:
Whose side are you on? Finding solutions in a biased search-tree. J. Satisf. Boolean Model. Comput. 4(2-4): 117-148 (2008) - 2007
- [j3]P. R. Herwig, M. J. H. Heule, P. M. van Lambalgen, Hans van Maaren:
A New Method to Construct Lower Bounds for Van der Waerden Numbers. Electron. J. Comb. 14(1) (2007) - [j2]M. J. H. Heule, Léon J. M. Rothkrantz:
Solving games: Dependence of applicable solving procedures. Sci. Comput. Program. 67(1): 105-124 (2007) - 2006
- [j1]Marijn Heule, Hans van Maaren:
March_dl: Adding Adaptive Heuristics and a New Branching Strategy. J. Satisf. Boolean Model. Comput. 2(1-4): 47-59 (2006)
Conference and Workshop Papers
- 2024
- [c110]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
From Clauses to Klauses [inline-graphic not available: see fulltext]. CAV (1) 2024: 110-132 - [c109]Thomas Garrison, Marijn J. H. Heule, Bernardo Subercaseaux:
PackIt!: Gamified Rectangle Packing. FUN 2024: 14:1-14:19 - [c108]Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule:
Formal Verification of the Empty Hexagon Number. ITP 2024: 35:1-35:19 - [c107]Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins:
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane. CICM 2024: 21-41 - [c106]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: 29:1-29:18 - [c105]Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule:
TaSSAT: Transfer and Share SAT. TACAS (1) 2024: 34-42 - [c104]Marijn J. H. Heule, Manfred Scheucher:
Happy Ending: An Empty Hexagon in Every Set of 30 Points. TACAS (1) 2024: 61-80 - 2023
- [c103]Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule:
Verified Encodings for SAT Solvers. FMCAD 2023: 141-151 - [c102]Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, Bryan Parno:
Mariposa: Measuring SMT Instability in Automated Program Verification. FMCAD 2023: 178-188 - [c101]Marijn J. H. Heule:
Without Loss of Satisfaction. ICTAC 2023: 4-14 - [c100]Emre Yolcu, Marijn J. H. Heule:
Exponential Separations Using Guarded Extension Variables. ITCS 2023: 101:1-101:22 - [c99]Bernardo Subercaseaux, Marijn Heule:
Toward Optimal Radio Colorings of Hypercubes via SAT-solving. LPAR 2023: 386-404 - [c98]Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule:
A Linear Weight Transfer Rule for Local Search. NFM 2023: 447-463 - [c97]Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule:
Certified Knowledge Compilation with Application to Verified Model Counting. SAT 2023: 6:1-6:20 - [c96]Andrew Haberlandt, Harrison Green, Marijn J. H. Heule:
Effective Auxiliary Variables via Structured Reencoding. SAT 2023: 11:1-11:19 - [c95]Armin Biere, Mathias Fleury, Nils Froleyks, Marijn J. H. Heule:
The SAT Museum. POS@SAT 2023: 72-87 - [c94]Joseph E. Reeves, Benjamin Kiesl-Reiter, Marijn J. H. Heule:
Propositional Proof Skeletons. TACAS (1) 2023: 329-347 - [c93]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: 348-366 - [c92]Bernardo Subercaseaux, Marijn J. H. Heule:
The Packing Chromatic Number of the Infinite Square Grid is 15. TACAS (1) 2023: 389-406 - [c91]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: 73-83 - 2022
- [c90]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Preprocessing of Propagation Redundant Clauses. IJCAR 2022: 106-124 - [c89]Marijn J. H. Heule, Anthony Karahalios, Willem-Jan van Hoeve:
From Cliques to Colorings and Back Again. CP 2022: 26:1-26:10 - [c88]Evan Lohn, Chris Lambert, Marijn J. H. Heule:
Compact Symmetry Breaking for Tournaments. FMCAD 2022: 179-188 - [c87]Graham Gobieski, Souradip Ghosh, Marijn Heule, Todd C. Mowry, Tony Nowatzki, Nathan Beckmann, Brandon Lucia:
A programmable, energy-minimal dataflow compiler and architecture. MICRO 2022: 546-564 - [c86]Leroy Chew, Marijn J. H. Heule:
Relating Existing Powerful Proof Systems for QBF. SAT 2022: 10:1-10:22 - [c85]Bernardo Subercaseaux, Marijn J. H. Heule:
The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. SAT 2022: 21:1-21:16 - [c84]Armin Biere, Md. Solimul Chowdhury, Marijn J. H. Heule, Benjamin Kiesl, Michael W. Whalen:
Migrating Solver State. SAT 2022: 27:1-27:24 - [c83]Randal E. Bryant, Armin Biere, Marijn J. H. Heule:
Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) 2022: 443-461 - [c82]Joseph E. Reeves, Marijn J. H. Heule, Randal E. Bryant:
Moving Definition Variables in Quantified Boolean Formulas. TACAS (1) 2022: 462-479 - 2021
- [c81]Randal E. Bryant, Marijn J. H. Heule:
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. CADE 2021: 433-449 - [c80]Emre Yolcu, Scott Aaronson, Marijn J. H. Heule:
An Automated Approach to the Collatz Conjecture. CADE 2021: 468-484 - [c79]Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. FMCAD 2021: 231-240 - [c78]Travis Hance, Marijn Heule, Ruben Martins, Bryan Parno:
Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. NSDI 2021: 115-131 - [c77]Marijn J. H. Heule:
Chinese Remainder Encoding for Hamiltonian Cycles. SAT 2021: 216-224 - [c76]Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J. H. Heule, Armin Biere:
XOR Local Search for Boolean Brent Equations. SAT 2021: 417-435 - [c75]Zhenjun Liu, Leroy Chew, Marijn J. H. Heule:
Avoiding Monochromatic Rectangles Using Shift Patterns. SOCS 2021: 225-227 - [c74]Seulkee Baek, Mario Carneiro, Marijn J. H. Heule:
A Flexible Proof Format for SAT Solver-Elaborator Communication. TACAS (1) 2021: 59-75 - [c73]Randal E. Bryant, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. TACAS (1) 2021: 76-93 - [c72]Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen:
cake_lpr: Verified Propagation Redundancy Checking in CakeML. TACAS (2) 2021: 223-241 - 2020
- [c71]Sean A. Weaver, Marijn Heule:
Constructing Minimal Perfect Hash Functions Using SAT Technology. AAAI 2020: 1668-1675 - [c70]Joshua Brakensiek, Marijn Heule, John Mackey, David E. Narváez:
The Resolution of Keller's Conjecture. IJCAR (1) 2020: 48-65 - [c69]Joseph Sweeney, Marijn J. H. Heule, Lawrence T. Pileggi:
Modeling Techniques for Logic Locking. ICCAD 2020: 80:1-80:9 - [c68]Peter Oostema, Ruben Martins, Marijn Heule:
Coloring Unit-Distance Strips using SAT. LPAR 2020: 373-389 - [c67]Joseph Sweeney, Marijn Heule, Lawrence T. Pileggi:
Sensitivity Analysis of Locked Circuits. LPAR 2020: 483-497 - [c66]Leroy Chew, Marijn J. H. Heule:
Sorting Parity Encodings by Reusing Variables. SAT 2020: 1-10 - [c65]Emre Yolcu, Xinyu Wu, Marijn J. H. Heule:
Mycielski Graphs and PR Proofs. SAT 2020: 201-217 - 2019
- [c64]Benjamin Kiesl, Marijn J. H. Heule, Armin Biere:
Truth Assignments as Conditional Autarkies. ATVA 2019: 48-64 - [c63]Marijn J. H. Heule:
Trimming Graphs Using Clausal Proof Optimization. CP 2019: 251-267 - [c62]Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Clausal Proofs of Mutilated Chessboards. NFM 2019: 204-210 - [c61]Marijn J. H. Heule, Manuel Kauers, Martina Seidl:
Local Search for Fast Matrix Multiplication. SAT 2019: 155-163 - [c60]Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Encoding Redundancy for Satisfaction-Driven Clause Learning. TACAS (1) 2019: 41-58 - 2018
- [c59]Marijn J. H. Heule:
Schur Number Five. AAAI 2018: 6598-6606 - [c58]Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule:
Extended Resolution Simulates DRAT. IJCAR 2018: 516-531 - [c57]Armin Biere, Marijn Heule:
The Effect of Scrambling CNFs. POS@SAT 2018: 111-126 - [c56]Marijn J. H. Heule, Armin Biere:
What a Difference a Variable Makes. TACAS (2) 2018: 75-92 - 2017
- [c55]Tomás Balyo, Marijn J. H. Heule, Matti Järvisalo:
SAT Competition 2016: Recent Developments. AAAI 2017: 5061-5063 - [c54]J Strother Moore, Marijn J. H. Heule:
Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. ARCADE@CADE 2017: 42-45 - [c53]Marijn Heule, Benjamin Kiesl:
The Potential of Interference-Based Proof Systems. ARCADE@CADE 2017: 51-54 - [c52]Marijn J. H. Heule, Benjamin Kiesl, Armin Biere:
Short Proofs Without New Variables. CADE 2017: 130-147 - [c51]Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp:
Efficient Certified RAT Verification. CADE 2017: 220-236 - [c50]Marijn Heule:
Everything's Bigger in Texas: "The Largest Math Proof Ever". GCAI 2017: 1-5 - [c49]Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, Armin Biere:
PRuning Through Satisfaction. Haifa Verification Conference 2017: 179-194 - [c48]Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek:
Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method. IJCAI 2017: 4864-4868 - [c47]Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler:
Efficient, Verified Checking of Propositional Proofs. ITP 2017: 269-284 - [c46]Benjamin Kiesl, Marijn J. H. Heule, Martina Seidl:
A Little Blocked Literal Goes a Long Way. SAT 2017: 281-297 - [c45]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: 3-20 - [c44]Katalin Fazekas, Marijn J. H. Heule, Martina Seidl, Armin Biere:
Skolem Function Continuation for Quantified Boolean Formulas. TAP@STAF 2017: 129-138 - 2016
- [c43]C. K. Cuong, M. J. H. Heule:
Computing Maximum Unavoidable Subgraphs Using SAT Solvers. SAT 2016: 196-211 - [c42]Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek:
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. SAT 2016: 228-245 - [c41]Marijn J. H. Heule, Rezwana Reaz, Hrishikesh B. Acharya, Mohamed G. Gouda:
Analysis of Computing Policies Using SAT Solvers (Short Paper). SSS 2016: 190-194 - [c40]Marijn J. H. Heule:
The Quest for Perfect and Compact Symmetry Breaking for Graph Problems. SYNASC 2016: 149-156 - 2015
- [c39]Marijn Heule, Torsten Schaub:
What's Hot in the SAT and ASP Competitions. AAAI 2015: 4322-4323 - [c38]Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Expressing Symmetry Breaking in DRAT Proofs. CADE 2015: 591-606 - [c37]Marijn Heule, Armin Biere:
Clausal Proof Compression. IWIL@LPAR 2015: 21-26 - [c36]Marijn J. H. Heule, Armin Biere:
Compositional Propositional Proofs. LPAR 2015: 444-459 - [c35]Marijn Heule, Martina Seidl, Armin Biere:
Blocked Literals Are Universal. NFM 2015: 436-442 - [c34]Rezwana Reaz, Muqeet Ali, Mohamed G. Gouda, Marijn Heule, Ehab S. Elmallah:
The Implication Problem of Computing Policies. SSS 2015: 109-123 - 2014
- [c33]Marijn Heule, Martina Seidl, Armin Biere:
A Unified Proof System for QBF Preprocessing. IJCAR 2014: 91-106 - [c32]Marijn Heule, Martina Seidl, Armin Biere:
Efficient extraction of Skolem functions from QRAT proofs. FMCAD 2014: 107-114 - [c31]Marijn Heule, Norbert Manthey, Tobias Philipp:
Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers. POS@SAT 2014: 12-25 - [c30]Anton Belov, Marijn Heule, João Marques-Silva:
MUS Extraction Using Clausal Proofs. SAT 2014: 48-57 - [c29]Tomás Balyo, Andreas Fröhlich, Marijn Heule, Armin Biere:
Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask). SAT 2014: 317-332 - [c28]Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.:
DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. SAT 2014: 422-429 - 2013
- [c27]Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Verifying Refutations with Extended Resolution. CADE 2013: 345-359 - [c26]Marijn Heule, Matti Järvisalo, Armin Biere:
Revisiting Hyper Binary Resolution. CPAIOR 2013: 77-93 - [c25]Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Trimming while checking clausal proofs. FMCAD 2013: 181-188 - [c24]Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.:
Mechanical Verification of SAT Refutations with Extended Resolution. ITP 2013: 229-244 - [c23]Marijn Heule, Armin Biere:
Blocked Clause Decomposition. LPAR 2013: 423-438 - [c22]Marijn Heule, Stefan Szeider:
A SAT Approach to Clique-Width. SAT 2013: 318-334 - 2012
- [c21]Matti Järvisalo, Marijn Heule, Armin Biere:
Inprocessing Rules. IJCAR 2012: 355-370 - [c20]Norbert Manthey, Marijn Heule, Armin Biere:
Automated Reencoding of Boolean Formulas. Haifa Verification Conference 2012: 102-117 - [c19]Peter van der Tak, Marijn Heule, Armin Biere:
Concurrent Cube-and-Conquer - (Poster Presentation). SAT 2012: 475-476 - [c18]Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits:
Guided Merging of Sequence Diagrams. SLE 2012: 164-183 - 2011
- [c17]Marijn Heule, Oliver Kullmann, Siert Wieringa, Armin Biere:
Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. Haifa Verification Conference 2011: 50-65 - [c16]Marijn Heule, Matti Järvisalo, Armin Biere:
Efficient CNF Simplification Based on Binary Implication Graphs. SAT 2011: 201-215 - [c15]Antonio Ramos, Peter van der Tak, Marijn Heule:
Between Restarts and Backjumps. SAT 2011: 216-229 - [c14]Oliver Gableske, Marijn Heule:
EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation. SAT 2011: 367-368 - 2010
- [c13]Marijn Heule, Toby Walsh:
Symmetry in Solutions. AAAI 2010: 77-82 - [c12]Marijn Heule, Sicco Verwer:
Exact DFA Identification Using SAT Solvers. ICGI 2010: 66-79 - [c11]Marijn Heule, Matti Järvisalo, Armin Biere:
Covered Clause Elimination. LPAR short papers(Yogyakarta) 2010: 41-46 - [c10]Marijn Heule, Matti Järvisalo, Armin Biere:
Clause Elimination Procedures for CNF Formulas. LPAR (Yogyakarta) 2010: 357-371 - [c9]Matti Järvisalo, Armin Biere, Marijn Heule:
Blocked Clause Elimination. TACAS 2010: 129-144 - 2009
- [c8]Bas Schaafsma, Marijn Heule, Hans van Maaren:
Dynamic Symmetry Breaking by Simulating Zykov Contraction. SAT 2009: 223-236 - 2007
- [c7]Marijn Heule, Hans van Maaren:
From Idempotent Generalized Boolean Assignments to Multi-bit Search. SAT 2007: 134-147 - [c6]Marijn Heule, Hans van Maaren:
Effective Incorporation of Double Look-Ahead Procedures. SAT 2007: 258-271 - [c5]Henriette Bier, Adriaan de Jong, Gijs van der Hoorn, Niels Brouwers, Marijn Heule, Hans van Maaren:
Prototypes for Automated Architectural 3D-Layout. VSMM 2007: 203-214 - 2005
- [c4]Marijn Heule, Hans van Maaren:
Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming. SAT 2005: 122-134 - 2004
- [c3]Marijn Heule, Hans van Maaren:
Aligning CNF- and Equivalence-Reasoning. SAT (Selected Papers 2004: 145-156 - [c2]Marijn Heule, Mark Dufour, Joris E. van Zwieten, Hans van Maaren:
March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver. SAT (Selected Papers 2004: 345-359 - [c1]Marijn Heule, Hans van Maaren:
Aligning CNF- and Equivalence-reasoning. SAT 2004
Parts in Books or Collections
- 2021
- [p4]Marijn J. H. Heule, Hans van Maaren:
Look-Ahead Based SAT Solvers. Handbook of Satisfiability 2021: 183-212 - [p3]Marijn J. H. Heule:
Proofs of Unsatisfiability. Handbook of Satisfiability 2021: 635-668 - 2018
- [p2]Marijn J. H. Heule, Oliver Kullmann, Armin Biere:
Cube-and-Conquer for Satisfiability. Handbook of Parallel Constraint Reasoning 2018: 31-59 - 2009
- [p1]Marijn Heule, Hans van Maaren:
Look-Ahead Based SAT Solvers. Handbook of Satisfiability 2009: 155-184
Editorship
- 2024
- [e7]Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt:
Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14739, Springer 2024, ISBN 978-3-031-63497-0 [contents] - [e6]Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt:
Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II. Lecture Notes in Computer Science 14740, Springer 2024, ISBN 978-3-031-63500-7 [contents] - [e5]Nikolaj S. Bjørner, Marijn Heule, Andrei Voronkov:
LPAR 2024 Complementary Volume, Port Louis, Mauritius, May 26-31, 2024. Kalpa Publications in Computing 18, EasyChair 2024 [contents] - [e4]Nikolaj S. Bjørner, Marijn Heule, Andrei Voronkov:
LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024. EPiC Series in Computing 100, EasyChair 2024 [contents] - 2021
- [e3]Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh:
Handbook of Satisfiability - Second Edition. Frontiers in Artificial Intelligence and Applications 336, IOS Press 2021, ISBN 978-1-64368-160-3 [contents] - 2015
- [e2]Marijn Heule, Sean A. Weaver:
Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings. Lecture Notes in Computer Science 9340, Springer 2015, ISBN 978-3-319-24317-7 [contents] - 2009
- [e1]Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh:
Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications 185, IOS Press 2009, ISBN 978-1-58603-929-5 [contents]
Data and Artifacts
- 2021
- [d3]Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. Zenodo, 2021
- [d2]Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. Zenodo, 2021 - 2020
- [d1]Joshua Brakensiek, Marijn Heule, John Mackey, David E. Narváez:
The Resolution of Keller's Conjecture - Computation Logs. Zenodo, 2020
Informal and Other Publications
- 2024
- [i33]Marijn J. H. Heule, Manfred Scheucher:
Happy Ending: An Empty Hexagon in Every Set of 30 Points. CoRR abs/2403.00737 (2024) - [i32]Thomas Garrison, Marijn J. H. Heule, Bernardo Subercaseaux:
PackIt! Gamified Rectangle Packing. CoRR abs/2403.12195 (2024) - [i31]Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule:
Formal Verification of the Empty Hexagon Number. CoRR abs/2403.17370 (2024) - 2023
- [i30]Bernardo Subercaseaux, Marijn J. H. Heule:
The Packing Chromatic Number of the Infinite Square Grid is 15. CoRR abs/2301.09757 (2023) - [i29]Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule:
A Linear Weight Transfer Rule for Local Search. CoRR abs/2303.14894 (2023) - [i28]Andrew Haberlandt, Harrison Green, Marijn J. H. Heule:
Effective Auxiliary Variables via Structured Reencoding. CoRR abs/2307.01904 (2023) - [i27]Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins:
Minimizing Pentagons in the Plane through Automated Reasoning. CoRR abs/2311.03645 (2023) - [i26]Marijn J. H. Heule, Inês Lynce, Stefan Szeider, André Schidler:
SAT Encodings and Beyond (Dagstuhl Seminar 23261). Dagstuhl Reports 13(6): 106-122 (2023) - 2022
- [i25]Isaac Grosof, Naifeng Zhang, Marijn J. H. Heule:
Towards the shortest DRAT proof of the Pigeonhole Principle. CoRR abs/2207.11284 (2022) - [i24]Emre Yolcu, Marijn J. H. Heule:
Exponential separations using guarded extension variables. CoRR abs/2211.12456 (2022) - 2021
- [i23]Randal E. Bryant, Marijn J. H. Heule:
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. CoRR abs/2105.00885 (2021) - [i22]Emre Yolcu, Scott Aaronson, Marijn J. H. Heule:
An Automated Approach to the Collatz Conjecture. CoRR abs/2105.14697 (2021) - [i21]Seulkee Baek, Mario Carneiro, Marijn J. H. Heule:
A Flexible Proof Format for SAT Solver-Elaborator Communication. CoRR abs/2109.09665 (2021) - [i20]Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki:
An Impossible Asylum. CoRR abs/2112.02142 (2021) - 2020
- [i19]Joseph Sweeney, Marijn J. H. Heule, Lawrence T. Pileggi:
Modeling Techniques for Logic Locking. CoRR abs/2009.10131 (2020) - [i18]Zhenjun Liu, Leroy Chew, Marijn Heule:
Avoiding Monochromatic Rectangles Using Shift Patterns. CoRR abs/2012.12582 (2020) - 2019
- [i17]Marijn J. H. Heule, Manuel Kauers, Martina Seidl:
Local Search for Fast Matrix Multiplication. CoRR abs/1903.11391 (2019) - [i16]Marijn J. H. Heule, Manuel Kauers, Martina Seidl:
New ways to multiply 3 x 3-matrices. CoRR abs/1905.10192 (2019) - [i15]Marijn J. H. Heule:
Trimming Graphs Using Clausal Proof Optimization. CoRR abs/1907.00929 (2019) - [i14]Joshua Brakensiek, Marijn Heule, John Mackey:
The Resolution of Keller's Conjecture. CoRR abs/1910.03740 (2019) - [i13]Sean A. Weaver, Marijn Heule:
Constructing Minimal Perfect Hash Functions Using SAT Technology. CoRR abs/1911.10099 (2019) - 2017
- [i12]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 abs/1701.04045 (2017) - [i11]Keenan Breik, Lakshmi Prakash, Chris Thachuk, Marijn Heule, David Soloveichik:
Computing properties of stable configurations of thermodynamic binding networks. CoRR abs/1709.08731 (2017) - [i10]Marijn J. H. Heule:
Schur Number Five. CoRR abs/1711.08076 (2017) - 2016
- [i9]Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek:
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. CoRR abs/1605.00723 (2016) - [i8]Marijn J. H. Heule:
The DRAT format and DRAT-trim checker. CoRR abs/1610.06229 (2016) - [i7]Luís Cruz-Filipe, Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp:
Efficient Certified RAT Verification. CoRR abs/1612.02353 (2016) - 2014
- [i6]Shai Haim, Marijn Heule:
Towards Ultra Rapid Restarts. CoRR abs/1402.4413 (2014) - [i5]Sid Mijnders, Boris de Wilde, Marijn Heule:
Symbiosis of Search and Heuristics for Random 3-SAT. CoRR abs/1402.4455 (2014) - [i4]Peter van der Tak, Marijn Heule, Armin Biere:
Concurrent Cube-and-Conquer. CoRR abs/1402.4465 (2014) - 2013
- [i3]Marijn Heule, Stefan Szeider:
A SAT Approach to Clique-Width. CoRR abs/1304.5498 (2013) - 2010
- [i2]Marijn Heule, Toby Walsh:
Symmetry within Solutions. CoRR abs/1004.2624 (2010) - [i1]Marijn Heule, Matti Järvisalo, Armin Biere:
Covered Clause Elimination. CoRR abs/1011.5202 (2010)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:16 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
