机械证明可不仅仅是枚举——最近Erdos某猜想特殊情况的证明

前段时间有这么一个新闻,说是有人用计算机证明了Erdos的一个猜想的特殊情况。因为忙,最近才看了这个论文,想给大家说说是怎么搞的。

首先,我们来说说这个问题到底是啥。

我认为这个问题可以归到拉姆赛类型的问题中,粗略来说,这类问题说的是即使在非常无序的结构中,当结构的大小达到一定程度时,必然会有高度有序的子结构出现。比如拉姆赛定理,说的就是对于任意给定的整数k和l,将完全图任意染红蓝两色,当完全图本身足够大时,最后要么出现红色的k阶完全子图,要么出现蓝色的l阶完全子图。也就是说,完全的无序是不可能的。

Erdos的这个问题,叫Erdos差异问题,也是同样的类型。我们取一个由+1与-1组成的数列,然后考虑它的一些子数列。如果是完全随机的话,这些子数列的和应该很接近0。但Erdos认为,只要数列足够长,长到无限长,对于任何的常数C,应该可以找到这样的子数列,它们的和的绝对值超过C。

具体的数学定义如下:对于任意由+1和-1组成的数列(a_n)_{n \in \mathbb{N}},考虑它的前N项。其中对于所有d \leq N,考虑子数列a_d, a_{2d}, \ldots, a_{\lfloor N/d \rfloor d}的和的绝对值S((a_n)_{n \in \mathbb{N}}, N, d) = \left| \sum_{k=1}^{\lfloor N/d \rfloor} a_{kd} \right|,然后取所有d中这个绝对值最大的d,将这个最大的绝对值记作MaxS((a_n)_{n \in \mathbb{N}}, N)。Erdos的问题就是,是否对于任意一个常数C与任意一个数列(a_n)_{n \in \mathbb{N}},当N足够大的时候,MaxS((a_n)_{n \in \mathbb{N}}, N)必定会超过C?也就是说,当数列无穷时,是否必定存在一个上述形式的有限子数列,它的和的绝对值超过C?

这样的子数列在某种意义上也可以看成一种需要每个分项配合的“秩序”,虽然可能比较弱,因为随机游走的结果也可以做到这一点。在这种情况下,我们可以认为这个问题的本质差不多也是“不存在完全的无序”。

当然了,这不是唯一的看法。另一种看法是这个问题实际上说明了,不存在某种可以避开所有子数列的结构,不过我觉得这也跟拉姆赛问题有些擦边。

然后之前一段时间有数学家把C=2的情况做掉了,具体论文在这里:http://arxiv.org/abs/1402.2184。也就是说,必定找到想要的子数列,使得和的绝对值大于2。

他们是怎么做的呢?其实很简单,他们用计算机证明了,只要数列长度超过1161,那么就必定能找到和的绝对值大于2的给定形式的子数列。显然这么长的数列,要人工分析是不太可能的,必须扔给电脑,但是怎么扔呢?

在自动推理的学界,有一样神器,叫SAT Solver。

如果你是计算机系的学生,那么你一定听说过SAT,也就是可满足性问题:给定一个由与、或、非连接布尔变量组成的命题,是否存在一个变量的赋值满足这个命题,也就是说使得这个命题为真?这个问题著名,主要是因为它是第一个NP-完全的问题,很多问题都是通过规约到SAT来证明是NP-完全的。也正因如此,很多工业和数学上遇到的问题,都可以规约为SAT问题。在这里,规约的意思是将问题表达为布尔变量组成的命题,其中命题的解与原问题的解相互对应。所以,如果命题可满足,那么原来问题必定有解;如果命题不可满足,原来的问题就没有解。只要解决了对应命题的SAT问题,那么就解决了原来的问题。

正因为很多问题都可以规约为SAT问题,所以与其对每个特定的问题开发解法,可能直接开发一个SAT问题的通用算法更方便。这就是SAT Solver,专门解SAT问题的程序。你只要给它一个公式,它吭哧吭哧一段时间就可能给你一个答案(对于所谓Complete Solver而言),虽然要多少时间是完全不知道的,取决于问题的难度。

SAT Solver的研究其实还算相当热门,几乎每年都会有一项SAT Solver的竞赛,由SAT Competition与SAT Race轮流,前者比较偏学术,后者比较偏应用,不过形式是类似的,就是选择一大堆问题,然后让很多SAT Solver去解,谁用的时间少谁赢。

SAT Solver一般分两大类,一类是基于推理,另一类基于撞大运……后者就是先随便找一个赋值,然后尝试改进这个赋值,使得满足命题的程度越来越大,最后如果运气好,就能撞上一个能满足命题的赋值。问题是,如果命题本身就是不可满足的,那么就永远不可能出解……

基于推理的SAT Solver则更加有趣。它们基本上就是一个叫DPLL的算法的变种,这个算法会把命题分成很多子句,要每个子句都为真,命题才为真,然后用逻辑与组合这些子句然后根据逻辑规则简化这些组合,不断重复,如果在某一步得到“False”,那么这个命题就是不可满足的,因为从应该为真的子句导出了矛盾。有时候这样的重复不足以揭示问题,所以也会给某些变量赋值,如果得到“False”,证明变量不可能取这个值,比如取另一个值。这样重复下去,直到找到一个满足的赋值,或者证明所有的赋值都是矛盾的所以命题不可满足。对于不可满足的命题,有些Solver会给出一个证书,通过某些证书(比如Backbone variable)可以在不重复相同计算的情况下验证这个命题不可满足。

说了这么多,这个与自动推理又有什么关系呢?

这些子句,在DPLL Solver的术语中也叫引理。组合子句,其实就是通过组合引理导出新的引理,而如果得到了“FALSE”的引理,也就意味着原来引理的组合可以推出“FALSE”,也就是说,原来的命题本身就有矛盾。

这实际上就是自动推理的一种。

当然,这个算法是50年前的了,现在的SAT Solver要更加先进得多。首先,它们有很多不同的优化,可以加速算法本身的运行。而更重要的是,它们有非常精巧的推理方法。要知道,推理方法,也就是在每一步选择哪些引理进行组合,得到新的引理,这一点对于效率非常关键。SAT Solver近几年的常青树之一,glucose,核心就是一种叫glue clause的引理选择。另外,引理的组合是无穷的,但内存是有限的,如何判断哪些引理重要,哪些引理可以舍弃,这本身就不容易。如果舍弃了重要的引理,可能就要兜一个大弯才能解决问题。但有些推理方法,对一类问题很有效,对另一类问题可能就要花比较长的时间,这时候就要进行取舍。这里边的学问非常深,而且与实际操作关系很大,因为SAT Solver设计出来就是要解决现实中的问题的。现在,最好的SAT Solver可以解开需要几百MB的数据才能表达的问题,也能解出一些非常难的问题。这对于工业来说很重要,比如说一些电路设计的线路排布,就需要用到SAT Solver。SAT Solver不仅是研究,而且对生产也是大大的有好处,绝对是非常有用。

好了,兜了这么一个大弯,回到Erdos的问题上。那些数学家是怎么证明C=2的情况呢?很简单:他们把长度为1161的数列用布尔变量编码,然后将对应的问题规约到SAT,也就是说翻译成命题,然后喂给SAT Solver,他们用的是Lingeling和glucose。这两个Solver哼哧哼哧了一段时间,不断把引理倒来倒去,最后报告了这个命题是不可满足的。glucose还顺便给出了一个证书,这个证书很大,大概是13GB。然后这个问题就被证明了。

有人可能觉得方法很暴力,但是从我的经验看来,其实这里边技术含量很高。先不说暗藏在SAT Solver里的技术含量,就算是将问题规约到SAT,也不是件容易的事。同一个问题可以有非常多的规约方式,但不是每种规约方式求解需要的时间都是一样的。我曾经尝试解某个问题,用一种方式死活解不开,另一种更精细的方法Solver就秒解了……有很多组合问题,其实即使用SAT Solver解,不找准问题的结构所在,盲目去规约的话,基本上做不出来。说到底,Solver是一个自动推理程序,如果一开始给的路就不对的话,那当然需要时间;如果一开始就根据问题结构把引理切好,那显然解起来容易得多。所以,这些数学家把问题做出来了,本身就说明他们很好地理解了这个问题。

可以预见,未来用SAT Solver解的离散数学问题会越来越多。但要记住,这其实并不是暴力枚举,而是巧妙的自动推理,其中的智慧,只有一群人经过漫长的积累才能做到。

起码在目前来说,计算机的智慧,其实是人的智慧的延伸。

Advertisements

发表评论

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / 更改 )

Twitter picture

You are commenting using your Twitter account. Log Out / 更改 )

Facebook photo

You are commenting using your Facebook account. Log Out / 更改 )

Google+ photo

You are commenting using your Google+ account. Log Out / 更改 )

Connecting to %s