Constraint Propagation in Program Synthesis

Abstract

Program synthesis is often seen as the holy grail of computer science. A user only needs to provide program specifications and a computer will automatically generate the desired program. This often involves searching for the desired program in the program space, which is like searching for a needle in a haystack. Luckily, there is room for improvement here. Many programs in the program space are redundant and should never be considered. To filter out these redundant programs, we propagated grammar constraints during search using a novel built-in constraint solver. Only programs that satisfy these constraints will be considered as candidates for synthesis. To measure the effectiveness of the solver, we have enumerated several program spaces with and without constraints. Although the amount of filtering largely depends on the concrete grammar and constraints, the results show that constraints can often eliminate $99\%$ of the program space. Accounting for the overhead of propagation, this comes down to a 50-fold improvement in runtime.