We propose a fully automated method that takes as input an iterative or recursive reference implementation and produces divide-and-conquer implementations that are functionally equivalent to the input. Three interdependent components have to be synthesized as part of this task: a function that divides the original problem instance, a function that solves each sub-instance, and a function that combines the results of sub-computations. We propose a methodology that splits this task into three successive synthesis phases, each with a substantially reduced state space compared to the monolithic task. The three subproblems are therefore substantially more tractable than the original problem and can be individually solved. We have implemented the methodology as a program synthesis tool, called DiscuRe, and demonstrate the efficacy of our approach by synthesizing highly nontrivial divide-and-conquer implementations of a set of benchmarks fully automatically.

The Appendix referred to in the submission has been submitted as anonymized Supplemental Text.