Proving Unrealizability for Syntax-Guided Synthesis

TL;DR

This paper introduces a novel method to automatically prove the unrealizability of syntax-guided synthesis problems by encoding them as reachability problems, enhancing the ability to handle complex instances with infinite search spaces.

Contribution

The paper presents a new approach that reduces unrealizability proofs to reachability problems using program encoding, and integrates this into existing SyGuS tools to improve unrealizability detection.

Findings

Proven unrealizability for 59 out of 134 benchmark variants.

Outperforms existing solvers which time out on these benchmarks.

Implemented in the NOPE tool, demonstrating practical effectiveness.

Abstract

Proving Unrealizability for Syntax-Guided Synthesis We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). Existing techniques have quite limited ability to establish unrealizability for general SyGuS instances in which the grammar describing the search space contains infinitely many programs. By encoding the synthesis problem's grammar G as a nondeterministic program P_G, we reduce the unrealizability problem to a reachability problem such that, if a standard program-analysis tool can establish that a certain assertion in P_G always holds, then the synthesis problem is unrealizable. Our method can be used to augment any existing SyGus tool so that it can establish that a successfully synthesized program q is optimal with respect to some syntactic cost -- e.g., q has the fewest possible if-then-else operators. Using known techniques, grammar G can be automatically transformed to generate exactly all programs with lower cost than q -- e.g., fewer conditional expressions. Our algorithm can then be applied to show that the resulting synthesis problem is unrealizable. We implemented the proposed technique in a tool called NOPE. NOPE can prove unrealizability for 59/134 variants of existing linear-integer-arithmetic SyGus benchmarks, whereas all existing SyGus solvers lack the ability to prove that these benchmarks are unrealizable, and time out on them.