Program Synthesis as Dependency Quantified Formula Modulo Theory

Given a specification over inputs X and output Y, defined over a background theory T, the problem of program synthesis is to design a program P such that Y=P(X) satisfies the specification. It can be considered a T-constrained synthesis as we deal with a specific theory. 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 Theory.

Furthermore, when the underlying theory is the theory of bit-vectors, the corresponding DQF(BV) problem can be further reduced to Dependency Quantified Boolean Formulas. We rely on the progress in DQBF solving to design DQBF-based synthesizers that outperform the domain-specific program synthesis techniques, thereby positioning DQBF as a core representation language for program synthesis. Our empirical analysis shows that the general-purpose DQBF solvers perform on par with domain-specific synthesis techniques.