电路评估、扩展分辨和总NP搜索问题的一致性
Consistency of circuit evaluation, extended resolution and total NP search problems
摘要：
我们认为集$Γ(n,s,k)$的狭窄条款表示，没有定义的大小$s$电路与$n$的输入是可反驳的$k$步骤中的分辨率R。我们表明，每一个CNF短期内可反驳的扩展R，ER，可以很容易地减少到一个实例的$Γ(0,s,k)$（与$s,k$取决于ER-反驳的大小），特别是，$Γ(0,s,k)$解释为一个相对化的NP搜索问题是完整的所有这些问题证明总有界算术理论$V^1_1$。我们使用的思想，隐式证明定义从$Γ(0,s,k)$一个非相对化NP搜索问题$iΓ$，我们表明，它是完整的所有这些问题证明在有界算术理论$V^1_2$。可在$S^1_2$中定义减少。我们指出如何类似的结果可以证明其他一些命题证明系统和有界算术理论，以及如何建设可以用来定义特定的随机不可满足的公式，我们制定了两个开放的问题。
英文摘要：
We consider sets $Γ(n,s,k)$ of narrow clauses expressing that no definition of a size $s$ circuit with $n$ inputs is refutable in resolution R in $k$ steps. We show that every CNF shortly refutable in Extended R, ER, can be easily reduced to an instance of $Γ(0,s,k)$ (with $s,k$ depending on the size of the ER-refutation) and, in particular, that $Γ(0,s,k)$ when interpreted as a relativized NP search problem is complete among all such problems provably total in bounded arithmetic theory $V^1_1$. We use the ideas of implicit proofs to define from $Γ(0,s,k)$ a non-relativized NP search problem $iΓ$ and we show that it is complete among all such problems provably total in bounded arithmetic theory $V^1_2$. The reductions are definable in $S^1_2$. We indicate how similar results can be proved for some other propositional proof systems and bounded arithmetic theories and how the construction can be used to define specific random unsatisfiable formulas, and we formulate two open problems about them.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
