203 citations · 391 across the 22 of their papers we have counts for
30 papers
Effective Auxiliary Variables via Structured Reencoding
Andrew Haberlandt, Harrison Green, Marijn J. H. Heule
Extended resolution shows that auxiliary variables are very powerful in theory. However, attempts to exploit this potential in practice have had limited success. One reasonably eff…
A Linear Weight Transfer Rule for Local Search
Md Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
The Divide and Distribute Fixed Weights algorithm (ddfw) is a dynamic local search SAT-solving algorithm that transfers weight from satisfied to falsified clauses in local minima.…
The Packing Chromatic Number of the Infinite Square Grid is 15
Bernardo Subercaseaux, Marijn J. H. Heule
A packing -coloring is a natural variation on the standard notion of graph -coloring, where vertices are assigned numbers from , and any two vertices assign…
Exponential separations using guarded extension variables
Emre Yolcu, Marijn J. H. Heule
We study the complexity of proof systems augmenting resolution with inference rules that allow, given a formula in conjunctive normal form, deriving clauses that are not necess…
Towards the shortest DRAT proof of the Pigeonhole Principle
Isaac Grosof, Naifeng Zhang, Marijn J. H. Heule
The Pigeonhole Principle (PHP) has been heavily studied in automated reasoning, both theoretically and in practice. Most solvers have exponential runtime and proof length, while so…
An Impossible Asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp +2
In 1982, Raymond Smullyan published an article, "The Asylum of Doctor Tarr and Professor Fether," that consists of a series of puzzles. These were later reprinted in the anthology,…
A Flexible Proof Format for SAT Solver-Elaborator Communication
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
We introduce FRAT, a new proof format for unsatisfiable SAT problems, and its associated toolchain. Compared to DRAT, the FRAT format allows solvers to include more information in…
An Automated Approach to the Collatz Conjecture
Emre Yolcu, Scott Aaronson, Marijn J. H. Heule
We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of t…
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
Randal E. Bryant, Marijn J. H. Heule
In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be enco…
Avoiding Monochromatic Rectangles Using Shift Patterns
Zhenjun Liu, Leroy Chew, Marijn Heule
Ramsey Theory deals with avoiding certain patterns. When constructing an instance that avoids one pattern, it is observed that other patterns emerge. For example, repetition emerge…
Tighter Bounds on Directed Ramsey Number R(7)
David Neiman, John Mackey, Marijn Heule
Tournaments are orientations of the complete graph, and the directed Ramsey number is the minimum number of vertices a tournament must have to be guaranteed to contain a tra…
Modeling Techniques for Logic Locking
Joseph Sweeney, Marijn J. H. Heule, Lawrence Pileggi
Logic locking is a method to prevent intellectual property (IP) piracy. However, under a reasonable attack model, SAT-based methods have proven to be powerful in obtaining the secr…
Constructing Minimal Perfect Hash Functions Using SAT Technology
Sean Weaver, Marijn Heule
Minimal perfect hash functions (MPHFs) are used to provide efficient access to values of large dictionaries (sets of key-value pairs). Discovering new algorithms for building MPHFs…
The Resolution of Keller's Conjecture
Joshua Brakensiek, Marijn Heule, John Mackey +1
We consider three graphs, , , and , related to Keller's conjecture in dimension 7. The conjecture is false for this dimension if and only if at least one…
Trimming Graphs Using Clausal Proof Optimization
Marijn J. H. Heule
We present a method to gradually compute a smaller and smaller unsatisfiable core of a propositional formula by minimizing proofs of unsatisfiability. The goal is to compute a mini…
New ways to multiply 3 x 3-matrices
Marijn J. H. Heule, Manuel Kauers, Martina Seidl
It is known since the 1970s that no more than 23 multiplications are required for computing the product of two 3 x 3-matrices. It is not known whether this can also be done with fe…
Local Search for Fast Matrix Multiplication
Marijn J. H. Heule, Manuel Kauers, Martina Seidl
Laderman discovered a scheme for computing the product of two 3x3 matrices using only 23 multiplications in 1976. Since then, some more such schemes were proposed, but it remains o…
Computing Small Unit-Distance Graphs with Chromatic Number 5
Marijn J. H. Heule
We present a new method for reducing the size of graphs with a given property. Our method, which is based on clausal proof minimization, allowed us to compute several 553-vertex un…
Schur Number Five
Marijn J. H. Heule
We present the solution of a century-old problem known as Schur Number Five: What is the largest (natural) number such that there exists a five-coloring of the positive numbers…
Computing properties of stable configurations of thermodynamic binding networks
Keenan Breik, Chris Thachuk, Marijn Heule +1
The promise of chemical computation lies in controlling systems incompatible with traditional electronic micro-controllers, with applications in synthetic biology and nano-scale ma…
Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions (Extended Version)
Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule +1
In an algorithmic complexity attack, a malicious party takes advantage of the worst-case behavior of an algorithm to cause denial-of-service. A prominent algorithmic complexity att…
Efficient Certified RAT Verification
Luís Cruz-Filipe, Marijn Heule, Warren Hunt +2
Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive eve…
The DRAT format and DRAT-trim checker
Marijn J. H. Heule
This document describes the DRAT format for clausal proofs and the DRAT-trim proof checker.
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek
The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = of natural numbers be divided into two parts, such th…