卡内基梅隆大学的计算机科学家和数学家解决了凯勒猜想的最后一个顽固的部分，这是科学家们困扰了90多年的几何问题。通过将这个难题解释为计算机科学家所说的可满足性问题，研究人员将这个问题搁置了四个月的疯狂计算机编程中，而使用一簇计算机仅需30分钟即可完成计算。

“我们真的很高兴能解决问题，但后来我为这个问题消失感到难过，”计算机科学系(CSD)和数学科学系的教学教授约翰·麦基(John Mackey)说，他从那时起一直从事凯勒猜想的研究。他30年前是一名研究生。“但是后来我又感到高兴。只有这种满足感。”

该解决方案是由计算机科学副教授Marijn Heule率先提出的方法的又一次成功，该方法于去年8月加入CSD。Heule使用了SAT解算器(一种使用命题逻辑来解决可满足性(SAT)问题的计算机程序)来解决一些数学上的难题，包括勾股三重问题和Schur数5。

休勒谈到凯勒的猜想时说：“这个问题已经困扰了很多人数十年，差不多一个世纪。” “这确实是一个展示过去可以做的事情的展示。”

由德国数学家爱德华·奥特·海因里希·凯勒(Eduard Ott-Heinrich Keller)提出的猜想与平铺有关—特别是如何用等大小的瓷砖覆盖区域而没有任何间隙或重叠。推测是至少有两个图块必须共享一条边，并且对于每个维度的空间都是如此。

很容易证明二维瓷砖和三维立方体是正确的。截至1940年，该猜想已被证明适用于所有六个维度。然而，在1990年，数学家证明它在10维或更高维度上不起作用。

那时，凯勒的猜想吸引了当时是夏威夷大学学生的麦基的想象。在大学计算机集群旁边的办公室里，他很感兴趣，因为可以使用离散图论将问题转换为计算机可以探索的形式。以这种形式称为凯勒图(Keller graph)，研究人员可以搜索“ cliques”，即不共享面孔而连接的元素子集，从而反驳了这一猜想。

2002年，Mackey做到了这一点，发现了第八维集团。通过这样做，他证明了猜想在那个维度上失败了，并因此在第九维度上失败了。

这就使第七维的猜想无法解决。

当Heule去年从德克萨斯大学到达CMU时，他已经因使用SAT解算器解决长期存在的开放式数学问题而享有盛誉。

“我心想，也许我们可以运用他的技术，”麦克基回忆道。不久之后，他开始与Heule和Joshua Brakensiek讨论如何在Keller猜想中使用SAT解算器，Joshua Brakensiek是数学科学和计算机科学的双主修，目前正在攻读博士学位。斯坦福大学计算机科学专业。

SAT求解器要求使用命题公式(A或非B和B或C)等来构造问题，以便求解器可以检查所有可能的变量，以获得满足所有条件的组合。

Heule说：“进行这些翻译的方法有很多，而翻译的质量通常会影响您解决问题的能力，或破坏您解决问题的能力。”

拥有15年的经验，Heule擅长于进行这些翻译。他的研究目标之一是开发自动化推理，以便可以自动完成此翻译，从而使更多的人可以使用这些工具解决问题。

即使是高质量的翻译，在第7维上要检查的组合的数量也令人难以置信-一个324位数字-即使超级计算机也找不到解决方案。但是Heule和其他人运用了许多技巧来减小问题的严重性。例如，如果一个数据配置被证明是行不通的，他们可以自动拒绝依赖它的其他组合。而且由于许多数据是对称的，因此如果该程序以一种排列方式达到死胡同，则该程序可以排除该配置的镜像。

使用这些技术，他们将搜索减少到大约十亿个配置。博士David Narvaez参与了这项工作。罗彻斯特理工学院的学生，他于2019年秋季担任访问研究员。

一旦他们在40台计算机的群集上运行代码，他们终于有了答案：这个猜想在第7维上是正确的。

Heule说：“我们成功的原因是John在这个问题上拥有数十年的经验和洞察力，我们能够将其转换为计算机生成的搜索。”

Heule说，与许多出版物结合了计算机检查过的证明部分与其他部分的手工记录相比，结果证明完全由计算机计算得出。他指出，这使读者难以理解。Heule强调说，Keller解决方案的计算机证明包括解决方案的所有方面，包括Narvaez贡献的对称性破缺部分，因此，证明的任何方面都无需依靠人工。

他说：“我们对这一结果的正确性有真正的信心。” 一篇描述Heule，Mackey，Brakensiek和Narvaez的解决方案的论文在6月的国际自动推理联合会议上获得了最佳论文奖。

麦克基说，解决凯勒的猜想有实际应用。科学家寻求反驳这些猜想的那些集团对于生成可以使数据传输更快的非线性代码很有用。因此，SAT求解器可用于查找比以前可能的维数更高的非线性代码。

Heule最近提议使用SAT解算器来解决一个更著名的数学问题：Collat​​z猜想。在此问题中，其想法是选择任何正整数，如果它是偶数则除以2;如果是奇数，则乘以3，然后加1。然后将相同的规则应用于结果数和每个后续结果。该猜想的是，最终的结果将始终为1。

Heule承认，使用SAT求解器解决Collat​​z的工作是“漫长的尝试”。他补充说，但这是一个雄心勃勃的目标，他解释说，即使Collat​​z证明无法达到，SAT求解器也可能用于解决一些不太令人恐惧的数学问题。