Toward Satisfiability Modulo Realizability

Andrew Krapivin, Benjamin Przybocki, Marijn J. H. Heule

Problems complete for the existential theory of the reals ($\exists \mathbb{R}$) arise throughout discrete geometry. We introduce satisfiability modulo realizability, a SAT-based a…