Marijn Heule

Publication Activity (10 Years)

Years Active: 2004-2023
Publications (10 Years): 24

Top Topics

Propositional Satisfiability

Computationally Costly

Symmetry Breaking

Top Venues

Publications

Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, Bryan Parno
Mariposa: Measuring SMT Instability in Automated Program Verification. FMCAD (2023)
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki
An Impossible Asylum. Am. Math. Mon. 130 (5) (2023)
Bernardo Subercaseaux, Marijn Heule
Toward Optimal Radio Colorings of Hypercubes via SAT-solving. LPAR (2023)
Joshua Brakensiek, Marijn Heule, John Mackey, David E. Narváez
The Resolution of Keller's Conjecture. J. Autom. Reason. 66 (3) (2022)
Graham Gobieski, Souradip Ghosh, Marijn Heule, Todd Mowry, Tony Nowatzki, Nathan Beckmann, Brandon Lucia
A programmable, energy-minimal dataflow compiler and architecture. MICRO (2022)
David Neiman, John Mackey, Marijn Heule
Tighter Bounds on Directed Ramsey Number R(7). Graphs Comb. 38 (5) (2022)
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki
An Impossible Asylum. CoRR (2021)
Travis Hance, Marijn Heule, Ruben Martins, Bryan Parno
Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. NSDI (2021)
Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda
SAT Competition 2020. Artif. Intell. 301 (2021)
Zhenjun Liu, Leroy Chew, Marijn Heule
Avoiding Monochromatic Rectangles Using Shift Patterns. CoRR (2020)
Peter Oostema, Ruben Martins, Marijn Heule
Coloring Unit-Distance Strips using SAT. LPAR (2020)
Joshua Brakensiek, Marijn Heule, John Mackey, David E. Narváez
The Resolution of Keller's Conjecture. IJCAR (1) (2020)
Sean A. Weaver, Marijn Heule
Constructing Minimal Perfect Hash Functions Using SAT Technology. AAAI (2020)
Joseph Sweeney, Marijn Heule, Lawrence T. Pileggi
Sensitivity Analysis of Locked Circuits. LPAR (2020)
Keenan Breik, Chris Thachuk, Marijn Heule, David Soloveichik
Computing properties of stable configurations of thermodynamic binding networks. Theor. Comput. Sci. 785 (2019)
Joshua Brakensiek, Marijn Heule, John Mackey
The Resolution of Keller's Conjecture. CoRR (2019)
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) (2019)
Sean A. Weaver, Marijn Heule
Constructing Minimal Perfect Hash Functions Using SAT Technology. CoRR (2019)
Armin Biere, Marijn Heule
The Effect of Scrambling CNFs. POS@SAT (2018)
Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler
Efficient, Verified Checking of Propositional Proofs. ITP (2017)
Marijn Heule
Everything's Bigger in Texas: "The Largest Math Proof Ever". GCAI (2017)
Keenan Breik, Lakshmi Prakash, Chris Thachuk, Marijn Heule, David Soloveichik
Computing properties of stable configurations of thermodynamic binding networks. CoRR (2017)
Marijn Heule, Benjamin Kiesl
The Potential of Interference-Based Proof Systems. ARCADE@CADE (2017)
Luís Cruz-Filipe, Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
Efficient Certified RAT Verification. CoRR (2016)
Marijn Heule, Armin Biere
Clausal Proof Compression. IWIL@LPAR (2015)
Marijn Heule, Stefan Szeider
A SAT Approach to Clique-Width. ACM Trans. Comput. Log. 16 (3) (2015)
Marijn Heule, Martina Seidl, Armin Biere
Blocked Literals Are Universal. NFM (2015)
Rezwana Reaz, Muqeet Ali, Mohamed G. Gouda, Marijn Heule, Ehab S. Elmallah
The Implication Problem of Computing Policies. SSS (2015)
Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, Armin Biere
Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. 53 (2015)
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Expressing Symmetry Breaking in DRAT Proofs. CADE (2015)
Marijn Heule, Torsten Schaub
What's Hot in the SAT and ASP Competitions. AAAI (2015)
Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.
DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. SAT (2014)
Marijn Heule, Martina Seidl, Armin Biere
A Unified Proof System for QBF Preprocessing. IJCAR (2014)
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)
Peter van der Tak, Marijn Heule, Armin Biere
Concurrent Cube-and-Conquer. CoRR (2014)
Marijn Heule, Norbert Manthey, Tobias Philipp
Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers. POS@SAT (2014)
Marijn Heule, Martina Seidl, Armin Biere
Efficient extraction of Skolem functions from QRAT proofs. FMCAD (2014)
Anton Belov, Marijn Heule, João Marques-Silva
MUS Extraction Using Clausal Proofs. SAT (2014)
Shai Haim, Marijn Heule
Towards Ultra Rapid Restarts. CoRR (2014)
Sid Mijnders, Boris de Wilde, Marijn Heule
Symbiosis of Search and Heuristics for Random 3-SAT. CoRR (2014)
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) (2014)
Marijn Heule, Stefan Szeider
A SAT Approach to Clique-Width CoRR (2013)
Marijn Heule, Matti Järvisalo, Armin Biere
Revisiting Hyper Binary Resolution. CPAIOR (2013)
Marijn Heule, Sicco Verwer
Software model synthesis using satisfiability solvers. Empir. Softw. Eng. 18 (4) (2013)
Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.
Mechanical Verification of SAT Refutations with Extended Resolution. ITP (2013)
Christiaan Hartman, Marijn Heule, Kees Kwekkeboom, Alain Noels
Symmetry in Gardens of Eden. Electron. J. Comb. 20 (3) (2013)
Marijn Heule, Stefan Szeider
A SAT Approach to Clique-Width. SAT (2013)
Marijn Heule, Armin Biere
Blocked Clause Decomposition. LPAR (2013)
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Trimming while checking clausal proofs. FMCAD (2013)
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Verifying Refutations with Extended Resolution. CADE (2013)
Norbert Manthey, Marijn Heule, Armin Biere
Automated Reencoding of Boolean Formulas. Haifa Verification Conference (2012)
Magdalena Widl, Armin Biere, Petra Brosch, Uwe Egly, Marijn Heule, Gerti Kappel, Martina Seidl, Hans Tompits
Guided Merging of Sequence Diagrams. SLE (2012)
Matti Järvisalo, Marijn Heule, Armin Biere
Inprocessing Rules. IJCAR (2012)
Peter van der Tak, Marijn Heule, Armin Biere
Concurrent Cube-and-Conquer - (Poster Presentation). SAT (2012)
Matti Järvisalo, Armin Biere, Marijn Heule
Simulating Circuit-Level Simplifications on CNF. J. Autom. Reason. 49 (4) (2012)
Antonio Ramos, Peter van der Tak, Marijn Heule
Between Restarts and Backjumps. SAT (2011)
Marijn Heule, Matti Järvisalo, Armin Biere
Efficient CNF Simplification Based on Binary Implication Graphs. SAT (2011)
Marijn Heule
, Victor W. Marek, Chapman & Hall/CRC, 2009. Hardback, ISBN-13: 978-143980167-3, $89.95. Theory Pract. Log. Program. 11 (1) (2011)
Marijn Heule, Oliver Kullmann, Siert Wieringa, Armin Biere
Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. Haifa Verification Conference (2011)
Peter van der Tak, Antonio Ramos, Marijn Heule
Reusing the Assignment Trail in CDCL Solvers. J. Satisf. Boolean Model. Comput. 7 (4) (2011)
Oliver Gableske, Marijn Heule
EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation. SAT (2011)
Marijn Heule, Toby Walsh
Symmetry within Solutions CoRR (2010)
Marijn Heule, Matti Järvisalo, Armin Biere
Covered Clause Elimination. LPAR short papers(Yogyakarta) (2010)
Marijn Heule, Matti Järvisalo, Armin Biere
Clause Elimination Procedures for CNF Formulas. LPAR (Yogyakarta) (2010)
Marijn Heule, Toby Walsh
Symmetry in Solutions. AAAI (2010)
Marijn Heule, Sicco Verwer
Exact DFA Identification Using SAT Solvers. ICGI (2010)
Matti Järvisalo, Armin Biere, Marijn Heule
Blocked Clause Elimination. TACAS (2010)
Marijn Heule, Matti Järvisalo, Armin Biere
Covered Clause Elimination CoRR (2010)
Bas Schaafsma, Marijn Heule, Hans van Maaren
Dynamic Symmetry Breaking by Simulating Zykov Contraction. SAT (2009)
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) (2008)
Marijn Heule, Hans van Maaren
Parallel SAT Solving using Bit-level Operations. J. Satisf. Boolean Model. Comput. 4 (2-4) (2008)
Henriette Bier, Adriaan de Jong, Gijs van der Hoorn, Niels Brouwers, Marijn Heule, Hans van Maaren
Prototypes for Automated Architectural 3D-Layout. VSMM (2007)
Marijn Heule, Hans van Maaren
From Idempotent Generalized Boolean Assignments to Multi-bit Search. SAT (2007)
Marijn Heule, Hans van Maaren
Effective Incorporation of Double Look-Ahead Procedures. SAT (2007)
Marijn Heule, Hans van Maaren
March_dl: Adding Adaptive Heuristics and a New Branching Strategy. J. Satisf. Boolean Model. Comput. 2 (1-4) (2006)
Marijn Heule, Hans van Maaren
Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming. SAT (2005)
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)
Marijn Heule, Hans van Maaren
Aligning CNF- and Equivalence-Reasoning. SAT (Selected Papers (2004)
Marijn Heule, Hans van Maaren
Aligning CNF- and Equivalence-reasoning. SAT (2004)