Divide and Conquer Divide-and-Conquer -- Inductive Synthesis for D&C-Like Algorithmic Paradigms

Algorithmic paradigms such as divide-and-conquer (D&C) are proposed to guide the design of efficient algorithms, but applying them to optimize existing programs is difficult. Therefore, many research efforts have been devoted to the automatic application of algorithmic paradigms. However, most existing approaches to this problem are based on deductive methods and thus put significant restrictions on how the original program is implemented. To overcome this limitation, we study the automatic application of paradigms as an oracle-guided inductive synthesis problem, where the synthesizer only invokes the original program as a black-box oracle or uses a given verifier to verify the correctness of candidate programs. Such a synthesizer puts no restriction on the original program and thus overcomes the limitation of deductive approaches. We notice that the application tasks of various paradigms have a similar form as that of D&C. We denote these paradigms as D&C-like paradigms, unify their application tasks into a novel type of synthesis problems, named lifting problems, and propose an efficient inductive synthesizer AutoLifter for lifting problems. The main challenge of solving lifting problems is from the usually large scale of efficient algorithms. To overcome this challenge, we divide and conquer lifting problems. We devise two novel decomposition methods, component elimination and variable elimination, to soundly divide a lifting problem into simpler subtasks, each tractable with existing inductive synthesizers. We evaluate AutoLifter on 96 programming tasks related to 6 different algorithmic paradigms. AutoLifter solves 82/96 tasks with an average time cost of 6.53 seconds, significantly outperforming existing approaches.