Stop the war!Остановите войну!
for scientists:
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
2020 – today
- 2023
[j29]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)- [j28]Petar Vukmirovic, Jasmin Blanchette, Marijn J. H. Heule:
SAT-Inspired Eliminations for Superposition. ACM Trans. Comput. Log. 24(1): 7:1-7:25 (2023) - [c91]Emre Yolcu, Marijn J. H. Heule:
Exponential Separations Using Guarded Extension Variables. ITCS 2023: 101:1-101:22 - [i26]Bernardo Subercaseaux, Marijn J. H. Heule:
The Packing Chromatic Number of the Infinite Square Grid is 15. CoRR abs/2301.09757 (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, 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 - [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
- [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) - [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 - [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] - [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, 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) - [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 - [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, 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 - [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, Armin Biere:
What a Difference a Variable Makes. TACAS (2) 2018: 75-92 - [p2]Marijn J. H. Heule, Oliver Kullmann, Armin Biere:
Cube-and-Conquer for Satisfiability. Handbook of Parallel Constraint Reasoning 2018: 31-59 - 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) - [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 - [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, 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 - [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, 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) - [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, 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 - [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, 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) - [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 - [i3]Marijn Heule, Stefan Szeider:
A SAT Approach to Clique-Width. CoRR abs/1304.5498 (2013) - 2012
- [j9]Matti Järvisalo, Armin Biere, Marijn Heule:
Simulating Circuit-Level Simplifications on CNF. J. Autom. Reason. 49(4): 583-619 (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
- [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]