# Modelling Program Spaces in Program Synthesis with Constraints

arXiv: https://arxiv.org/abs/2508.00005 · HTML: https://mlsanity.com/paper/2508.00005/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 39 references that are in the map.
- First posted on arXiv 10 Jul 2025.

## Builds on (most cited first, 9 of 9)

- [DeepCoder: Learning to Write Programs](https://mlsanity.com/paper/1611.01989/) (2016)
- [Multi-shot ASP solving with clingo](https://mlsanity.com/paper/1705.09811/) (2017)
- [Inductive logic programming at 30: a new introduction](https://mlsanity.com/paper/2008.07912/) (2020)
- [Learning programs by learning from failures](https://mlsanity.com/paper/2005.02259/) (2020)
- [Program Synthesis using Conflict-Driven Learning](https://mlsanity.com/paper/1711.08029/) (2017)
- [Logical reduction of metarules](https://mlsanity.com/paper/1907.10952/) (2019)
- [Just-in-Time Learning for Bottom-Up Enumerative Synthesis](https://mlsanity.com/paper/2010.08663/) (2020)
- [Rewrite Rule Inference Using Equality Saturation](https://mlsanity.com/paper/2108.10436/) (2021)
- [Semantics-Guided Synthesis](https://mlsanity.com/paper/2008.09836/) (2020)

## Built on by (most cited first, 1 of 1)

- [Herb.jl: A Unifying Program Synthesis Library](https://mlsanity.com/paper/2510.09726/) (2025)

## Abstract (arXiv)

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.