计算机科学家想改变Collat​​z的假设

强大的SAT求解器技术可以处理臭名昭著的Collat​​z假设。但是，这样做的机会不是很高。

在过去几年中，Marin Hijul使用了一种称为SAT解算器（SAT可满足性）的计算机证明查找技术，以征服了一系列令人印象深刻的数学问题。2016年的毕达哥拉斯三胞胎，舒尔（Schur）在2017年排名第五，以及凯勒（Keller）在第七维度的假说，我们不久前在文章“计算机搜索帮助处理了一个已有90年历史的数学问题”中写道。



然而，现在，卡内基梅隆大学的计算机科学家Hijul将目光投向了一个更加雄心勃勃的目标：Collat​​z猜想被许多人认为是数学中最困难的开放问题（并且可以说是最简单的公式化问题）。其他数学家从我那里得知Khiyul进行了这种尝试，对此表示怀疑。



匹兹堡大学计算机证据研究专家托马斯·海尔斯（Thomas Hales） 说：“我不知道如何用SAT解算器完全解决这个问题。”这项技术从本质上帮助数学家将问题转化为离散的有限问题，从而解决了其中一些问题的无限选择。



但是，海尔斯和其他人一样，对低估Khiyul持谨慎态度。 “他非常擅长寻找巧妙的方法来表达SAT语言中的问题。他非常擅长。”



斯科特·亚伦森来自德克萨斯大学奥斯汀分校的人与Hiyul合作研究了Collat​​z猜想。他试图将其应用于几乎所有事物。”但是只有时间才能证明他是否可以将Collat​​z的假设变成钉子。



SAT解决方案要求使用命题逻辑以计算机可理解的语言重新构造问题，然后连接计算机以确定是否存在使这些陈述正确的方法。这是一个简单的例子。



假设您是一位试图安排托儿服务的父母。除周二和周四外，您的保姆之一可能整周都在工作。另一个是星期二和星期五。第三个-除了星期四和星期五。您需要在星期二，星期四和星期五与孩子一起坐。能做到吗？



一种测试方法是将保姆约束转化为公式并将其提供给SAT解算器。该程序将寻找一种在保姆之间分配天数的方法，以使公式变为真实的或“满意的”-也就是说，您可以获得所需的三天时间。如果成功，则将存在这种方法。



不幸的是，目前尚不清楚如何将许多最重要的数学问题重新表达为SAT语言。但是有时它们可​​以以意想不到的方式改写为满意度问题。



“很难预测何时将任务简化为庞大而有限的计算，” Aaronson说。



Collat​​z猜想是那些数学问题，这些问题一开始似乎根本不是一个保姆问题。她建议以下内容：取任意数字（整数，非零）。如果是奇数，则将其乘以3并加1。如果是奇数，则将其除以2。结果，您得到一个新数字。对它应用相同的规则，然后继续。该假设预测，不管起始数字是多少，您最终都会得到1，然后陷入循环：1、4、2、1。



而且，尽管这一假设已经使用了将近100年，但数学家并没有接近证明这一假设。



但这并没有阻止Khiyul。在2018年，她和阿伦森（当时是大学同事）获得了美国国家科学基金会的资助，将SAT求解器应用于Collat​​z猜想。





取任何数字。如果是奇数，则将其乘以3并加1。如果是奇数，则将其除以2。结果，您得到一个新数字。对它应用相同的规则，然后继续。您能找到不以1结尾的数字吗？您可以自己尝试。



首先，计算机科学家Aaronson提出了Collat​​z假设的另一种表述，即所谓的。一种“替代规则系统”，使计算机更易于使用。



在替换规则系统中，使用一组字符，例如字母A，B和C。使用它们来形成序列：ACACBACB。您还具有转换这些序列的规则。一个规则可能会说，遇到AC后，您将其替换为BC。其他人可以用AAA取代飞机。您可以定义任意数量的规则来定义任何转换。



计算机科学家通常需要知道给定的合资企业是否总是结局。也就是说，无论以哪条线开头以及以什么顺序应用规则，这条线最终会变成无法应用规则的状态，这是真的吗？



Aaronson提出了一个带有七个符号和11条规则的SP，类似于Collat​​z的假设。如果他们能够证明他的合资企业总是会结束，那么他们将证明该假设是正确的。



为了将Collat​​z的猜想变成一个SAT解算器问题，Aaronson和Hiyul必须采取进一步的步骤，涉及矩阵或数字数组。他们需要为其SP中的每个符号分配唯一的矩阵。这种方法是寻找SP正在完成工作的证据的一种常见方式，它将使他们能够通过矩阵乘法来推理数字转换。用SP表示七个符号的七个矩阵必须满足整套约束，这反映了11个规则之间的对应关系。



“首先，您尝试找到满足这些约束的矩阵，”他说卡内基梅隆大学的博士生Emre Yolchu与Hijul合作解决了这个问题。 “如果成功，您将证明执行停止。”因此，Collat​​z的假设是正确的。



SAT求解器可以回答存在满足这些约束条件的矩阵的问题。 Aaronson和Hijul首先在小型2x2矩阵上运行SAT求解器。他们没有找到工作的选择。然后他们尝试了3x3矩阵。再次无济于事。他们继续增加矩阵的大小，希望能够找到它们。



但是，这种方法不能无限发展，因为寻找合适矩阵的复杂度随其大小呈指数增长。 Hijul建议，现代计算机根本无法处理大于12x12的矩阵。



他说：“当矩阵过于复杂时，您将无法解决问题。”



Hijul仍在努力优化搜索，试图提高搜索效率，以便SAT求解器可以检查越来越大的矩阵。她和她的同事正在写一篇文章，总结他们目前的发现，但是他们几乎没有想法，可能很快就要放弃-至少要暂时放弃。



毕竟，SAT解算器的吸引力在于，如果您仅能弄清楚如何检查另一种情况，请给另一个保姆打电话，甚至将搜索范围延长一会儿，就可能找到所需的内容。从这个意义上讲，Khiyul的主要优势可能不是他在SAT解算器方面的经验，而是他对追求结果的热爱。



他说：“我只是一个乐观主义者。” “我常常觉得自己很幸运，所以我只想看看我能走多远。”