SAT Certificates for the Matrix-Multiplication Challenges over F2: All Ten `Expected-UNSAT` Instances Are Satisfiable, and a Type-3-Free Rank-23 Scheme

想象一下，你正在试图解决一个巨大的、三维的拼图。但这并不是一张日落或猫的照片；这是一个旨在将两个数字网格相乘的数学机器。在计算机科学和数学的世界里，这被称为“矩阵乘法”。几十年来，数学家们一直在寻找构建这个机器最有效的方法。他们想知道，要让整个机器运转起来，绝对最少需要多少个微小的、基础的构建模块（称为“乘法”）。

把这些构建模块想象成乐高积木。长期以来，大家都知道如何用 23 块积木构建一个 3x3 的乘法机器。大问题在于：我们能不能只用 22 块就完成？为了找出答案，研究人员将这个问题转化成了一个巨大的逻辑谜题，类似于你在视频游戏或数独书中看到的那些，但规模之大会让你的头晕目眩。他们将数学规则编码成一种计算机可以检查的格式，即一个“SAT”问题（代表“可满足性”）。如果计算机能找到一种方法，在不破坏任何规则的前提下将所有开关都拨到“开启”状态，那么谜题就解开了。如果计算机说“不可能”，那么也许 22 块积木确实不够用。这篇论文深入探讨了一组特定的逻辑谜题，这些谜题旨在测试我们现有计算机以及对这些数学机器理解的极限。

---

一个并非“不可能”的伟大谜题

见见尼克·帕拉迪诺斯（Nick Palladinos），一位数字侦探，他决定对一组被其他人放弃了的十个逻辑谜题进行全新的审视。这些被称为“挑战 2”的实例是由其他研究人员构建的，具有非常特定且僵化的规则。这些谜题的创造者认为它们是“不可能”解决的。他们认为规则如此严苛，以至于没有任何 23 块乐高积木的组合能够拼凑出这个机器。这就像是被告知：“这里有一个带锁的盒子，它绝对无法被打开，”而所有人都只是点了点头，然后走开了。

但帕拉迪诺斯并没有试图用一把更大的锤子去强行砸开锁，相反，他观察了锁本身，并意识到了一件至关重要的事情：规则并不像大家想象中那样严格。

谜题的创造者使用“正面”指令编写了规则。他们说，“你必须在这里有这块特定的积木，”以及“你必须在那里有那块积木。”但他们忘了说，“而且你不能有其他积木与这些积木接触。”事实证明，数学允许添加额外的积木，只要最终的机器仍然能正确工作即可。那些“不可能”的谜题实际上只是在等待有人意识到门并没有锁上；只是大家之前都试图把拼图碎片塞进一个太小的盒子里，却忽略了那个盒子其实可以稍微大一点。

位移与交换的魔力

那么，帕拉迪诺斯是如何解决它们的呢？他使用了一个涉及“对称性”的巧妙技巧。想象一下你有一个魔方。如果你旋转整个魔方或转动它，颜色会移动，但魔方本身还是同一个物体。帕拉迪诺斯意识到，他正在构建的这个数学“机器”也有类似的属性。他可以拿一个工作的解决方案（一组成功进行 3x3 矩阵乘法的 23 块积木）并利用一种被称为“GL(3, 2) 群作用”的特殊数学舞蹈，来旋转、转动或重新排列这些碎片。

这就像是在重新布置房间里的家具。你可以把沙发向左移动，把灯向右移动，把地毯放在中间。房间仍然是一个房间，家具仍然可以正常使用，只是布局不同了。帕拉迪诺斯拿了一个已知的、工作的解决方案，并应用了这些数学上的“扭转”。然后，他使用一个匹配游戏，来看看这些经过重新排列的“家具版本”是否能完美契合到那些棘手谜题所要求的特定“插槽”中。

你猜怎么着？它们完美契合！

事实上，帕拉迪诺斯不仅仅找到了一个解；他为所有十个原本被认为是不可能解决的谜题都找到了解。他证明了这些所谓的“不可解”公式实际上是可满足的。计算机不仅仅是在瞎猜；它检查了每一条规则。论文确认，对于所有 10 个“挑战 2”文件，都存在一种有效的排列 23 块构建模块来使机器工作的方案。那个“不可能”的标签其实是一种误解，而非真正的数学障碍。

“幽灵”积木与完美解

这篇论文还处理了第三个挑战——“挑战 3”。这个挑战提出了一个不同的问题：我们能否在用 23 块积木构建机器的同时，确保其中一块特定的积木是“幽灵”式的？用数学术语来说，这意味着 23 块积木中的一块应该具有“类型-3 计数”为零的特征。这是一种高级说法，意味着其中一块积木不应该参与到这些机器中通常会出现的一种特定常见模式中。

帕拉迪诺斯也做到了这一点。他从一个工作的解决方案开始，进行了一次微小而精确的交换。他拿了两块正在执行特定任务的积木，并用另外两块虽然执行同样工作但外观不同的积木替换了它们。这次交换如此巧妙，以至于它创造了一个“幽灵”积木——一个完全不会触发那种禁忌模式的积木。他证明了你确实可以用 23 块积木构建 3x3 矩阵乘法机器，且其中一块积木完全不受该特定模式的影响。

最终检查

为了确保没有人能说“噢，你只是靠运气骗过了计算机”，帕拉迪诺斯构建了一个极其严格的检查器。他为所有 21 个谜题（10 个来自挑战 1，10 个来自挑战 2，以及 1 个来自挑战 3）生成了完整的 26,541 个变量（即开关）列表。然后，他运行了一个独立的程序，读取原始的谜题规则和新的解决方案，检查了全部 2,461,316 条逻辑子句。

结果如何？零失败。每一条规则都得到了满足。这些解决方案是真实的，它们经过了验证，并且是可复现的。任何拥有合适软件的人都可以运行相同的代码，并在大约九秒钟内得到完全相同的答案。

这意味着什么（以及并不意味着什么）

所以，主要的启示是什么？这篇论文表明，那些“不可能”的谜题其实一直都是可以解决的；只是规则不像谜题制作者想象得那么紧凑。它提醒我们，在数学和计算机科学中，有时最难的部分不是寻找解决方案，而是意识到问题并不像看起来那样彻底坏掉了。

然而，这里有一个陷阱。这篇论文解决的是针对特定数学世界“F2”的谜题（这就像是一个数字只能在 1 之后循环的世界，即 1+1=0）。它并没有证明我们可以构建一个 22 块积木的机器。寻找 22 块积木机器的任务（挑战 4）仍然是一个开放的问题。这篇论文也没有说这些解决方案适用于你在现实世界中使用（如工程学中使用的复数）的每一种数学。它只是解决了作为书写的特定逻辑谜题。

但对于那些被写出来的谜题，结论是明确的：所谓的“不可能”其实是可能的。门从来没有锁上；我们只是需要一把正确的钥匙来转动把手。