Z3 SMT浮点运算约束下密钥求解无返回结果问题咨询

• 浮点约束求解复杂度极高
  Z3的浮点理论求解默认采用位爆破策略，你的代码中涉及19次双精度浮点乘法、浮点转无符号位向量操作，叠加其他整数约束后，搜索空间呈指数级扩张，并非约束无解，而是求解耗时远超预期，感知上就是没有返回结果。而移除浮点约束后仅剩余整数约束，整数线性算术求解是Z3的强项，所以能快速返回大量结果。
• 潜在的精度匹配偏差
  你代码中使用的FPVal(float(i) * float(3.141592), Float(64))在转换为双精度浮点数时，可能和Python原生float运算的截断规则存在微小偏差，叠加多次运算后，可能导致部分实际满足Python版sum_mul_pi的密钥，不匹配Z3的浮点约束逻辑。
• 求解器优化不足
  默认的Solver实例对混合浮点+位向量+整数的约束场景适配性差，进一步拖慢了求解速度。

完全没必要在约束中引入浮点运算，直接把sum_mul_pi的逻辑等价转换为整数运算即可，Z3对整数约束的求解效率要高出几个数量级：

def sum_mul_pi_int(values):
    val = BitVecVal(0, 64)
    for i in range(0, len(values)):
        # 正数场景下整数除法朝零截断和int()效果完全一致，等价于int(values[i] * i * 3.141592)
        val += (values[i] * i * 3141592) / 1000000
    return val

# 替换原有浮点版本的约束即可
s.add(sum_mul_pi_int(key) == 39944)

修改后运行代码可以秒出符合要求的密钥。

如果必须保留浮点约束，可以调整Z3求解参数提升效率：

s = SolverFor("QF_FPBV")
set_param("fp.xform_simplify", True)

但该方案求解速度依然远低于整数等价方案，仅做参考。

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