{"id":"arxiv/2607.02958","url":"https://arxiv.org/abs/2607.02958","tags":["cs.CG","math.CO"],"score":0,"title":"Toward Satisfiability Modulo Realizability","domain":"cs.CG","source":"arxiv","authors":["Andrew Krapivin","Benjamin Przybocki","Marijn J. H. Heule"],"reviews":0,"subject":"cs.CG","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-03","reactions":{}}