Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
Hu, Q., Cyphert, J., D'Antoni, L., and Reps, T.
We consider the problem of automatically establishing that a given
syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e.,
has no solution).
We formulate the problem of proving that a SyGuS problem is
unrealizable over a finite set of examples as one of solving a set
of equations: the solution yields an overapproximation of the set
of possible outputs that any term in the search space can produce
on the given examples.
If none of the possible outputs agrees with all of the examples, our
technique has proven that the given SyGuS problem is unrealizable.
We then present an algorithm for exactly solving the set of equations
that result from SyGuS problems over linear integer arithmetic (LIA)
and LIA with conditionals (CLIA), thereby showing that LIA and CLIA
SyGuS problems over finitely many examples are decidable.
We implement the proposed technique and algorithms in a tool called
NAY.
NAY can prove unrealizability for 70/132 existing SyGuS benchmarks,
with running times comparable to those of the state-of-the-art tool
NOPE.
Moreover, Nay can solve 11 benchmarks that NOPE cannot solve.
(Click here to access the paper:
PDF.)
University of Wisconsin