卡内基梅隆大学拜伦·斯皮斯著 几十年来，约翰·麦基(左)和玛丽·赫勒一直在研究一个被称为凯勒猜想的数学难题
他们通过把它转化为可满足性问题找到了解决办法
信用:斯蒂芬·亨德森 卡内基梅隆大学的计算机科学家和数学家解决了凯勒猜想中最后一个顽固的问题，这是一个困扰科学家90年的几何问题
通过将这个难题构造成计算机科学家所说的可满足性问题，研究人员用四个月的疯狂计算机编程和仅仅30分钟的计算机集群计算解决了这个问题
“当我们解决这个问题的时候，我真的很高兴，但是当问题消失的时候，我有点难过，”约翰·麦基说，他是计算机科学系和数学科学系的教授，30年前他还是研究生的时候就开始研究凯勒的猜想
“但后来我又感到高兴了
只有这种满足感
" 该解决方案是计算机科学副教授玛丽·赫勒(Marijn Heule)开创的一种方法的又一成功，她于去年8月加入了可持续发展委员会
豪勒使用SAT求解器——一种使用命题逻辑解决可满足性问题的计算机程序——来克服几个古老的数学挑战，包括毕达哥拉斯三元组问题和舒尔5号
“这个问题已经困扰了许多人几十年，几乎一个世纪了，”豪勒在谈到凯勒的猜想时说
“这确实是一个展示，展示了现在可以做的事情，而这在以前是不可能的
" 这个猜想是由德国数学家爱德华·奥特-海因里希·凯勒提出的，与瓷砖有关——具体来说，就是如何用大小相等的瓷砖覆盖一个区域，而没有任何缝隙或重叠
据推测，至少有两块瓷砖必须共享一条边，这对于每个维度的空间都是正确的
对于二维瓷砖和三维立方体，很容易证明是真的
截至1940年，该猜想已被证明适用于六维以下的所有维度
然而，在1990年，数学家证明了它在10维或10维以上是不适用的
这时，凯勒的猜想引起了当时夏威夷大学学生麦基的想象
他的办公室靠近大学的计算集群，他对此很感兴趣，因为这个问题可以用离散图论的方法转化成计算机可以探索的形式
在这种被称为凯勒图的形式中，研究人员可以搜索“小集团”——连接在一起但不共享一张脸的元素子集，从而推翻这个猜想
2002年，麦基做到了这一点，在第八维度发现了一个小团体
通过这样做，他证明了这个猜想在那个维度上是失败的，并且延伸到了第九个维度
这使得这个猜想在第七维度上没有得到解决
当海尔去年从德克萨斯大学来到CMU时，他已经因使用SAT解决方案解决长期悬而未决的数学问题而闻名
“我心想，也许我们可以用他的技术，”麦基回忆道
不久，他开始与休勒和约书亚·布拉肯西克讨论如何将SAT求解器用于凯勒猜想，约书亚·布拉肯西克是数学科学和计算机科学的双学位，目前正在攻读博士学位
D
斯坦福大学的计算机科学
SAT的求解者需要使用命题公式来构造问题——比如(A或不是B)和(B或C)，等等
-因此求解器可以检查满足所有条件的组合的所有可能变量
“有很多方法可以进行翻译，翻译的质量通常会决定你解决问题的能力，”豪勒说
凭借15年的经验，豪勒擅长翻译这些作品
他的研究目标之一是开发自动推理，这样翻译就可以自动完成，允许更多的人在他们的问题上使用这些工具
即使有高质量的翻译，在第七维度中要检查的组合数量也是令人难以置信的——一个324位的数字——即使有超级计算机也看不到解决方案
但豪勒和其他人运用了一些技巧来缩小问题的规模
例如，如果一个数据配置被证明不可行，他们可以自动拒绝依赖它的其他组合
由于大部分数据是对称的，如果在一种排列方式中达到死胡同，程序可以排除一种配置的镜像
使用这些技术，他们将搜索减少到大约10亿种配置
大卫·纳瓦埃斯博士参与了这项工作
D
罗彻斯特理工学院的学生，2019年秋天是访问研究员
一旦他们在一组40台计算机上运行他们的代码，他们最终得到了一个答案:这个猜想在第七维是正确的
“我们成功的原因是约翰在这个问题上有几十年的经验和洞察力，我们能够将其转化为计算机生成的搜索，”豪勒说
豪勒说，结果的证明完全是由计算机计算出来的，这与许多出版物将证明的计算机检查部分与其他部分的人工记录相结合形成对比
他指出，这让读者很难理解
凯勒解决方案的计算机证明包括解决方案的所有方面，其中包括由纳瓦埃斯贡献的对称性破缺部分，豪勒强调说，因此证明的任何方面都不需要依靠人工努力
“我们可以对这个结果的正确性有真正的信心，”他说
六月，在国际自动推理联合会议上，一篇描述由赫勒、麦基、布拉肯西克和纳瓦埃斯提出的解决方案的论文获得了最佳论文奖
麦基说，解决凯勒猜想有实际应用
科学家们寻找来推翻这一猜想的那些小团体，在生成能够加快数据传输速度的非线性代码方面非常有用
因此，SAT求解器可以用来寻找比以前更高维的非线性码
豪勒最近提议使用SAT求解器来解决一个更著名的数学问题:柯拉茨猜想
在这个问题中，想法是选择任何一个正整数，如果它是偶数就除以2，如果它是奇数就乘以3再加1
然后将相同的规则应用于结果数和每个连续的结果
推测是最终的结果总是1
豪勒承认，用SAT解决方案解决柯拉茨问题“是一个渺茫的希望”
但这是一个有抱负的目标，他补充说，他解释说，即使证明柯拉茨无法实现，SAT求解器也可以用来解决一些不那么令人生畏的数学问题
来源：由phyica.com整理转载自PH，转载请保留出处和链接！
