计算机科学家试图驳斥科拉茨猜想

在过去的几年里，Marijn Heule使用了一种名为SAT Solution(SAT代表“可满足性”)的计算机化证明技术，攻克了一系列令人印象深刻的数学问题：2016年的毕达哥拉斯三重问题，2017年的舒尔5号问题，现在是凯勒在第七维的猜想--广达在我们最近的文章“计算机搜索解决了90岁的数学问题”(Computer Search Setting 90-Year-Old Math Problem)中谈到了这个结果。

但是，卡内基梅隆大学(Carnegie Mellon University)的计算机科学家希勒(Heule)将目光投向了一个更雄心勃勃的目标：科拉茨猜想，许多人认为这是数学中最臭名昭著的公开问题(如果也是最容易陈述的问题之一)。当我向其他数学家提到Heule正在尝试这样做时，他们的第一反应是怀疑。

匹兹堡大学的托马斯·黑尔斯(Thomas Hales)是计算机打样领域的领先者，他说：“我看不出你怎么能用SAT解题来完全解决这个问题。”这项技术通过将问题转化为离散的、有限的问题，有效地帮助数学家解决问题-其中一些问题具有无限的可能性。

然而，黑尔斯和其他人一样，对低估海勒持谨慎态度。“他非常善于找到将问题编码为SAT问题的聪明方法。他只是在这方面做得很出色。“。

德克萨斯大学奥斯汀分校的Scott Aaronson正在与Heule合作研究Collatz的工作，他补充道：“Marijn是一个拥有锤子的人，这是SAT的解题，他现在可能是世界上最伟大的锤子使用者。他几乎什么都试过。“。时间会证明他是否能把科拉茨变成钉子。

SAT解决包括将问题转化为计算机友好的使用命题逻辑的陈述，并使用计算机来确定是否有方法使这些陈述成为现实。这里有一个简单的例子。

假设你是一位家长，正在努力安排照看孩子。除周二和周四外，一名保姆可以工作一周。另一个可以工作一周，除了星期二和星期五。第三个可以工作一周，除了星期四和星期五。你需要覆盖周二、周四和周五。你能够办得到吗？

找出答案的一种方法是将保姆约束转换为一个公式，然后将该公式输入到SAT解算器中。这个程序会找出是否有办法给保姆分配天数，使公式成为现实，或者说是“可满足的”，意思是你可以得到你想要的三天。在这种情况下，你很幸运--确实有。

不幸的是，数学中许多最重要的问题并不直接类似于SAT问题。但有时，它们可以以令人惊讶的方式重新表述为可满足性问题。

Aaronson说：“很难预测一个问题何时会简化为一个巨大但有限的计算。”

科拉茨猜想是那些数学问题中的一个，乍一看，它与照看孩子的问题一点也不像。它说选择一个数字，任何你想要的数字(只要它是一个非零整数)。如果是奇数，乘以3再加1；如果是偶数，除以2。现在你得到一个新的数字。应用相同的规则，获得一个新的号码，然后继续前进。这个猜想预测，无论你从哪个数字开始，最终你都会以1结束，在这一点上你会陷入一个小循环：1，4，2，1。

尽管经过近一个世纪的努力，数学家们还没有接近证明这一点。

但这并没有阻止Heule的尝试。2018年，他和Aaronson-当时在奥斯汀的同事-获得了国家科学基金会(National Science Foundation)的资金，将SAT求解应用于Collatz猜想。

作为第一步，计算机科学家Aaronson想出了Collatz猜想的另一个公式，称为重写系统，这对计算机来说更自然。

在重写系统中，您有一组符号，如字母A、B和C。您可以使用它们组成序列：ACACBACB。您也有转换这些序列的规则。有一条规则可能会说，只要你看到“AC”，就用“BC”代替。另一种可能是用“aaa”代替“bc”。您可以有任意数量的规则来指定您想要的任何类型的转换。

计算机科学家通常感兴趣的是知道给定的重写系统是否总是终止。也就是说，无论您从哪个字符串开始，也不管您应用规则的顺序如何，字符串最终是否会转换为您不能再对其应用规则的状态？

Aaronson提出了一个重写系统，有7个符号和11条规则，类似于Collatz程序。如果他和赫勒能证明这个重写系统总是终止的，他们就会证明这个猜想是真的。

为了把Collatz变成SAT问题，Aaronson和Heule不得不再走一步。它涉及矩阵，它是由数字组成的数组。他们需要为重写系统中的每个符号分配一个唯一的矩阵。这种方法-一种试图证明重写系统终止的常用方法-将允许他们将符号的转换视为矩阵乘法。代表重写系统中七个符号的七个矩阵需要满足若干约束，反映了11个规则需要彼此一致的方式。

卡内基梅隆大学(Carnegie Mellon)的研究生埃姆雷·约尔库(Emre Yolcu)正与海勒一起研究这个问题，他说：“你试图找到满足这些限制的矩阵。”“如果你能找到他们，你就证明了[他们]正在终止，”言下之意是，你证明了科拉茨。

问题是“是否存在满足这些约束的矩阵？”是一个SAT解算器类型的问题。Aaronson和Heule在2乘2的小矩阵上启动了SAT解算器。它没有找到任何有效的方法。接下来，他们尝试了3乘3矩阵。再说一次，没有运气。Heule和Aaronson不断增加矩阵的大小，希望他们能找到合适的矩阵。

然而，这种方法只能走到这一步，因为随着矩阵变大，搜索正确矩阵的复杂度呈指数级增长。Heule估计，任何大于12乘12的矩阵都会压倒当今的计算能力。

“一旦矩阵变得太复杂，你就无法解决问题，”他说。

Heule仍在努力优化搜索，试图使其更有效率，以便SAT解算器可以检查越来越大的矩阵。他和他的合作者正在撰写一篇论文，总结他们到目前为止的发现，但他们几乎没有想法，很可能很快就会放弃Collatz-至少目前是这样。

毕竟，SAT解决方案的诱人吸引力在于，如果你能想出如何再检查一个病例，再给一个保姆打电话，把搜索延长一点，你可能会找到你正在寻找的东西。在这方面，Heule最大的资产可能不是他使用SAT解算器的技能。可能是他对追逐的热爱。

“我只是个乐观的人，”他说。“我经常觉得自己很幸运，所以我就试一试，看看我能走多远。”