default search action
Marijn 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
2020 – today
- 2024
- [c110]Joseph E. Reeves
, Marijn J. H. Heule
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
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
TaSSAT: Transfer and Share SAT. TACAS (1) 2024: 34-42 - [c104]Marijn J. H. Heule
Happy Ending: An Empty Hexagon in Every Set of 30 Points. TACAS (1) 2024: 61-80 - [e7]Christoph Benzmüller
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
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] - [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
- [j33]Emre Yolcu
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
An Impossible Asylum. Am. Math. Mon. 130(5): 446-453 (2023) - [j29]Petar Vukmirovic
SAT-Inspired Eliminations for Superposition. ACM Trans. Comput. Log. 24(1): 7:1-7:25 (2023) - [j28]Randal E. Bryant
Generating Extended Resolution Proofs with a BDD-Based SAT Solver. ACM Trans. Comput. Log. 24(4): 31:1-31:28 (2023) - [c103]Cayden R. Codel, Jeremy Avigad
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
A Linear Weight Transfer Rule for Local Search. NFM 2023: 447-463 - [c97]Randal E. Bryant
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
The SAT Museum. POS@SAT 2023: 72-87 - [c94]Joseph E. Reeves
Propositional Proof Skeletons. TACAS (1) 2023: 329-347 - [c93]Dawn Michaelson
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers. TACAS (1) 2023: 348-366 - [c92]Bernardo Subercaseaux
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 - [d5]Armin Biere
The SAT Museum POS'23 Artifact. Zenodo, 2023 - [d4]Md. Solimul Chowdhury
Artifact for TaSSAT: A Stochastic Local Search Solver for SAT. Zenodo, 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
- [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) - [c90]Joseph E. Reeves
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
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
Migrating Solver State. SAT 2022: 27:1-27:24 - [c83]Randal E. Bryant
Clausal Proofs for Pseudo-Boolean Reasoning. TACAS (1) 2022: 443-461 - [c82]Joseph E. Reeves
Moving Definition Variables in Quantified Boolean Formulas. TACAS (1) 2022: 462-479 - [i25]Isaac Grosof, Naifeng Zhang
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
- [j24]Nils Froleyks
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) - [c81]Randal E. Bryant
Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver. CADE 2021: 433-449 - [c80]Emre Yolcu
An Automated Approach to the Collatz Conjecture. CADE 2021: 468-484 - [c79]Petar Vukmirovic, Jasmin Blanchette
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
XOR Local Search for Boolean Brent Equations. SAT 2021: 417-435 - [c75]Zhenjun Liu, Leroy Chew
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
cake_lpr: Verified Propagation Redundancy Checking in CakeML. TACAS (2) 2021: 223-241 - [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 - [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] - [d3]Petar Vukmirovic
SAT-Inspired Eliminations for Superposition. Version 1. Zenodo, 2021 [all versions] - [d2]Petar Vukmirovic
SAT-Inspired Eliminations for Superposition. Version 2. Zenodo, 2021 [all versions] - [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
- [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
Simulating Strong Practical Proof Systems with Extended Resolution. J. Autom. Reason. 64(7): 1247-1267 (2020) - [c71]Sean A. Weaver, Marijn Heule
Constructing Minimal Perfect Hash Functions Using SAT Technology. AAAI 2020: 1668-1675 - [c70]Joshua Brakensiek, Marijn Heule
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
Sensitivity Analysis of Locked Circuits. LPAR 2020: 483-497 - [c66]Leroy Chew
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 - [d1]Joshua Brakensiek, Marijn Heule
The Resolution of Keller's Conjecture - Computation Logs. Zenodo, 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)
2010 – 2019
- 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) - [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
Clausal Proofs of Mutilated Chessboards. NFM 2019: 204-210 - [c61]Marijn J. H. Heule
Local Search for Fast Matrix Multiplication. SAT 2019: 155-163 - [c60]Marijn J. H. Heule
Encoding Redundancy for Satisfaction-Driven Clause Learning. TACAS (1) 2019: 41-58 - [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) - 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
What a Difference a Variable Makes. TACAS (2) 2018: 75-92 - [p2]Marijn J. H. Heule
Cube-and-Conquer for Satisfiability. Handbook of Parallel Constraint Reasoning 2018: 31-59 - 2017
- [j16]Marijn J. H. Heule
The science of brute force. Commun. ACM 60(8): 70-79 (2017) - [j15]Marijn J. H. Heule
Solution Validation and Extraction for QBF Preprocessing. J. Autom. Reason. 58(1): 97-125 (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
The Potential of Interference-Based Proof Systems. ARCADE@CADE 2017: 51-54 - [c52]Marijn J. H. Heule
Short Proofs Without New Variables. CADE 2017: 130-147 - [c51]Luís Cruz-Filipe
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
PRuning Through Satisfaction. Haifa Verification Conference 2017: 179-194 - [c48]Marijn J. H. Heule
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
Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions. TACAS (2) 2017: 3-20 - [c44]Katalin Fazekas
Skolem Function Continuation for Quantified Boolean Formulas. TAP@STAF 2017: 129-138 - [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
- [c43]C. K. Cuong, M. J. H. Heule
Computing Maximum Unavoidable Subgraphs Using SAT Solvers. SAT 2016: 196-211 - [c42]Marijn J. H. Heule
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. SAT 2016: 228-245 - [c41]Marijn J. H. Heule
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 - [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) - 2015
- [j14]Marijn Heule, Matti Järvisalo
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) - [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 - [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] - 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) - [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
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 - [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
- [j11]Christiaan Hartman, Marijn Heule
Symmetry in Gardens of Eden. Electron. J. Comb. 20(3): 16 (2013) - [j10]Marijn Heule
Software model synthesis using satisfiability solvers. Empir. Softw. Eng. 18(4): 825-856 (2013) - [c27]Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Verifying Refutations with Extended Resolution. CADE 2013: 345-359 - [c26]Marijn Heule
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 - [i3]Marijn Heule, Stefan Szeider:
A SAT Approach to Clique-Width. CoRR abs/1304.5498 (2013) - 2012
- [j9]Matti Järvisalo
Simulating Circuit-Level Simplifications on CNF. J. Autom. Reason. 49(4): 583-619 (2012) - [c21]Matti Järvisalo
Inprocessing Rules. IJCAR 2012: 355-370 - [c20]Norbert Manthey, Marijn Heule
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
Guided Merging of Sequence Diagrams. SLE 2012: 164-183 - 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) - [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
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
Clause Elimination Procedures for CNF Formulas. LPAR (Yogyakarta) 2010: 357-371 - [c9]Matti Järvisalo
Blocked Clause Elimination. TACAS 2010: 129-144 - [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)
2000 – 2009
- 2009
- [c8]Bas Schaafsma, Marijn Heule, Hans van Maaren:
Dynamic Symmetry Breaking by Simulating Zykov Contraction. SAT 2009: 223-236 - [p1]Marijn Heule
Look-Ahead Based SAT Solvers. Handbook of Satisfiability 2009: 155-184 - [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] - 2008
- [b1]M. J. H. Heule:
SmArT solving: tools and techniques for satisfiability solvers. Delft University of Technology, Netherlands, 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
A New Method to Construct Lower Bounds for Van der Waerden Numbers. Electron. J. Comb. 14(1) (2007) - [j2]M. J. H. Heule
Solving games: Dependence of applicable solving procedures. Sci. Comput. Program. 67(1): 105-124 (2007) - [c7]Marijn Heule
From Idempotent Generalized Boolean Assignments to Multi-bit Search. SAT 2007: 134-147 - [c6]Marijn Heule
Effective Incorporation of Double Look-Ahead Procedures. SAT 2007: 258-271 - [c5]Henriette Bier
Prototypes for Automated Architectural 3D-Layout. VSMM 2007: 203-214 - 2006
- [j1]Marijn Heule
March_dl: Adding Adaptive Heuristics and a New Branching Strategy. J. Satisf. Boolean Model. Comput. 2(1-4): 47-59 (2006) - 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
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
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-12-13 20:06 CET 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: