Generalizing Conflict Analysis in Program Synthesis
O.A.R. Poeth (TU Delft - Electrical Engineering, Mathematics and Computer Science)
S. Dumančić – Mentor (TU Delft - Algorithmics)
M.A. Costea – Graduation committee member (TU Delft - Programming Languages)
N. Yorke-Smith – Graduation committee member (TU Delft - Algorithmics)
T.R. Hinnerichs – Graduation committee member (TU Delft - Algorithmics)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Program synthesis aims to solve problems through coding by removing the need to write the programs yourself.
Given the grammar and problem specification, it aims to find a program that adheres to your problem specification.
This is done by iterating over many failing programs until a solution that adheres to the problem specification is found.
Conflict analysis automatically takes these failing solutions and learns new constraints to make the search more efficient.
Unfortunately, many conflict analysis techniques are heavily specialized.
They are difficult to apply to diverse problems or when trying to use a different search algorithm.
In this work, we present a modular framework in which these techniques can be implemented in a generalized way and applied independently to different problems and solvers, while having the ability to share generated constraints and parsed information.
We identify two distinct conflict types and show how to use semantics in conflict analysis effectively.
The framework is evaluated on two diverse domains; it prunes up to 96\% of the search space, where combining techniques can further improve its average effectiveness.
Domain applicability for the techniques has to be considered for optimal framework performance.
Compared to an enumeration solver, the framework shows marginal improvements on a real-world benchmark.
While the framework's overhead needs improvement, its modularity allows for comparison between solvers, problems, and conflict analysis techniques.