Meta-Complexity 2023
前言：我今年的一月到五月在访问Simons Institute的Meta-Complexity program。有四个大的workshop和断断续续的小talk，一时半会吸收不完！这里会记录一些我觉得有意思的talk
The Hitting Proof System
我们都知道${\sf CNF}\text{-SAT}$是${\sf NP}$-完全的，但是如果给出的${\sf CNF}$是无歧义（unambiguous）的，那么${\sf CNF}\text{-SAT}$是简单的。我们说一个${\sf CNF}$ $C = C_1 \land C_2 \land \dots \land C_m$是无歧义的，当且仅当任意$x\in\{0, 1\}^n$会拒绝至多一个子句$C_{i(x)}$。如果保证了${\sf CNF}$ $C$是无歧义的，那么子句$C_i$会干掉$2^{n-|C_i|}$个输入，所以$C(x) = 1$有解当且仅当$\sum_{i=1}^m 2^{n-|C_i|} < 2^n$。
根据以上事实，我们可以定义一个叫做Hitting的证明系统（propositional proof system）如下。给出一个${\sf CNF}$ $C$，若想证明$C$不可满足，只需要提供一个无歧义的${\sf CNF}$ $C'$，使得$C'$的每个子句$C'_i$都被$C$的某个子句$C_j$覆盖（也就是说$C'_i(x) = 0 \implies C_j(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(4^{\log^3 m})$的树形Resolution证明，而且可以证明$2^{\log^{2-o(1)} m}$大小的下界。对于（非树形）Resolution我们知道得并不多：因为Resolution和树形Resolution有指数分隔，所以Resolution和Hitting也有指数分隔。然而，我们并不知道如何用Resolution模拟Hitting（比如说，如果要检查一个Hitting证明的话，我们需要数数，所以Resolution不一定能干这个事）。
Towards ${\sf P}\ne {\sf NP}$ from Extended Frege Lower Bounds
本文研究的问题是：在什么情况下，证明复杂度中的下界能够推出计算复杂度中的下界？如果某些定理在Extended Frege中需要超多项式大小的证明，能否推出${\sf NP}\not\subseteq {\sf P}/_{\rm poly}$？某种意义上来说，Extended Frege刻画的是“${\sf P}/_{\rm poly}$-reasoning”，所以Extended Frege的下界理应能够推出${\sf P}/_{\rm poly}$的下界，但是我们不知道任何的formal connection。事实上，“证明复杂度下界 $\implies$ 计算复杂度下界”的例子极为少见（例如Ideal Proof System）。
这篇文章将这个问题与“witnessing for ${\rm SAT}$”联系了起来。假设${\sf NP}\not\subseteq {\sf P}/_{\rm poly}$，那么$\text{search-}{\rm SAT}$需要超多项式的电路复杂度。我们能不能构造一个多项式时间的“refuter”${\cal R}$，使得对任意多项式大小的电路$C$，${\cal R}(C)$输出$(\varphi, x)$，使得$\varphi(x) = 1$但是$C(\varphi)$无法成功找到满足$\varphi$的输入？如果我们有更强的假设的话，这样的${\cal R}$是可以构造出来的：假设单向函数存在并且${\sf E}\not\subseteq {\sf SIZE}[2^{0.1n}]$。那么我们用$C$来对单向函数求逆（一定会失败），就可以得到一个随机多项式时间的refuter；再用${\sf E}\not\subseteq {\sf SIZE}[2^{0.1n}]$来把这个refuter去随机化即可。但是能不能用更弱的假设推出这样的refuter的存在性？
假设${\sf S}^1_2$能够推出这类refuter的存在性，那么我们可以从Extended Frege的复杂度下界推出${\sf NP}\not\subseteq {\sf P}/_{\rm poly}$。原因很简单：假设${\sf NP}\subseteq {\sf P}/_{\rm poly}$。如果${\sf S}^1_2$能够证明${\cal R}$存在，那么由propositional translation，Extended Frege也可以证明${\cal R}$存在。对于任意$\varphi$，如果我们想在Extended Frege中证明$\varphi$是不可满足的，我们只需要（1）提供一个解决${\rm SAT}$的多项式大小的电路$C$（注意我们假设了${\sf P} = {\sf NP}$），然后（2）跑${\cal R}(C)$来验证${\cal R}$失败了，从而$C$真的解决了${\rm SAT}$，最后（3）跑$C(\varphi)$然后验证$\varphi$不可满足。
一个直接推论是：如果${\sf S}^1_2$中可以排除Heuristica和Pessiland（也就是证明${\sf NP}\not\subseteq {\sf P}/_{\rm poly}\implies \text{OWF}$）并且证明去随机化（比如${\sf E}\not\subseteq {\sf SIZE}[2^{0.1n}]$），那么Extended Frege的复杂度下界能够推出电路复杂度下界。话说回来，我其实觉得这个假设很强。。。“排除Heuristica和Pessiland”与“去随机化”听上去都是很靠谱的假设，但是我对${\sf S}^1_2$能否证明这些东西持观望态度（
Frontiers of Proof Complexity Lower Bounds via Algebraic Complexity & Open Problems
我觉得这是个非常有意思的topic！Iddo讨论了代数证明系统（algebraic proof systems）的复杂度下界的问题（重点讨论了IPS）。布尔证明系统（例如Frege和Extended Frege）证明的是${\sf CNF}$ $\bigwedge_{i=1}^mC_i(x)$的不可满足性；代数证明系统证明的是多项式方程组$\{f_i(x) = 0\}_{i=1}^m$不存在解。我们能把任意${\sf CNF}$代数化（algebrization）（例如把$a\lor b$换成$a+b-ab$，把$\bar{x}$换成$(1-x)$），所以当我们在说“IPS比Extended Frege强”的时候，我们实际上说的是：如果$F$是一个${\sf CNF}$且有复杂度为$s$的Extended Frege refutation，那么把$F$代数化之后得到的方程组也有复杂度为${\rm poly}(s)$的IPS refutation。
Iddo指出：如果我们不考虑“由${\sf CNF}$代数化得来的方程组”，而是放宽眼界考虑最一般的方程组的话，我们可以证明很强的代数系统的复杂度下界！比如说：
- 在有理数域上的常数深度IPS（$\text{depth-}O(1)$ ${\sf IPS}_{\mathbb{Q}}$）已经比${\sf TC}^0\text{-Frege}$要强一些了（注：我不确定出处在哪里，可能是这篇但是存疑）；
- ${\sf TC}^0\text{-Frege}$的复杂度下界是证明复杂度中很困难的问题；
- 我们已经有了不错的$\text{depth-}O(1)$ ${\sf IPS}_{\mathbb{Q}}$的下界（这篇、这篇）。
上述$\text{depth-}O(1)$ ${\sf IPS}_{\mathbb{Q}}$的下界并不能推出${\sf TC}^0\text{-Frege}$的下界，因为这些下界是对一般的方程组证明的，而不是对“由${\sf CNF}$代数化得来的方程组”证明的！
Iddo给出了更多的例子：
- 假设Shub-Smale猜想成立，那么IPS甚至无法（多项式长度地）证明“任意二进制数都是非负的”——考虑方程$\sum_{i=0}^{n-1}2^ix_i = -1$，再加上Boolean axioms $\{x_i(1-x_i) = 0\}_{i=1}^n$，IPS需要超多项式的证明复杂度才能证明这个方程组无解。
- 无条件地，上述方程组在Extended Polynomial Calculus内需要$2^{\Omega(n)}$-bit的证明复杂度（也就是说，证明可能只用到寥寥几个“高精度数”，但是如果想把整个证明表示成0/1串的话需要$2^{\Omega(n)}$位才能写下来）。
- （在有限域中）${\sf VP} \ne {\sf VNP}$当且仅当${\sf IPS}$无法证明“${\sf IPS}$无法证明${\sf VP} \ne {\sf VNP}$”。（注意：在这个结果中，我们需要把“${\sf VP}\ne {\sf VNP}$”和“${\sf IPS}$无法证明blabla”都写成${\sf CNF}$的形式。）
对于只有一个axiom的方程组来说，我们可以用如下方法证${\sf IPS}$下界。假设该方程为$f(x) = 0$。（当然，我们还要加上Boolean axioms $\{x_i(1-x_i) = 0\}_{i=1}^n$。）那么任何在$x\in\{0, 1\}^n$上满足$g(x)f(x) = 1$的多项式$g$都是一个合法的${\sf IPS}$证明。也就是说，${\sf IPS}$下界可以规约到$\frac{1}{f(x)}$的代数（电路）复杂度的下界——但是和一般的代数复杂度有一个区别！我们想证明$\frac{1}{f(x)}$作为一个函数的复杂度下界，而不是作为一个formal polynomial的复杂度下界——所以这个复杂度下界会稍稍难搞一些。不过据说现在的无条件${\sf IPS}$下界都是这么证来的。
但是如果有多于一个axiom呢？我们想证明对任意$g_1, g_2$使得$g_1(x) f_1(x) + g_2(x) f_2(x) = 1$，$g_1$和$g_2$的复杂度会比较大。这个我们就不会了。Iddo在最后把这个问题作为open problem列出，感觉很有意思。
（一月份刚来到Simons的模样）
（五月份的模样，马上就要离开了捏）
（四月的樱花盛开）
评论 (0)