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

TL;DR

The paper introduces AutoLifter, a decomposition-based framework for automatically applying D&C-like algorithmic paradigms to practical programming tasks, avoiding restrictive syntax-based transformations. It formalizes lifting problems, proposes two decomposition strategies (component elimination and variable elimination), and employs inductive synthesis with CEGIS for leaf subtasks. Empirical evaluation on 96 tasks shows AutoLifter solving $82$ tasks with an average synthesis time of $20.01$ seconds, outperforming general-purpose and specialized baselines and with competitive or better resulting program efficiency. The work demonstrates that lifting-based decomposition, together with observational covering and a principled efficiency regime, yields practical, scalable synthesis for a broad class of algorithmic paradigms, with potential extensions to additional paradigms and operator inference.

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.

Figures (19)

• Figure 1: aux and comb for incrementalization
• Figure 2: Maximum segment sum
• Figure 3: An example of calculating mss.
• Figure 4: An example of calculating mps.
• Figure 5: The extended program $\mathcal{L}_{\textit{aux}}^{\textit{mss}}$ of $\hbox{\it aux}$ for the mss example, where semantics of $\hbox{\it mps}$ and $\hbox{\it mts}$ are explained using a Python-like syntax.

Theorems & Definitions (18)

• definition 1: Lifting Problem
• Theorem 4.1: Soundness
• proof
• definition 2: Size-Limited Unrealizable Rate
• definition 3: Mismatch Factor
• Theorem 4.2: Upper Bound on the Unrealizable Rate
• Theorem 4.3: Unrealizable Rate Under the Compressing Property
• Theorem 4.4: Minimality
• Theorem A.1: Theorem \ref{['theorem:soundness']}
• proof