203 citations · 391 across the 22 of their papers we have counts for
4 papers · 1 filter
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…