5 papers · 1 filter
Toward Satisfiability Modulo Realizability
Andrew Krapivin, Benjamin Przybocki, Marijn J. H. Heule
Problems complete for the existential theory of the reals () arise throughout discrete geometry. We introduce satisfiability modulo realizability, a SAT-based a…
Unfolding Boxes with Local Constraints
Long Qian, Eric Wang, Bernardo Subercaseaux +1
We consider the problem of finding and enumerating polyominos that can be folded into multiple non-isomorphic boxes. While several computational approaches have been proposed, incl…
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…
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane
Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule +1
We present a comprehensive demonstration of how automated reasoning can assist mathematical research, both in the discovery of conjectures and in their verification. Our focus is a…