Combining the Smallest Subset of Programs from Enumerative Search with Decision Trees

Abstract

Program synthesis aims to automatically generate programs that fulfil user-specified constraints. The field has developed many different techniques to enable program synthesis in various application domains. This work will focus on the enumerative approach, which iteratively explores solutions in the program space from the smallest programs to larger ones. This technique works well on small to medium-sized problems. With the exponentially growing program space performance of the enumerative solver rapidly declines.

This work aims to generalize the divide and conquer approach to combine partial solutions found by an enumerative solver. Firstly by forming the smallest subset that satisfies every example in a problem and then using decision trees to find the final program that satisfies all input-output examples. Our prototype named SubsetDT will be incorporated into the Julia library Herb.jl which provides a flexible environment for testing and developing program synthesis ideas.

This methodology was evaluated on SyGuS competition benchmarks from two different tracks. Results indicate that the use of a decision tree on top of enumeration search improves solver performance by 33% on the string manipulation track and significantly on the bit-vector manipulation track, though both tracks showed some overfitting. The experiments demonstrate that the SubsetDT algorithm can substantially improve enumeration solvers, its effectiveness highly depends on the iterators used.