ACM通信
研究突出了
技术视角:图同构问题的一个逻辑步骤
图同构问题一直是理论计算机科学中令外行人和专家着迷的谜题之一。1979年，加里和约翰逊在他们著名的关于计算机和难处理性的书中提到了这个问题，但事实上，这个问题可以追溯到更早的时候，并且已经解决了半个多世纪。2015年，一项重大进展轰动了媒体:巴巴的准多项式算法。这是30多年来对普遍问题的第一次改进。然而，这仍然是一个悬而未决的问题。该问题的核心是利用算法检测组合对象的对称性。
也许令人惊讶的是，这个问题在许多不同的、截然不同的领域都有应用。我们可以在逻辑上下文中找到这样一个应用程序域。事实上，同构问题似乎与逻辑学家所称的寻找捕获PTIME的逻辑密切相关，这是有限模型理论中的一个主要开放问题。简而言之，我们想要一个足够强大的逻辑，它能够精确地允许所有可有效求解的问题都被捕捉到公式中，但不能比这更强大。就数据库而言，我们想要一种查询语言，它的表达能力足以让所有的查询都能得到有效的回答，但不能超过这个限度。
对于一个正在探索的逻辑学家来说，为某些类型的结构设计一个有效的同构算法并不是特别有帮助。所需要的是能够在逻辑中“解决”问题。事实上，虽然这是必要的一步，但这可能还不够。但是，能够在逻辑中“解决”类的封圣问题就足够了。直观地说，规范化问题需要一种有效的标准形式，一种明确地(也就是规范化地)表示给定输入的方式。封圣问题与同构问题密切相关，考虑到同构的实际应用，事实证明封圣问题的解决方案是用户通常实际想要和需要的。
在接下来的论文中，Grohe和Neuen考虑了有界秩宽度图的一类。这个类等价于有界团宽度的图，这个术语有时对不关注算法方面的图理论家更熟悉。这个类不容易定义，但它在图结构理论中起着核心作用。本质上，该类中的图可以递归分解为小的部分，以便不同部分之间的相互作用不会太复杂。几年前，这类图基本上是我们没有有效同构检验的唯一一类自然可分解图。
2015年，高仪和施韦策找到了一种有效的测试方法，但对这位求索的逻辑学家来说，答案并不令人满意。该算法涉及大量计算群论技术，使得解决方案不仅复杂，而且不能提供逻辑可定义性和规范化的充分答案。在他们的新论文中，Grohe和Neuen使用了一种纯粹的组合方法:weisfeler - leman算法。这种算法起源于代数图论，它被用在了Babai的算法中，最近它以图核的形式在机器学习中得到了应用。
作者现在表明，值得注意的是，完善的weisfeiller - leman算法在其普通形式中解决了有界秩宽度图的同构问题。事实上，本文甚至更进一步表明，在与算法相对应的逻辑(带计数的定点逻辑)中可以解决封圣问题。总的来说，他们获得了一种逻辑，可以在有界秩宽度的图上捕获PTIME。这意味着，从本质上说，所有可以在这些图上用算法高效求解的东西都可以用一个相当简单的逻辑公式来表示。
高仪和诺恩使用了一种纯粹的组合方法:韦斯菲勒-勒曼算法。
高仪此前已经证明，这种方法可以非常富有成效。事实上，他在2017年出版的关于这个问题的书，篇幅超过500页，对因选修未成年人而关闭的图形课采用了这种方法。然而，秩宽度有界的图类是该方法成功应用的最普遍的一类图。
总的来说，与之前的最佳结果相比，本文基于更简单的算法提供了更强的结果。最重要的是，整体的证明——至少从我的角度来看——更简单，对很多人来说，更容易理解。最后，算法运行时间中的常数，在逻辑上转化为所需变量的数量，是很小的(具体地说，在秩宽度上是线性的)，在某种意义上是尽可能小的。分析的中心是引入了分裂对和翻转函数的新概念，这明显地促进了许多论点。我们经常会发现，当涉及到理论问题时，正确的方法、谨慎的定义选择和预感可以使一切不同。总的来说，Grohe和Neuen找到了一种干净利落的方法来完成逻辑学家对有界秩宽图的探索。
数字图书馆是由计算机协会出版的。版权所有©2021 ACM, Inc.
没有找到条目