Revisiting Incremental Linearization for Nonlinear Integer Arithmetic

想象一下你是一名正在试图破解谜题的侦探，但你得到的线索是用一种其含义会根据观察角度而变化的语言编写的。这就是 可满足性模理论 (Satisfiability Modulo Theories, SMT) 的世界，它是计算机科学的一个分支，其中软件试图弄清楚一组逻辑规则是否能同时成立。你可以把它想象成一个超级聪明的解谜者，用于检查程序是否会崩溃、秘密代码是否会被破解，或者机器人的路径是否安全。

大多数情况下，这些谜题很容易解决，因为它们只涉及直线和简单的加法（比如 $x + y = 5$）。计算机在这方面表现出色。但当引入 非线性算术 (nonlinear arithmetic) 时——即规则涉及乘法或幂运算（如 $x \times y$ 或 $x^3$）——生活就会变得混乱。突然间，规则变得弯曲且扭曲，数学问题变得异常困难。事实上，对于整数而言，创造一种完美的、100% 完整的、能解决所有此类谜题的方法在数学上是不可能的。因此，计算机科学家构建了“足够好”的侦探，他们使用巧妙的捷径来快速寻找答案，即使他们无法保证能解决每一个不可能的案例。

你即将阅读的这篇论文介绍了一位名为 qfn2l 的新侦探，它比以前的侦探更擅长解决这些棘手的、弯曲的谜题。作者们（来自布拉格捷克理工大学的研究人员）意识到，旧的捷径在处理一种特定类型的困难谜题时显得力不从心：即涉及 幂运算（如 $x^3$）和 混合乘积（如 $x^2y$）的谜题。他们决定为这位侦探的工具箱升级一套全新的规则，这套规则就像一个更紧密的网，能够捕捉到以前那些会溜掉的错误猜测。

旧方法：使用未解释函数进行猜测

为了理解这次升级，让我们看看之前的侦探是如何工作的。想象你有一个贴着标签 $f(x, y)$ 的神秘盒子。你不知道里面装了什么，但你知道如果输入相同的数字，就会得到相同的输出。旧方法将每一次乘法（如 $x \times y$）都视为这样一个神秘的盒子。计算机会猜测这个盒子的值，检查它是否合理，如果不对，它就会添加一条规则来修正这个猜测。

这种方法在简单情况下表现尚可，但就像是通过仅仅知道一个西瓜是“重”的来猜测它的重量一样。这太模糊了。当谜题涉及高次幂（如 $x^3$）时，旧的规则过于宽松。侦探会做出一个猜测，计算机会说：“不对，这不符合要求”，然后添加一条非常微弱的规则来修正。侦探必须不断地经历猜测、失败、再猜测的过程，往往在找到答案之前就耗尽了时间。

新技巧：用割线 tightening 紧缩网络

本文的作者决定不再将这些幂运算视为神秘的盒子，而是将其视为 新鲜的常数 (fresh constants)——即代表幂运算结果的普通、简单的数字。但真正的魔力在于他们用来检查这些数字的新规则。

他们发现，对于任何整数 $v$，函数 $x^k$（如 $x^3$）在 $v$ 和 $v+1$ 之间表现得非常有规律。他们创建了一套基于 割线 (secant lines) 的新规则。想象一下图表上的曲线。一条割线是连接曲线上两点的直线。作者们意识到，如果你在点 $(v, v^k)$ 和下一个整数点之间画一条直线，这条线就会在曲线周围形成一个非常紧密的“围栏”。

以下是类比：

• 旧方法： 侦探在可能的答案周围画了一个巨大的、松散的圆圈。这很容易画出来，但会让很多错误的猜测进入。
• 新方法： 侦探画出一系列紧密的、笔直的围栏（割线），紧紧贴合答案的曲线。如果一个猜测落在这些紧密的围栏之外，侦探会立即知道它是错误的，并添加一条规则将猜测推回圈内。

因为这些围栏如此紧密，侦探不需要进行那么多次猜测。它能更快地收敛到正确答案，尤其是在处理涉及立方和混合乘积的谜题时。

“三立方之和”挑战

为了证明他们的新侦探确实有效，作者们在一种著名的谜题类别上对其进行了测试，即“三立方之和 (sum of three cubes)”。这些问题是在问：“能否找到三个整数，使它们的立方和等于一个特定的数字？”

例如，谜题可能是：$x^3 + y^3 + z^3 = 79$。

这是标准求解器的噩梦。数字可能非常巨大，且关系复杂。作者们将他们的新求解器 qfn2l 与现有的顶尖求解器（如 Z3, cvc5 和 MathSAT）进行了对比测试。

• 其他求解器尝试解决 $x^3 + y^3 + z^3 = 79$ 谜题，但在 3 分钟后放弃了（它们“超时”了）。
• 新求解器 qfn2l 只用了 20 秒 就找到了答案——$x = -19, y = 35, z = -33$。

结果：一个具有竞争力的挑战者

研究人员在来自标准库 SMT-LIB 的 25,444 个谜题的大型集合上运行了他们的求解器。以下是他们的发现：

1. 整体性能： 新求解器与现有的顶级工具相比具有竞争力。它总共解决了大约 14,000 个谜题，这接近于顶尖水平，尽管它并没有在 每一种 类型的问题上都击败最强的对手（如 Z3）。
2. 优势领域： 新求解器在由幂运算和混合乘积主导的谜题上表现极其出色。在“MathProblems”系列（包括三立方之和）中，它解决了约 53% 的实例（1,100 个中的 585 到 587 个）。其他求解器在处理这些特定类型的题目时明显更加吃力。
3. 权衡： 作者测试了一个尝试在检查不同部分是否一致（称为“同余公理/congruence axioms”）方面更加谨慎的版本。他们发现，这种额外的检查实际上减慢了求解器在处理一般性问题时的速度，导致总共减少了约 1,600 个实例的解决量。这表明对于大多数问题，紧密的围栏（割线界限）已经足够了，并不需要进行额外的繁重检查。

为什么这很重要

这篇论文并不声称自己解决了不可解的问题。他们承认，由于该问题在数学上是不可判定的，没有任何计算机能解决所有案例。然而，他们展示了通过改变我们近似这些弯曲、非线性规则的方式——特别是通过使用这些基于割线的紧密围栏——我们可以让这些“足够好”的侦探变得更加聪明。

他们构建了一个开源工具，并在现有的引擎（Z3）之上运行，证明了在处理最难的整数谜题时，一种更聪明的策略可以击败暴力破解法。对于任何试图验证软件是否会崩溃或加密协议是否安全的人来说，这种新方法为检查背后的数学逻辑提供了一种更快、更可靠的方式。

简而言之，作者将一个杂乱、弯曲的问题，在周围画出了更紧密的线条，从而让计算机能够比以前更快地找到真相。