Specification and Automatic Verification of Computational Reductions

TL;DR

This paper addresses the problem of validating candidate computational reductions between problems by introducing cookbook reductions, a graphical, modular language built from building blocks like edge, node, and global gadgets. It demonstrates that cookbook reductions can express many classical graph reductions and that, under a linear input order, they preserve NP-hardness via quantifier-free FO interpretations, while also identifying several natural decidable variants of the Reduction? problem. The authors establish decidability results for restricted cookbook reductions (bounded arity with FO-definable target problems and MSO- definable edge gadgets) and show how reductions can be analyzed via FO/MSO-type equivalences of their recipes, enabling automated counterexample generation in teaching contexts. They also discuss a teaching-oriented prototype integrated into Iltis, illustrating the practical utility of the framework for designing, testing, and giving feedback on reductions in introductory computer science courses.

Abstract

We are interested in the following validation problem for computational reductions: for algorithmic problems $P$ and $P^\star$, is a given candidate reduction indeed a reduction from $P$ to $P^\star$? Unsurprisingly, this problem is undecidable even for very restricted classes of reductions. This leads to the question: Is there a natural, expressive class of reductions for which the validation problem can be attacked algorithmically? We answer this question positively by introducing an easy-to-use graphical specification mechanism for computational reductions, called cookbook reductions. We show that cookbook reductions are sufficiently expressive to cover many classical graph reductions and expressive enough so that SAT remains NP-complete (in the presence of a linear order). Surprisingly, the validation problem is decidable for natural and expressive subclasses of cookbook reductions.

Figures (10)

• Figure 1: Collection of algorithmic problems considered in the paper.
• Figure 2: Graphical representations of four reductions. The reductions are applied stepwise, from the top-most step to the bottom-most step. Nodes and edges coloured blue are created in this step, grey nodes and edges were created in a previous step.
• Figure 3: Three reductions formalized as cookbook reductions. Nodes introduced for type $\mathfrak{t}\xspace_{\emptyset}$ are coloured green, nodes and edges introduced for type $\mathfrak{t}\xspace_{ }$ are coloured grey, and nodes and edges introduced for types $\mathfrak{t}\xspace_{ }$ and $\mathfrak{t}\xspace_{ }$ are coloured blue. Compare to Figure \ref{['figure:example:informal-cookbook']}(b), (c), and (d).
• Figure 4: The recipe $\text{recipe}(\rho\xspace)$ for the cookbook reduction of arity $2$ from $3$-Clique to $4$-Clique from Figure \ref{['figure:example:cookbook-reduction']}. There are four unary relations for the types $\mathfrak{t}\xspace_\emptyset$, $\mathfrak{t}\xspace_{ }$, $\mathfrak{t}\xspace_{ }$, and $\mathfrak{t}\xspace_{ }$ of loopless undirected graphs. The dotted edges represent the binary inheritance relation $\approx$.
• Figure 8: Correct node gadgets for reducing HamCycle$_d$ to HamCycle$_u$ with node graphs with at most three nodes.

Theorems & Definitions (24)

• Theorem 1
• Theorem 2
• Corollary 3
• Theorem 4
• Proposition 4
• Proposition 4
• Proposition 5
• Theorem 6
• Lemma 6
• Theorem 7