乘法与除法运算优化问题排查：Z3求解结果异常

首先得戳破核心点：Z3对非线性整数算术（整数乘法、除法都属于这类）的支持是启发式的，而非完备算法——这也是你查的那篇文章要讲的核心：非线性整数问题本身是不可判定的，没有通用解法能保证所有情况都给出sat/unsat的明确结果，Z3只能靠启发式搜索碰运气，运气不好就会返回unknown。

接下来拆解你的问题：

1. 为什么结果不符合预期？ #

先排查两个关键：

（1）约束是否存在整数解？ #

先手动验算你的预期结果：如果除法结果是4，乘法是8000000，假设约束是x / y = 4且x * y = 8000000——那代入x=4y到乘法约束，会得到4y²=8000000，即y²=2000000，但2000000不是完全平方数，根本没有整数解。如果是这种情况，Z3返回unknown甚至unsat都是合理的，因为你的预期本身在整数域里不成立。

如果你的约束逻辑是另一种（比如y = 8000000 / x且结果为4，即x=2000000，y=4，这时候x*y=8000000完全成立），那可能是你在代码里的约束写法有问题：

• Z3的整数除法是向零截断的，如果你需要精确整除，必须额外添加x % y == 0的约束，否则17 / 4会被算成4，但17和4的乘积显然不是8000000。
• 变量是否没设置范围？如果变量的取值空间是整个整数域，Z3的搜索空间会直接爆炸，很容易放弃并返回unknown。

（2）Z3的默认策略没触发有效搜索 #

Z3对非线性约束的默认启发式不一定能覆盖你的场景，尤其是当变量范围无界时，它可能找不到解。

2. 解决办法 #

针对你的情况，试试这几个调整：

（1）明确约束的精确性 #

如果需要除法是精确整除，一定要加上余数为0的约束：

from z3 import *

x, y = Ints('x y')
s = Solver()
# 精确整除约束，确保除法无余数
s.add(x % y == 0)
# 业务约束：用存在整数解的例子
s.add(x / y == 4)
s.add(x * y == 8000000)
# 排除负数干扰（根据你的业务场景调整）
s.add(y > 0)
s.add(x > 0)

print(s.check())
if s.check() == sat:
    m = s.model()
    print(f"x = {m[x]}, y = {m[y]}")

这个例子里，Z3会直接返回sat，并给出正确的整数解。

（2）给变量添加合理的上下界 #

Z3在处理无界变量时搜索效率极低，给变量设置符合业务场景的范围，能大幅提升求解成功率。比如你知道x不会超过1e7，y不会超过1e6，就加上：

s.add(x <= 10000000)
s.add(y <= 1000000)

（3）切换Z3的求解策略 #

可以尝试启用模型基量词实例化（MBQI），这对部分非线性整数问题有帮助：

s.set("smt.mbqi", True)

或者启用非线性算术的专用策略（新版本Z3可能默认开启，但手动开启更保险）：

s.set("nl-arith", True)

3. 关键结论 #

• 非线性整数算术的不可判定性是Z3返回unknown的根本原因，不要指望它能解决所有这类问题；
• 先手动验证你的约束是否存在整数解，避免预期本身不合理；
• 通过添加精确性约束、缩小变量范围、调整求解策略，能让Z3在大多数简单场景下找到解。

内容的提问来源于stack exchange，提问作者Frank Wawrzik