Learning from Failure in Program Synthesis: Generalizing and Minimizing Conflicts

Abstract

Program synthesis searches a grammar-defined space for a program that satisfies a user specification. Constraints can significantly reduce this search space. They can either be added manually by the user or derived through conflict analysis, which turns failed candidates into learned constraints. These constraints often retain irrelevant candidate details and accumulate costly redundancy. This thesis extends a conflict-analysis framework with core-guided MUC generalization and constraint-set cleanup. Generalization uses a semantic unsatisfiable core to wildcard irrelevant branches while preserving the candidate root and core nodes, as well as values referenced by core relations. Cleanup minimizes the active constraint set in many ways: by either removing constraints through exact deduplication or subsumption, or by merging constraints through single-differences and cross-relations. We evaluate both extensions on several benchmarks, assessing the reduced search space, constraint set size, runtime, and number of solved problems and used enumerations. At the largest program sizes, generalized MUC reduces enumerations by anywhere between 60 and 99.9%, consistently improving over the previous MUC implementation. Similarly, the strongest cleanup configuration can reduce the mean active constraint population by more than three orders of magnitude. While the new extensions manage to solve slightly more problems, their runtime improvement is negligible. Nonetheless, our extensions show that conflict analysis can learn substantially more general constraints and represent them more compactly.