论文标题
精确而近似的方法，用于证明语法引导的合成问题的不实现性
Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
论文作者
论文摘要
我们认为自动确定给定语法指导合成（SYGUS）问题的问题是不可交通的（即没有解决方案）。我们提出了一个问题，即证明Sygus问题在有限的示例中是无法实现的，因为解决了一组方程之一：该解决方案会产生过度应用搜索空间中任何术语可以在给定示例上产生的可能输出的过度应用。如果可能的输出都不符合所有示例，那么我们的技术证明了给定的Sygus问题是不可交通的。然后，我们提出了一种算法，用于精确求解由线性整数算术（LIA）和有条件（CLIA）的Sygus问题引起的一组方程组，从而表明LIA和CLIA Sygus问题超过了许多示例，这是可以决定的。我们在称为Nay的工具中实现了提出的技术和算法。 NAY可以证明70/132现有的Sygus基准标准，其运行时间与最先进的工具NOPE相当。此外，否可以解决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.
