证明句法引导综合问题不可实现性的精确和近似方法
Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
摘要：
我们考虑自动建立给定的语法引导合成（SyGuS）问题是不可实现的（即，没有解决办法）。我们制定的问题，证明一个SyGuS的问题是不可实现的一组有限的例子之一，解决一组方程：解决方案产生一个overapproximation的一组可能的输出，任何项在搜索空间可以产生的给定的例子。如果没有一个可能的输出与所有的例子一致，我们的技术已经证明了给定的SyGuS问题是不可实现的。然后，我们提出了一个算法，精确求解的方程组，导致SyGuS问题的线性整数算术（LIA）和LIA与条件（CLIA），从而表明，LIA和CLIA SyGuS问题超过100个例子是可判定的。我们在一个名为Nay的工具中实现了所提出的技术和算法。Nay可以证明70/132现有SyGuS基准测试的不可实现性，其运行时间与最先进的工具Nope相当。此外，Nay可以解决Nope无法解决的11个基准。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
