Marijn Heule在过去的几年中取得了辉煌战功。他应用被称为SAT solving (SAT表示“可满足性”，不是美国高考那个缩写)的计算机证明技术，征服了一系列令人印象深刻的数学问题：2016年的勾股三元数问题，2017年的舒尔数=5时的舒尔猜想，以及现在为凯勒猜想画上句号。
关于凯勒猜想，可见前文90年历史的凯勒猜想被数学家利用计算机解决
但是，卡内基梅隆大学的计算机科学家Heule拥有更大的雄心：Collatz猜想，它被许多人认为是数学中最臭名昭著的开放问题(也是最容易被表述的问题)。
考拉兹猜想Collatz conjecture，俗称3x+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/
联系客服
