Modelling Program Spaces in Program Synthesis with Constraints

TL;DR

This paper introduces BART, a solver that uses syntactic constraints to efficiently model and prune large program spaces in synthesis, leading to faster enumeration and more feasible solutions.

Contribution

The work presents a novel approach to model program spaces with syntactic constraints, improving search efficiency in program synthesis.

Findings

Constraints eliminate up to 99% of program space

Modeling program spaces reduces enumeration time significantly

BART efficiently propagates and solves syntactic constraints

Abstract

A core challenge in program synthesis is taming the large space of possible programs. Since program synthesis is essentially a combinatorial search, the community has sought to leverage powerful combinatorial constraint solvers. Here, constraints are used to express the program semantics, but not as a potentially potent tool to remove unwanted programs. Recent inductive logic programming approaches introduce constraints on the program's syntax to be synthesized. These syntactic constraints allow for checking and propagating a constraint without executing the program, and thus for arbitrary operators. In this work, we leverage syntactic constraints to model program spaces, defining not just solutions that are feasible, but also ones that are likely useful. To demonstrate this idea, we introduce BART, a solver that efficiently propagates and solves these constraints. We evaluate BART on program space enumeration tasks, finding that the constraints eliminate up to 99 percent of the program space, and that modeling program spaces significantly reduces enumeration time.