Decomposition-Based Synthesis for Applying Divide-and-Conquer-Like Algorithmic Paradigms

TL;DR

This paper introduces AutoLifter, a novel synthesis tool that automatically applies divide-and-conquer-like paradigms without relying on syntax-based transformations, effectively simplifying complex program synthesis tasks.

Contribution

AutoLifter employs two new decomposition methods to enable paradigm application without syntax restrictions, improving efficiency and scalability in program synthesis.

Findings

AutoLifter solves 82 out of 96 tasks within 20 seconds on average.

It significantly outperforms existing approaches in applying D&C-like paradigms.

The methods reduce the complexity of large-scale program synthesis tasks.

Abstract

Algorithmic paradigms such as divide-and-conquer (D&C) are proposed to guide developers in designing efficient algorithms, but it can still be difficult to apply algorithmic paradigms to practical tasks. To ease the usage of paradigms, many research efforts have been devoted to the automatic application of algorithmic paradigms. However, most existing approaches to this problem rely on syntax-based program transformations and thus put significant restrictions on the original program. In this paper, we study the automatic application of D&C and several similar paradigms, denoted as D&C-like algorithmic paradigms, and aim to remove the restrictions from syntax-based transformations. To achieve this goal, we propose an efficient synthesizer, named AutoLifter, which does not depend on syntax-based transformations. Specifically, the main challenge of applying algorithmic paradigms is from the large scale of the synthesized programs, and AutoLifter addresses this challenge by applying two novel decomposition methods that do not depend on the syntax of the input program, component elimination and variable elimination, to soundly divide the whole problem into simpler subtasks, each synthesizing a sub-program of the final program and being tractable with existing 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 20.17 seconds, significantly outperforming existing approaches.