9 citations · 17 across the 7 of their papers we have counts for
7 papers
Formal Verification of the Empty Hexagon Number
Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio +3
A recent breakthrough in computer-assisted mathematics showed that every set of points in the plane in general position (i.e., without three on a common line) contains an empt…
Happy Ending: An Empty Hexagon in Every Set of 30 Points
Marijn J. H. Heule, Manfred Scheucher
Satisfiability solving has been used to tackle a range of long-standing open math problems in recent years. We add another success by solving a geometry problem that originated a c…
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.…
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…
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…
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.