Meta-Complexity 2023

“朝着变小的公园走去”

前言：我今年的一月到五月在访问Simons Institute的Meta-Complexity program。有四个大的workshop和断断续续的小talk，一时半会吸收不完！这里会记录一些我觉得有意思的talk

The Hitting Proof System

我们都知道CNF-SAT是NP-完全的，但是如果给出的CNF是无歧义（unambiguous）的，那么CNF-SAT是简单的。我们说一个CNF C=C1∧C2∧⋯∧Cm是无歧义的，当且仅当任意x∈{0,1}n会拒绝至多一个子句Ci(x)。如果保证了CNF C是无歧义的，那么子句Ci会干掉2n−|Ci|个输入，所以C(x)=1有解当且仅当∑mi=12n−|Ci|<2n。

根据以上事实，我们可以定义一个叫做Hitting的证明系统（propositional proof system）如下。给出一个CNF C，若想证明C不可满足，只需要提供一个无歧义的CNF C′，使得C′的每个子句C′i都被C的某个子句Cj覆盖（也就是说C′i(x)=0⟹Cj(x)=0），并且C′不可满足。如果我们想要验证一个证明C′，那么我们需要验证（1）C′是无歧义的，（2）C′的每个子句都被C的某个子句覆盖，（3）C′是不可满足的；这三条都可以在多项式时间内验证，所以Hitting是一个标准的Cook-Reckhow证明系统。我们说C的Hitting证明复杂度就是C′的大小（子句个数）。

作为一个证明系统，Hitting的复杂度和树形（tree-like）Resolution的复杂度有着紧密的关联。首先，多项式大小的树形Resolution证明可以改写成多项式大小的Hitting证明。反方向需要quasi-poly：大小为m的Hitting证明可以改写为大小为O(4log3m)的树形Resolution证明，而且可以证明2log2−o(1)m大小的下界。对于（非树形）Resolution我们知道得并不多：因为Resolution和树形Resolution有指数分隔，所以Resolution和Hitting也有指数分隔。然而，我们并不知道如何用Resolution模拟Hitting（比如说，如果要检查一个Hitting证明的话，我们需要数数，所以Resolution不一定能干这个事）。

Towards P≠NP from Extended Frege Lower Bounds

本文研究的问题是：在什么情况下，证明复杂度中的下界能够推出计算复杂度中的下界？如果某些定理在Extended Frege中需要超多项式大小的证明，能否推出NP⊈P/poly？某种意义上来说，Extended Frege刻画的是“P/poly-reasoning”，所以Extended Frege的下界理应能够推出P/poly的下界，但是我们不知道任何的formal connection。事实上，“证明复杂度下界 ⟹ 计算复杂度下界”的例子极为少见（例如Ideal Proof System）。

这篇文章将这个问题与“witnessing for SAT”联系了起来。假设NP⊈P/poly，那么search-SAT需要超多项式的电路复杂度。我们能不能构造一个多项式时间的“refuter”R，使得对任意多项式大小的电路C，R(C)输出(φ,x)，使得φ(x)=1但是C(φ)无法成功找到满足φ的输入？如果我们有更强的假设的话，这样的R是可以构造出来的：假设单向函数存在并且E⊈SIZE[20.1n]。那么我们用C来对单向函数求逆（一定会失败），就可以得到一个随机多项式时间的refuter；再用E⊈SIZE[20.1n]来把这个refuter去随机化即可。但是能不能用更弱的假设推出这样的refuter的存在性？

假设S12能够推出这类refuter的存在性，那么我们可以从Extended Frege的复杂度下界推出NP⊈P/poly。原因很简单：假设NP⊆P/poly。如果S12能够证明R存在，那么由propositional translation，Extended Frege也可以证明R存在。对于任意φ，如果我们想在Extended Frege中证明φ是不可满足的，我们只需要（1）提供一个解决SAT的多项式大小的电路C（注意我们假设了P=NP），然后（2）跑R(C)来验证R失败了，从而C真的解决了SAT，最后（3）跑C(φ)然后验证φ不可满足。

一个直接推论是：如果S12中可以排除Heuristica和Pessiland（也就是证明NP⊈P/poly⟹OWF）并且证明去随机化（比如E⊈SIZE[20.1n]），那么Extended Frege的复杂度下界能够推出电路复杂度下界。话说回来，我其实觉得这个假设很强。。。“排除Heuristica和Pessiland”与“去随机化”听上去都是很靠谱的假设，但是我对S12能否证明这些东西持观望态度（

Frontiers of Proof Complexity Lower Bounds via Algebraic Complexity & Open Problems

我觉得这是个非常有意思的topic！Iddo讨论了代数证明系统（algebraic proof systems）的复杂度下界的问题（重点讨论了IPS）。布尔证明系统（例如Frege和Extended Frege）证明的是CNF ⋀mi=1Ci(x)的不可满足性；代数证明系统证明的是多项式方程组{fi(x)=0}mi=1不存在解。我们能把任意CNF代数化（algebrization）（例如把a∨b换成a+b−ab，把ˉx换成(1−x)），所以当我们在说“IPS比Extended Frege强”的时候，我们实际上说的是：如果F是一个CNF且有复杂度为s的Extended Frege refutation，那么把F代数化之后得到的方程组也有复杂度为poly(s)的IPS refutation。

Iddo指出：如果我们不考虑“由CNF代数化得来的方程组”，而是放宽眼界考虑最一般的方程组的话，我们可以证明很强的代数系统的复杂度下界！比如说：

• 在有理数域上的常数深度IPS（depth-O(1) IPSQ）已经比TC0-Frege要强一些了（注：我不确定出处在哪里，可能是这篇但是存疑）；
• TC0-Frege的复杂度下界是证明复杂度中很困难的问题；
• 我们已经有了不错的depth-O(1) IPSQ的下界（这篇、这篇）。

上述depth-O(1) IPSQ的下界并不能推出TC0-Frege的下界，因为这些下界是对一般的方程组证明的，而不是对“由CNF代数化得来的方程组”证明的！

Iddo给出了更多的例子：

• 假设Shub-Smale猜想成立，那么IPS甚至无法（多项式长度地）证明“任意二进制数都是非负的”——考虑方程∑n−1i=02ixi=−1，再加上Boolean axioms {xi(1−xi)=0}ni=1，IPS需要超多项式的证明复杂度才能证明这个方程组无解。
• 无条件地，上述方程组在Extended Polynomial Calculus内需要2Ω(n)-bit的证明复杂度（也就是说，证明可能只用到寥寥几个“高精度数”，但是如果想把整个证明表示成0/1串的话需要2Ω(n)位才能写下来）。
• （在有限域中）VP≠VNP当且仅当IPS无法证明“IPS无法证明VP≠VNP”。（注意：在这个结果中，我们需要把“VP≠VNP”和“IPS无法证明blabla”都写成CNF的形式。）

对于只有一个axiom的方程组来说，我们可以用如下方法证IPS下界。假设该方程为f(x)=0。（当然，我们还要加上Boolean axioms {xi(1−xi)=0}ni=1。）那么任何在x∈{0,1}n上满足g(x)f(x)=1的多项式g都是一个合法的IPS证明。也就是说，IPS下界可以规约到1f(x)的代数（电路）复杂度的下界——但是和一般的代数复杂度有一个区别！我们想证明1f(x)作为一个函数的复杂度下界，而不是作为一个formal polynomial的复杂度下界——所以这个复杂度下界会稍稍难搞一些。不过据说现在的无条件IPS下界都是这么证来的。

但是如果有多于一个axiom呢？我们想证明对任意g1,g2使得g1(x)f1(x)+g2(x)f2(x)=1，g1和g2的复杂度会比较大。这个我们就不会了。Iddo在最后把这个问题作为open problem列出，感觉很有意思。

（一月份刚来到Simons的模样）

（五月份的模样，马上就要离开了捏）

（四月的樱花盛开）