Toward Satisfiability Modulo Realizability
For researchers in discrete geometry and computational geometry, this provides a practical SAT-based approach to solve realizability problems, with a concrete open problem solved.
The paper introduces satisfiability modulo realizability, a SAT-based method for solving existential theory of the reals problems by encoding geometric configurations as SAT instances over abstract order types. Using diversity-driven sampling and a flippability heuristic, they resolve an open problem, proving the largest set of points avoiding empty convex hexagons and heptagons is size 23.
Problems complete for the existential theory of the reals ($\exists \mathbb{R}$) arise throughout discrete geometry. We introduce satisfiability modulo realizability, a SAT-based approach for solving satisfiable instances of $\exists \mathbb{R}$ whose solutions correspond to realizable geometric configurations. Our method encodes an underapproximation of a geometric problem as a SAT instance over abstract order types. Since almost all abstract order types are unrealizable, naive search is infeasible. We guide the search toward realizable order types using diversity-driven sampling, partial realizability feedback, and a novel flippability heuristic that passes only limited information between components. We apply our method to discrete geometry problems and resolve an open problem by showing that the largest set of points avoiding empty convex hexagons and convex heptagons is of size 23.