往期文章：

• 【计算复杂性理论】证明复杂性（Proof Complexity）（一）：简介
  
• 【计算复杂性理论】证明复杂性（二）：归结（Resolution）与扩展归结（Extended Resolution）证明系统
• 【计算复杂性理论】证明复杂性（三）：弗雷格（Frege）与扩展弗雷格（Extended Frege）证明系统
• 【计算复杂性理论】证明复杂性（四）：相继式演算（Sequent Calculus）
• 【计算复杂性理论】证明复杂性（五）：量化命题演算（Quantified Propositional Calculus）
  
• 【计算复杂性理论】证明复杂性（六）：其他证明系统简介
  
• 【计算复杂性理论】证明复杂性（七）：有界算术（Bounded Arithmetic）与IΔ₀理论
• 【计算复杂性理论】证明复杂性（八）：命题鸽巢原理（Propositional Pigeonhole Principle）的指数级归结下界

看完上期文章的小伙伴们恐怕都觉得：这么长的证明，谁能看懂啊？确实，那篇文章是证明这个下界的第一篇文章，其方法的确很繁杂。不过，这个问题有很简短_{（其实可能也不算简短，但比上一个要简短的）}的证明。这个证明出自Paul Beame和Toniann Pitassi 1996年的论文Simplified and Improved Resolution Lower Bounds，他也被收录进了《计算复杂性：现代方法》中。它给出的证明步数下界，$\Omega \left(2^{\frac{n}{20}}\right)$，比Haken的论文还要好。

对于鸽巢原理等术语的定义，请参阅往期文章。

一、整体框架

首先我们定义一个概念：关键赋值（和上期文章的定义一样），就是舍弃一只鸽子、为其他所有鸽子安排好住处的赋值。还是一样，设$n$为鸽子的个数，$n-1$为巢的个数，共有$n(n-1)$个变量，关键赋值使得其中$n-1$个变量为$1$，其余变量都为$0$。我们将会在关键赋值上讨论问题。

我们将会重点关系证明的宽度，也就是证明中一个子句最多包含了多少个文字。对于一个证明，我们想办法把它的宽子句都消除，具体方法是找到一个能消除宽子句最多的文字使其赋值为$1$，就可以成比例地消除宽子句，消除之多$O(\log S)$次后就没有宽子句了（$S$是证明的步数，它大于等于宽子句的个数）。如果$S$很小的话，消除的步数很少，$n$就没有消掉多少，只消了一部分，这样我们最后就得到了一个对${\mathrm{PHP}}_{n^{\prime }}^{n^{\prime }-1}$的窄证明（$n^{\prime }$是消除了这么多次之后还剩多少个鸽子）。随后我们还会论证，窄证明根本证明不了${\mathrm{PHP}}_{n^{\prime }}^{n^{\prime }-1}$，产生矛盾，这就说明宽子句有指数个，进而说明$S$是指数级的。

接下来我们会严谨的论述上面的证明过程。

二、宽子句消除

首先我们明确一下我们有$n(n-1)$个变量$P_{ij}(i=1,2,\cdots ,n;j=1,2,\cdots ,n-1)$，表示是否给第$i$个鸽子安排第$j$个巢。

1. 关键赋值（Critical Truth Assignments）、关于关键赋值的等价性和可靠性

一个对 { P i j ∣ i = 1 , 2 , ⋯ , n ; j = 1 , 2 , ⋯ , n − 1 } \{P_{ij}|i=1,2,\cdots,n;j=1,2,\cdots,n-1\} {Pij​∣i=1,2,⋯,n;j=1,2,⋯,n−1}的赋值是关键赋值，就是说它定义了$n-1$只鸽子到$n-1$个巢的一一映射。

如图，这种分配方式就是一个关键赋值，其中变量$P_{12},P_{31},P_{43}$为真，其余变量为假。在一个关键赋值中，如果第$i$只鸽子是无家可归的，我们就称它是一个“落下$i$的赋值”_{（原文是i-critical，不过我这里翻译得更形象了一些）}。

我们接下来的语境都是在关键赋值上说的。我们定义两个子句$c_1,c_2$关于关键赋值等价为：对于任何关键赋值$\alpha$，$c_1$在$\alpha$上的值都等于$c_2$在$\alpha$上的值。两个并不完全等价的子句可能关于关键赋值等价。同样，我们还有推理关于关键赋值可靠的定义：两个子句$c_1,c_2$推出$c_3$的这步推理关于关键赋值可靠，就是说对于每个使$c_1=c_2=1$的关键赋值也使$c_3=1$。

2. 消去否定连接词

接下来我们会利用关于关键赋值等价这个概念。我们知道，${\mathrm{PHP}}_n^{n-1}$里含有很多形如$\neg P_{ik}\vee \neg P_{jk}$的子句，我们想把$\neg$消掉（这一步不是关键步骤，不过会使我们的证明更简洁）。我们接下来证明这样一个事实：

引理1 设$\overline{P_{ik}}=P_{1k}\vee P_{2k}\vee \cdots \vee P_{i-1,k}\vee P_{i+1,k}\vee \cdots \vee P_{nk}$。则$\neg P_{ik}$与$\overline{P_{ik}}$关于关键赋值等价。

证明：核心的东西就是注意到关键赋值是一个一一映射，第$k$个巢一定是住了鸽子的；要么第$i$只鸽子占据该巢，要么其他某个鸽子占据该巢。

• 如果$P_{ik}=1$，即$\neg P_{ik}=0$，则鸽子$i$占据了巢$k$，那么其他鸽子都不能占据巢$k$，即$\neg P_{1k}\wedge \neg P_{2k}\wedge \cdots \wedge \neg P_{i-1,k}\wedge \neg P_{i+1,k}\wedge \cdots \wedge \neg P_{nk}$成立；
• 如果$P_{ik}=0$，即$\neg P_{ik}=1$，则鸽子$i$没有占据巢$k$，那么一定有其他某个鸽子占据了巢$k$，即$P_{1k}\vee P_{2k}\vee \cdots \vee P_{i-1,k}\vee P_{i+1,k}\vee \cdots \vee P_{nk}$成立。∎

所以我们就把每个$\neg P_{ik}$转化为了一个不含$\neg$的子句$\overline{P_{ik}}$。我们不仅要处理掉原${\mathrm{PHP}}_n^{n-1}$公式中的$\neg$，还要处理推理过程中的$\neg$。每一步归结$$a\vee b,\neg a\vee c⟹b\vee c$$现在变成了$$a\vee b,\overline{a}\vee c⟹b\vee c$$这列推理是关于关键赋值可靠的，可以这么理解：在关键赋值下，$a$和$\overline{a}$中有且仅有一个成立；$a\vee b$就是说若$\overline{a}$成立，则$b$成立；$\overline{a}\vee c$就是说如果$a$成立，则$c$成立。因此$b$与$c$必至少有一个成立。

处理完之后，我们证明就不含任何否定连接词了。

3. 宽子句的定义

定义宽子句为含有至少$\frac{n^2}{10}$个文字（即变量）的子句，也就是包含了至少总变量个数的（大约）$\frac{1}{10}$的子句。例如，当$n=5$时，子句$P_{12}\vee P_{13}\vee P_{14}$就是包含了$3>\frac{5^2}{10}$个变量的宽子句。为什么选择分母为$10$呢？我们待会会看到其原因。

4. 消除宽子句

回忆我们在整体框架中提到的，我们采用反证法，先假设证明步数$S<2^{\frac{n}{20}}$，然后推出矛盾。设宽子句的个数为$W$。注意，每个宽子句包含了至少$\frac{n^2}{10}$个变量，而一个子句只包含了一个变量，所以这$W$个宽子句一共有$W\frac{n^2}{10}$个变量。而变量总共只有$n(n-1)$个，所以其中一个变量（设为$P_{ij}$）一定在超过$\frac{W}{10}$个宽子句中出现了（否则，如果所有变量都只在不超过$\frac{W}{10}$个宽子句中出现，则它们的出现次数加起来至多为$\frac{W}{10}n(n-1)<W\frac{n^2}{10}$）。那么，如果在证明的所以步数中令$P_{ij}=1$，就可以消去所有含$P_{ij}$的子句，也就是消除了至少$\frac{W}{10}$个宽子句。换言之，我们让宽子句的数量减少了$\frac{1}{10}$。这一步也相当于是将第$i$只鸽子与第$j$个巢配对了。当然，不要忘记，我们是在关键赋值下讨论问题的，所以我们还要让其他所有的$P_{il}(l\ne j)$、$P_{uj}(u\ne i)$等于$0$，这样才能让鸽子$i$不与另一个巢配对、且其他鸽子也不能与第$j$个巢配对了。至此，变量还剩下$(n-1)(n-2)$个，证明被转化为了“除第$i$只外的其他$n-1$只鸽子不能与除第$j$个以外的其他$n-2$个巢配对”，即我们得到了一个${\mathrm{PHP}}_{n-1}^{n-2}$的证明。

以此类推，如法炮制，每增加一个新的配对就可以让宽子句的个数减少至少$\frac{1}{10}$，最多只需要${\log }_{\frac{10}{9}}W$次宽子句就消完了。

此时，我们得到的是一个对于${\mathrm{PHP}}_{n^{\prime }}^{n^{\prime }-1}$的证明，其中$n-n^{\prime }$就是确定配对的个数，所以$n-n^{\prime }\le {\log }_{\frac{10}{9}}W$，$$n^{\prime }\ge n-{\log }_{\frac{10}{9}}W\ge n-{\log }_{\frac{10}{9}}S>n-{\log }_{\frac{10}{9}}{2}^{\frac{n}{20}}=\left(1-\frac{1}{20}{\log }_{\frac{10}{9}}2\right)n\approx 0.67106n$$也就是说，我们证明了：如果$S<2^{\frac{n}{20}}$，则存在一个对${\mathrm{PHP}}_{n^{\prime }}^{n^{\prime }-1}$的不含宽子句的证明。接下来，我们将证明一个引理与这个结论矛盾。

三、宽度下界

引理2 任何对于${\mathrm{PHP}}_n^{n-1}$的归结证明都存在一个宽度至少为$\frac{2}{9}{n}^2$的子句。

证明：
(1) 子句的复杂性 设$H$是一个子句集，定义$H$对于所有关键赋值蕴含子句$C$为：所有满足$H$中全部子句的关键赋值$\alpha$都能满足$C$。设$C$的复杂度$\mathrm{complexity}(C)$为：在${\mathrm{PHP}}_n^{n-1}$的所有子句中能蕴含$C$的最少子句个数。有些结论是一个子句蕴含不了的，需要多各子句蕴含，比如我们用$a\vee b$和$\neg a\vee c$推出$b\vee c$，$a\vee b$一个子句是蕴含不了$b\vee c$的，需要配合$\neg a\vee c$才能蕴含出来，因此$b\vee c$的复杂性至少是$2$。

对于关键赋值而言，前提中描述两只鸽子不能飞进同一个巢的子句是自动被满足的，所以我们只考虑描述一只鸽子必须至少占一个巢的子句（称为“鸽子有家子句”）。每个“鸽子有家子句”的复杂度为$1$（因为它自己就可以蕴含自己），证明中最后一个子句$0$的复杂度为$n$（前提一个都不能少）。那么归结能干什么呢？设子句$C_1,C_2$被归结成$C_3$，$C_i$是由包含一些“鸽子有家子句”的初始子句集$T(C_i)$蕴含得来的，则$T(C_3)=T(C_1)\cup T(C_2)$，$\mathrm{complexity}(C_3)=|T(C_3)|\le \mathrm{complexity}(C_1)+\mathrm{complexity}(C_2)$。

我们断言：证明过程中一定存在一个“中等”复杂度子句，其复杂度介于$\frac{1}{3}n$和$\frac{2}{3}n$之间。原因在于，我们从复杂度为$n$的$0$子句开始向上回溯，每次选择那个复杂度较大的前提，则我们观察的子句的复杂度在一点一点地减少（可能不变，但因为“鸽子有家子句”的复杂度为$1$所以一定有一些时刻是减少的）。我们要证明其复杂度不可能一下子从$>\frac{2}{3}n$跳到$<\frac{1}{3}n$。因为如果这种情况存在，设复杂度$>\frac{2}{3}n$的子句为$L$，其复杂度较高、较低的前提分别为$J,K$，因为$J$的复杂度$<\frac{1}{3}n$所以$K$的复杂度也$<\frac{1}{3}n$；这与绿色不等式矛盾。这样我们就证明了“中等”复杂度的子句的存在性。

(2) 中等复杂度子句一定含有很多个变量 设$C$是那个中等复杂度子句，$H$是能蕴含$C$的最小的“鸽子有家子句”的集合，$|H|=m$。我们将证明$C$至少有$(n-m)m\ge \frac{2}{9}{n}^2$个变量。这个不等式成立的原因是一个二次函数极值问题，可以用下图简要地理解。

证明一个子句中含有某个变量的方法就是证明该变量的赋值发生改变可以改变该子句的赋值。

注意到不满足子句$Q_i$=“第$i$只鸽子必须飞进某个巢”的关键赋值就是“落下$i$的赋值”。因为$H$是“鸽子有家子句”的集合，所以$H$包含了一些$Q_i$。任选一个$i$使得$Q_i\in H$。我们断言：存在一个“落下$i$的赋值”$\beta$不仅不满足$Q_i$，还不满足$C$。这是因为如果所有“落下$i$的赋值”都满足$C$，那么$Q_i$就可以从$H$中移除了，这与$H$的最小性矛盾。你问我为什么$Q_i$可以从$H$中移除？设 H ∖ { Q i } H\setminus\{Q_i\} H∖{Qi​}的合取为$R$，我们有$R\wedge Q_i\to C$，即$\forall$关键赋值$\alpha$，若$\alpha$同时满足$R$和$Q_i$则$\alpha$满足$C$。现在又有：$\forall$关键赋值$\alpha$，若$\alpha$不满足$Q_i$则$\alpha$满足$C$，这也意味着满足$R$且不满足$Q_i$的$\alpha$都满足$C$。结合起来就得到$\alpha$只要满足$R$就可以满足$C$，即$R\to C$。因为$\beta$是关键赋值，所以$\beta$一定给除了$i$以外的每只鸽子$j$都单独安排了住处。现在任取鸽子$j$使得$j\notin H$，把$\beta$给$j$的住处分配给$i$，我们就得到了一个与$\beta$只有一些细微差别的“落下$j$的赋值”${\beta }^{\prime }$。${\beta }^{\prime }$满足所有$H$中的子句，因为这些子句描述的鸽子都有住处，没住处的鸽子对应的“鸽子有家子句”在$H$外面。设$\beta$给鸽子$j$分配的巢是$l$，则$\beta$与${\beta }^{\prime }$的差别在于两个地方：$\beta$给$P_{jl}$分配$1$而${\beta }^{\prime }$分配$0$；$\beta$给$P_{il}$分配$0$而${\beta }^{\prime }$分配$1$。由于$C$是一个不含否定连接词的子句，如果$C$不含$P_{il}$，$P_{jl}$从$1$变$0$不可能让$C$从$0$变$1$；因此$C$一定含$P_{il}$。让$i$取遍$H$中“鸽子有家子句”描述的鸽子，让$j$取遍所有与$H$无关的鸽子并让$l$去$\beta$为$j$分配的住处，则这样的$P_{il}$共有$m(n-m)$个，即$C$的宽度至少为$m(n-m)\ge \frac{2}{9}{n}^2$。∎

回顾第二节结束时我们提到的：如果$S<2^{\frac{n}{20}}$，则存在一个对${\mathrm{PHP}}_{n^{\prime }}^{n^{\prime }-1}$的不含宽子句的证明，其中$n^{\prime }\ge 0.67106n$。而引理$2$意味着对${\mathrm{PHP}}_{n^{\prime }}^{n^{\prime }-1}$的任何一个归结证明都包含了一个宽度至少为$\frac{2}{9}{n}^{\prime 2}=0.10007n>\frac{1}{10}{n}^2$的子句，与证明不含宽子句矛盾，因此$S\ge 2^{\frac{n}{20}}$。证毕。

四、总结

最后，我们就证明了：

定理 对于充分大的$n$，任何对${\mathrm{PHP}}_n^{n-1}$的归结证明的大小都至少为$2^{\frac{n}{20}}$。

这里我还想提一句：为什么把宽子句定义为包含了至少$\frac{n^2}{10}$个变量？为什么分母是$10$而不是$9$、$11$？以及$2^{\frac{n}{20}}$是最好上界吗？首先我们需要知道：引理2的$\frac{2}{9}{n}^2$已经是最优的结果了，根据二次函数的性质，$\frac{m}{n}$的上界是下界的两倍时只有它们关于$\frac{1}{2}$对称才能让$\min (n-m)m$最大；此时上下界分别为$\frac{1}{3}$和$\frac{2}{3}$，$\min (n-m)m=\frac{2}{9}{n}^2$。我们再设我们能得到的最好上界为$2^{xn}$，宽子句的定义是含有至少$\mu n^2$个变量的子句，那么$n^{\prime }$的计算公式为$$n^{\prime }\ge (1-x{\log }_{\frac{1}{1-\mu }}2)n$$而引理2意味着对${\mathrm{PHP}}_{n^{\prime }}^{n^{\prime }-1}$的任何一个归结证明都包含了一个宽度至少为$\frac{2}{9}{n}^{\prime 2}$的子句，我们要控制$\frac{2}{9}{n}^{\prime 2}\ge \mu n^2$，同时使$x$最大。即$$\max x,\text{ s.t. }\exists \mu ,\frac{2}{9}(1-x{\log }_{\frac{1}{1-\mu }}2{)}^2\ge \mu$$这个问题非常奇怪，我算出来$x$可以高达$0.278$左右，不过$\frac{1}{20}$的确是一个解，有兴趣的童鞋们可以自己算一下~

五、可以不消去否定连接词吗？

可以，方法详见Eli Ben-Sasson和Avi Wigderson与1999年发表的论文Short Proofs Are Narrow - Resolution Made Simple的第$5$节与第$6.2$节。

六、关于深度受限弗雷格系统的指数级下界

证明深度不超过$d$的弗雷格系统下界的方法大概是：假设证明的步数不超过一个预定值$S$，对整个弗雷格证明施加随即约束，证明有很大的概率深度会减少$1$，但问题的复杂度并没有太大的变化。施加$d-2$次后，证明的深度变为$2$（也就是变成了一个带弱化规则的归结证明），其步数并没有发生显著变化，也就意味着用$S$步归结就可以证明一个$n$相当大的$\mathrm{PHP}$，然后再用这篇文章的内容反驳这一点即可。