电路求值、扩展归结与全 NP 搜索问题的一致性

我们考虑窄子句集合 $\Gamma(n,s,k)$，其表达：大小为 $s$、输入为 $n$ 的电路的定义不能在归结 R 的 $k$ 步内被反驳。我们证明，在扩展归结 ER 中可短时反驳的每一个 CNF 都能轻易归约到 $\Gamma(0,s,k)$ 的一个实例（其中 $s,k$ 依赖于 ER 反驳的大小）；特别地，当 $\Gamma(0,s,k)$ 被解释为相对化 NP 搜索问题时，它在有界算术理论 $V^1_1$ 中可证全的所有此类问题中是完备的。我们利用隐式证明的思想从 $\Gamma(0,s,k)$ 定义一个非相对化 NP 搜索问题 $i\Gamma$，并证明它在有界算术理论 $V^1_2$ 中可证全的所有此类问题中是完备的。这些归约在 $S^1_2$ 中可定义。我们指出，对于其他一些命题证明系统和有界算术理论也可证明类似结果，且该构造可用于定义特定的随机不可满足公式，我们还提出了关于它们的两个开放问题。