静园5号院科研讲座 | 陈翌佳谈逻辑语言与算法
关键词：逻辑 算法
编者按
2019年6月25日，复旦大学陈翌佳教授受邀访问北京大学前沿计算研究中心，并在静园五院做了题为“Algorithmic Meta-Theorems – Where Logic meets Algorithms”的主题报告，介绍了如何用逻辑语言刻画一些图上的算法问题，并用逻辑领域的工具给出这些算法问题的解决方案。报告由中心讲席教授邓小铁主持，听众包括来自北京大学信息学院、元培学院等院系的师生。
陈翌佳教授报告现场
陈翌佳教授首先简单讲述了理论计算机的发展历史：早期的理论计算机很多时候就是用逻辑去刻画的，而随着P versus NP概念的引入，北美主流的理论计算机就沿着算法和复杂性的思路发展，结论和工具以及方法论都源自代数、组合、图论等。此时候的逻辑用一些不一样的方式存在于理论计算机领域，比如：通过逻辑理解复杂性——有限模型论、用逻辑的方法去设计算法——算法元定理、用逻辑证明复杂性——证明复杂性。
接下来，陈老师从算法元定理的角度，给我们展示了逻辑工具是如何解决算法问题的。一个符合算法元定理风格的结论的一般描述如下：
对于可以用某类逻辑描述的计算问题，对一类满足结构性质的图，存在一个高效算法。
陈老师说到，很多NP-难的问题在树结构上都有多项式时间算法，如独立集问题、3染色问题、支配集问题等。这些结论可以用Büchi定理描述：对每个单元二阶逻辑公式（Monadic Second-order Logic，简称MSO），存在一个线性时间算法判断树结构问题满足这一逻辑公式。但树结构的局限性太大了，于是Robertson和Seymour引入了树宽度（tree-width）的概念，用来描述一个给定的图和树有多接近。这一概念的数学描述较为复杂，于是陈老师通过一些例子，让大家对树宽度的概念有一些感觉，并介绍了Courcelle定理，即树宽度版本的Büchi定理。而Courcelle定理对于MSO近乎最优，这是基于Kreutzer和Tazari在2010年的结论，即在一些合理假设下，对无限树宽度的图，验证MSO性质在多项式时间内无法完成。
对于用一阶逻辑刻画的问题，陈老师也介绍了相关结论，这些结论中最强的结论证明了，在处处不稠密（nowhere dense）性质的图上，验证一阶逻辑公式可以在近乎线性时间（almost linear time）完成，在一些合理假设下，这一结论是最优的。陈老师总结了一下这一研究主线，提到大家对这一系列结果的批评：逻辑太抽象，而算法元定理过于一般性；算法元定理中的常数都非常大；算法学家都不喜欢逻辑。但陈老师也提到，算法元定理用一种统一的方式给出了一大类算法问题的做法，而且这些结论用一种简单的方式给出了一些问题在某类图甚至是所有图上解决的可能性，此外有一些问题现有的最好的算法就是用逻辑做的。
之后，陈老师介绍了自己在这一领域的一些工作，这些工作的计算模型是AC0电路，这一电路和并行计算有着一定关联。一个众所周知的结论是，在一些自然一致性（uniformity）条件下，AC0电路可以在关系数据库中计算SQL查询。陈老师和Flum在AC0电路下证明了一系列的算法元定理类型的结论，包括：1) 在树深度（tree-depth）不超过d的图中验证MSO性质，可以用一个深度为O(d)，大小为nO(d)的AC0电路解决；2) 对任何常数d，存在整数h使得在灌木深度（shrub-depth）不超过d的图上验证FO性质，可以用一个深度为O(h)，大小为nO(d)的AC0电路解决。陈老师说，这里用到的树深度的概念，直观上描述了一个图和星形图有多接近，而灌木深度的定义是树深度在稠密图上的一种推广，并从树模型给出了灌木深度的定义。陈老师也提到，即使对于一些简单情况，这一电路的实际大小非常大，即使是一个常数。最后陈老师提到和Flum，Huang的一个结果：对k-vertex cover问题，可以用深度为34的AC0电路解决。
最后陈老师总结到，算法元定理从逻辑角度给出了算法设计方案，证明的工具包括结构图论和模型论，以及这一领域还有许多公开待解的问题。报告引起了大家的热烈讨论，陈老师一一解答了大家的疑惑。
陈翌佳教授报告中
文字 | 肖涛
EconCS@PKU
往 期 报 告
— 版权声明 —
本微信公众号所有内容，由北京大学前沿计算研究中心微信自身创作、收集的文字、图片和音视频资料，版权属北京大学前沿计算研究中心微信所有；从公开渠道收集、整理及授权转载的文字、图片和音视频资料，版权属原作者。本公众号内容原作者如不愿意在本号刊登内容，请及时通知本号，予以删除。
点“阅读原文”看报告概要等信息