在图论(有限或无限图)里有一类问题叫 packing coloring(填充着色) 。

下面就是一个具体的packing coloring问题。

过平面里x轴上的整数坐标，做垂线垂直于x轴；对y轴同样处理。可把平面分割成一个个标准正方形的格子。

假设每个格子的几何中心的坐标是(Xi,Yi)我们可以定义平面上任意两个格子的距离:|Xi-Xj|+|Yi-Yj|(两竖代表绝对值)。(回忆一下通常的距离定义，感受一下区别。虽然在这里无关紧要，但以这种方式定义距离的几何学，叫出租车几何。)

按上面的距离定义，如果两个方格有一条公共边，显然它们之间的距离是1。但是如果两个方格仅有一个公共顶点(也就是斜对角那种)，则它们的距离是2。

现在，在每个方格里填上一个正整数(这就是着色，因为数字可以理解成颜色的代号)，同时要求，如果一个方格里的数字是n，则与它的距离在n以内的所有格子里的数字都不能是n。问：我们是否能用有限个数字完成着色？

上面就是平面无限格填充着色问题。

在2008年已经有人证明，22个数字就够了。但一直没有人能确定其精确下界。

结果到今年2月初，Bernardo Subercaseaux和Marijn J. H. Heule借助SAT solving计算机证明技术，证明15可以，但是14不行。最终彻底解决了该问题。

他们把这个问题翻译成复杂的布尔代数式，然后用计算机执行计算。为了排除14，去年计算机整整跑了4个月之久。这里简简单单一句话“把问题翻译成复杂的布尔代数式”，实际上如今全数学界也没有几个人能做到(为数不多的几个人里，恰有下面要稍加介绍的Heule)。因为问题千差万别，翻译也没有一定之规。这是一种极其需要创造性的思想方法。

SAT solving里SAT是satisfiablity的缩写，和美国高考无关。

SAT solving的历史可以追溯到上世纪60年代，当时Davis和Putnam提出了一种基于演绎推理的算法，通过对布尔公式进行迭代的存在量化和归结来判断其可满足性。这种算法被称为Davis-Putnam算法。

SAT在过去的几十年里取得了显著的进步，能够处理数百万个变量和约束的实际问题。SAT求解器在软件验证、程序分析、约束求解、人工智能、电子设计自动化等领域有着重要的应用和影响。

从上面可以看出来，SAT原本是用于计算机工程和逻辑规划上的技术。

以个人看法，把SAT solving方法应用于纯数学证明，是2000年之后出现的最伟大的数学思想。

同时，解决了平面无限格填充着色问题的两位合作者之一的卡内基梅隆大学的计算机科学家Heule，是当代SAT solving领域里最顶尖的大师(没有能与之相提并论的)。

过去20年，Heule凭借其对于SAT solving技术的超人感悟，解决了一连串猜想。

有位数学家赞叹曰：现在Heule Marijn手里有了一个锤子，那就是SAT solving——可能是世界上最伟大的一把锤子。所以他期望所有问题都能变成钉子。

后来或许是心态过于膨胀乐观，Heule认为著名的“3x+1”问题也可以看作是钉子。但到现在为止，实际上都是浪费时间。所幸大师这几年又把精力放回到更合理的问题上。

参考:
https://www.quantamagazine.org/the-number-15-describes-the-secret-limit-of-an-infinite-grid-20230420/

PREV : 大家听说过“一日一餐”(OMAD)饮食法吗
NEXT : 今日好价 0425