计算归约的规范与自动验证
Specification and Automatic Verification of Computational Reductions
AI总结：
本文提出 cookbook reductions 这一图形化归约规范机制，证明其表达力足以覆盖经典图归约并保持 SAT 的 NP 完全性，同时验证问题在自然子类上是可判定的。
摘要：
我们关注计算归约的如下验证问题：对于算法问题 $P$ 和 $P^\star$，给定的候选归约是否确实是从 $P$ 到 $P^\star$ 的归约？毫不意外，即使对于非常受限的归约类，该问题也是不可判定的。这引出一个问题：是否存在一个自然且表达能力强的归约类，使得验证问题可以被算法化地处理？我们通过引入一种易于使用的计算归约图形化规范机制——cookbook reductions（食谱式归约）来正面回答该问题。我们证明 cookbook reductions 的表达能力足以覆盖许多经典图归约，并且其表达能力足以使 SAT 在存在线性序的情况下仍保持 NP 完全性。令人惊讶的是，对于 cookbook reductions 的自然且表达能力强的子类，验证问题是可判定的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
