203 citations · 391 across the 22 of their papers we have counts for
13 papers · 1 filter
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…
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…
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…
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…
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…
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…
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…
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.
Covered Clause Elimination
Marijn Heule, Matti Järvisalo, Armin Biere
Generalizing the novel clause elimination procedures developed in [M. Heule, M. Järvisalo, and A. Biere. Clause elimination procedures for CNF formulas. In Proc. LPAR-17, volume 63…