论文标题
证明复杂性和TFNP的分离
Separations in Proof Complexity and TFNP
论文作者
论文摘要
众所周知，可以通过Sherali-Adams（SA）证明有效模拟解决方案。但是，我们表明，任何此类仿真都需要利用巨大的系数：当系数写成一单元时，SA不能有效地模拟分辨率。我们还表明，无法通过Nullstellensatz（NS）有效地模拟可逆分辨率（MaxSat分辨率的变体）。 这些结果对NP搜索问题产生了影响。首先，我们分别通过Unary-SA，Unary-NS和可逆分辨率来表征PPAD，PPAD，SOPL。其次，我们证明，相对于Oracle，PLS $ \ not \ subseteq $ ppp，sopl $ \ not \ subseteq $ ppa和eopl $ \ not \ subseteq $ ueopl。特别是，与先前的工作一起，这给了1990年代介绍的所有经典TFNP类之间的黑盒关系。
It is well-known that Resolution proofs can be efficiently simulated by Sherali-Adams (SA) proofs. We show, however, that any such simulation needs to exploit huge coefficients: Resolution cannot be efficiently simulated by SA when the coefficients are written in unary. We also show that Reversible Resolution (a variant of MaxSAT Resolution) cannot be efficiently simulated by Nullstellensatz (NS). These results have consequences for total NP search problems. First, we characterise the classes PPADS, PPAD, SOPL by unary-SA, unary-NS, and Reversible Resolution, respectively. Second, we show that, relative to an oracle, PLS $\not\subseteq$ PPP, SOPL $\not\subseteq$ PPA, and EOPL $\not\subseteq$ UEOPL. In particular, together with prior work, this gives a complete picture of the black-box relationships between all classical TFNP classes introduced in the 1990s.
