Version space algebra (VSA) is an effective data structure for representing program sets and has been extensively used in program synthesis. Despite this success, a crucial shortcoming of VSA-based synthesis is its inefficiency when processing many examples. Given a set of IO examples, a typical VSA-based synthesizer runs by first constructing an individual VSA for each example and then iteratively intersecting these VSAs one by one. However, the intersection of two VSAs can be much larger than the original ones – this effect can accumulate during the iteration, making the VSA scale quickly explode.

In this paper, we aim to reduce the cost of intersecting VSAs in synthesis. We investigate the process of the iterative intersection and observe that, although this process may construct some huge intermediate VSAs, its final VSA is usually small in practice because only a few programs can pass all examples. Utilizing this observation, we propose the scheme of \emph{multi-way intersection}, which directly intersects multiple small VSAs into the final result, thus avoiding the previous bottleneck of constructing huge intermediate VSAs. Besides, since the previous intersection algorithm is inefficient for multiple VSAs, we further design a novel intersection algorithm to avoid most unnecessary VSA nodes involved in the previous algorithm.

We implemented our approach into two SOTA VSA-based synthesizers: a general synthesizer based on FTA and a specialized synthesizer for the string domain based on Blaze. The two implementations are evaluated over 4 different datasets and 994 synthesis tasks. The result shows that Mole significantly boosts the performance of these existing synthesizers, with up to 105 more solved tasks and a speedup of up to $\times 7.36$.