论文标题
关于单调可行插值的协议
On Protocols for Monotone Feasible Interpolation
论文作者
论文摘要
可行的插值是证明证据复杂性下限的一般技术。该技术的单调版本以其基本变体转换，用于单调布尔电路的下限，将两个NP组分开以证明复杂性下限。在该技术的广义版本中，使用类似DAG的通信协议代替单调布尔电路。我们研究三种协议并比较其强度。 我们的结果以多项式降低的意义建立了以下关系：具有平等的协议至少与具有不平等的协议和平等协议具有与具有两个不平等的协议相同的强度。已知有不平等方案方案的指数下限。获得平等协议的下限将立即意味着以平等分辨率（R（LIN））分辨率的下限。
Feasible interpolation is a general technique for proving proof complexity lower bounds. The monotone version of the technique converts, in its basic variant, lower bounds for monotone Boolean circuits separating two NP-sets to proof complexity lower bounds. In a generalized version of the technique, dag-like communication protocols are used instead of monotone Boolean circuits. We study three kinds of protocols and compare their strength. Our results establish the following relationships in the sense of polynomial reducibility: Protocols with equality are at least as strong as protocols with inequality and protocols with equality have the same strength as protocols with a conjunction of two inequalities. Exponential lower bounds for protocols with inequality are known. Obtaining lower bounds for protocols with equality would immediately imply lower bounds for resolution with parities (R(LIN)).
