Meta-Complexity 2023

r_64 posted @ 2023年5月14日 11:10 in 未分类 , 244 阅读

朝着变小的公园走去

前言:我今年的一月到五月在访问Simons InstituteMeta-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的模样)

(五月份的模样,马上就要离开了捏)

(四月的樱花盛开)


登录 *


loading captcha image...
(输入验证码)
or Ctrl+Enter