Geek
解决了凯勒猜想的计算机科学家剑指3x+1问题
Marijn Heule在过去的几年中取得了辉煌战功。他应用被称为SAT solving (SAT表示“可满足性”，不是美国高考那个缩写)的计算机证明技术，征服了一系列令人印象深刻的数学问题：2016年的勾股三元数问题，2017年的舒尔数=5时的舒尔猜想，以及现在为凯勒猜想画上句号。
关于凯勒猜想，可见前文90年历史的凯勒猜想被数学家利用计算机解决
但是，卡内基梅隆大学的计算机科学家Heule拥有更大的雄心：Collatz猜想，它被许多人认为是数学中最臭名昭著的开放问题(也是最容易被表述的问题)。
考拉兹猜想Collatz conjecture，俗称3x+1猜想，大概是著名数学中表述最为简单的一个。但是，曾有知名数学家告诫年轻学者：不要碰考拉兹猜想！不要被命题那人畜无害的外表所蒙蔽，那是恶魔设下的陷阱啊！
所谓的考拉兹猜想，就是大名鼎鼎的3x+1猜想。具体的内容是说，任取一个自然数x，如果x是偶数，则除以2；反之，3x+1后，再除以2；如此得到的数字记为x1，对x1继续执行如上的操作得到x2……如此反复，最终必然能够得到数字1！
整套运算都没有脱离加减乘除的范围。
匹兹堡大学计算机证明领域的负责人Thomas Hales说：“我看不出如何使用SAT solving解决它。”不过与其他人一样，Hales仅谨慎地表示不乐观。“他非常擅长寻找将问题编码为SAT的巧妙方法。他在这方面确实出色。”
德克萨斯大学奥斯汀分校，正在与Heule合作攻坚Collatz猜想的Scott Aaronson补充说：“Marijn手里有一个锤子，那就是SAT solving——可能是世界上最伟大的一把锤子。所以他期望所有问题都能变成钉子。”时间会证明他是否可以将Collatz变成钉子。
至于说什么是SAT solving，简单来说：将问题转化为使用命题逻辑的计算机语句，并使用计算机确定是否有办法使这些语句的真值=1。
小红，小黄，小绿，小蓝四个人分别穿着红黄绿蓝四种颜色的衣服和红黄绿蓝四种颜色的裤子。已知条件如下：
1 只有1个人的名字与自己衣服的颜色相同；
2 只有1个人的名字与自己裤子的颜色相同；
3 没有1个人的名字与自己的衣服和裤子的颜色完全相同；
4 穿红衣服的人(不是小蓝)的名字与小蓝穿的裤子颜色相同；
5 穿蓝衣服的人(不是小黄)的名字与小黄穿的裤子颜色相同。
请问四人分别穿什么颜色的衣服和裤子？
一种检索方法是将人名和颜色约束条件转换为公式，然后输入SAT解算器。该程序将找出是否有办法(一般是循环为各个变量赋值0或1)使公式输出结果为true或“令人满意”。
不幸的是，数学中许多最重要的问题乍看之下和SAT问题毫无关系。但是有时可以用令人惊讶的方式将它们重新表述为可满足性问题。
为了将Collatz猜想转化成SAT问题，Aaronson和Heule必须采取进一步的措施。它涉及矩阵，他们将符号转换视为矩阵乘法。
卡内基·梅隆大学的研究生Emre Yolcu说：“您试图找到满足这些约束的矩阵。如果找到它们，就尝试证明他们的乘机不会越来越大。”亦即相当于证明了Collatz猜想。
“是否存在满足这些约束的矩阵？”是适用于SAT solving的一类问题。Aaronson和Heule在小型2×2矩阵上启动了SAT解算器。毫无效果。接下来，他们尝试了3×3矩阵。运气还是不佳。Heule和Aaronson不断增加矩阵的大小，希望能找到合适的矩阵。
但是，随着矩阵规模的增大，搜索正确矩阵的复杂性呈指数增长。Heule估计，任何大于12x12的矩阵都会噎死当今的计算机。
Heule仍在努力优化搜索，试图提高搜索效率。
毕竟，SAT solving的诱人之处在于，您只要构思出正确的算法，再有点耐心，便会得到想要的东西。在这方面，Heule最重要的资产可能不是他应用SAT solving的技术，而是他对真理和数学的热情。
他说：“我是乐观的人。我经常感到运气在自己这边，所以我想尝试一下，看看能走多远。”
https://www.quantamagazine.org/can-computers-solve-the-collatz-conjecture-20200826/