Program Synthesis as Dependency Quantified Formula Modulo Theory

Abstract

Given a specification φ(X, Y ) over inputs X and output Y , defined over a background theory T, the problem of program synthesis is to design a pro- gram f such that Y = f (X) satisfies the specification φ. Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant approach for pro- gram synthesis where in addition to the specification φ, the end-user also speci- fies a grammar L to aid the underlying synthesis engine. This paper investigates the feasibility of synthesis techniques without grammar, a sub-class defined as T-constrained synthesis. We show that T-constrained synthesis can be reduced to DQF(T), i.e., to the problem of finding a witness of a Dependency Quantified Formula Modulo The- ory. When the underlying theory is the theory of bitvectors, the corresponding DQF(BV) problem can be further reduced to Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF solving to design DQBF- based synthesizers that outperform the domain-specific synthesis techniques, thereby positioning DQBF as a core representation language for program synthesis.

Publication
International Workshop on Quantified Boolean Formulas and Beyond, co-located with SAT

Next
Previous