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.
翻译:我们关注计算归约的以下验证问题:对于算法问题 $P$ 和 $P^\star$,给定的候选归约是否确实是从 $P$ 到 $P^\star$ 的归约?不出所料,即使对于限制性很强的归约类,该问题也是不可判定的。这引出了一个问题:是否存在一种自然、表达能力强的归约类,其验证问题可以通过算法方式解决?我们通过引入一种易于使用的计算归约图形化规范机制(称为烹饪书归约)对这个问题给出了肯定回答。我们证明,烹饪书归约具有足够的表达能力,能够涵盖许多经典的图归约,并且其表达能力足以使 SAT 在(线性序存在的情况下)保持 NP 完全性。令人惊讶的是,对于烹饪书归约中自然且表达能力强的子类,其验证问题是可判定的。