14 papers
Coloring Queens with Thousands of Encodings
Bernardo Subercaseaux, Benjamin Przybocki, Marijn J. H. Heule
In The Art of Computer Programming, Knuth benchmarked 10 encoding techniques for computing the chromatic number of the queen's graph: the minimum number of colors needed to color t…
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…
Tao's Equational Proof Challenge Accepted (Technical Report)
Lydia Kondylidou, Jasmin Blanchette, Marijn J. H. Heule
In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover.…
Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery
Benjamin Przybocki, John Mackey, Marijn J. H. Heule +1
Ramsey-good graphs are graphs that contain neither a clique of size nor an independent set of size . We study doubly saturated Ramsey-good graphs, defined as Ramsey-good gra…
Automated Reencoding Meets Graph Theory
Benjamin Przybocki, Bernardo Subercaseaux, Marijn J. H. Heule
Bounded Variable Addition (BVA) is a central preprocessing method in modern state-of-the-art SAT solvers. We provide a graph-theoretic characterization of which 2-CNF encodings can…
Orbitopal Fixing in SAT
Markus Anders, Cayden Codel, Marijn J. H. Heule
Despite their sophisticated heuristics, boolean satisfiability (SAT) solvers are still vulnerable to symmetry, causing them to visit search regions that are symmetric to ones alrea…
On the Edge of Core (Non-)Emptiness: An Automated Reasoning Approach to Approval-Based Multi-Winner Voting
Ratip Emin Berker, Emanuel Tewolde, Vincent Conitzer +3
Core stability is a natural and well-studied notion for group fairness in multi-winner voting, where the task is to select a committee from a pool of candidates. We study the setti…
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…
Automated Symmetric Constructions in Discrete Geometry
Bernardo Subercaseaux, Ethan Mackey, Long Qian +1
We present a computational methodology for obtaining rotationally symmetric sets of points satisfying discrete geometric constraints, and demonstrate its applicability by discoveri…
Certified Knowledge Compilation with Application to Formally Verified Model Counting
Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad +1
Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when form…
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…
PackIt! Gamified Rectangle Packing
Thomas Garrison, Marijn J. H. Heule, Bernardo Subercaseaux
We present and analyze PackIt!, a turn-based game consisting of packing rectangles on an grid. PackIt! can be easily played on paper, either as a competitive two-playe…
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…