适用于域初等代数的最佳Z3策略：解决有效性证明超时问题

问题描述 #

要证明的代数语句：

∀ a b: ℤ, ~ b = 0 -> (a / b) ^ 2. = (a * a) / (b * b)

对应的SMT-LIB代码：

(declare-fun b () Int)
(declare-fun a () Int)
(assert (=> (= b 0) false))
(assert (let ((a!1 (= (^ (/ (to_real a) (to_real b)) 2.0)
              (/ (to_real (* a a)) (to_real (* b b))))))
  (not a!1)))
(check-sat)

运行时遇到的问题：用默认策略会超时，推测Z3在不断实例化整数找反例上浪费了太多时间。我们只需要得到unsat结果来证明原语句有效，需要找合适的战术组合。

可行的战术组合 #

这类问题本质是实数域的代数恒等式验证，没必要让Z3在整数实例化上耗时间，直接用针对实数算术的战术就能快速解决，推荐以下几种方式：

1. 直接用qfnra-nlsat战术 #

这个战术专门处理无量纲的非线性实数算术问题，正好匹配我们的场景（原全称量词已通过取反转为存在量词，属于无量纲问题）。修改代码加入战术调用：

(declare-fun b () Int)
(declare-fun a () Int)
(assert (=> (= b 0) false))
(assert (let ((a!1 (= (^ (/ (to_real a) (to_real b)) 2.0)
              (/ (to_real (* a a)) (to_real (* b b))))))
  (not a!1)))
(check-sat-using (then simplify qfnra-nlsat))

• 先跑simplify做基础化简，比如展开逻辑蕴含、处理整数转实数的初步转换
• 再调用qfnra-nlsat直接用非线性实数算术求解器，跳过无意义的整数实例化，专注代数等式验证

2. 结合值传播与非线性求解器 #

如果需要更精细的控制，可以先做值传播缩小变量范围，再调用求解器：

(check-sat-using (then simplify propagate-values nlsat))

propagate-values会先把b≠0的约束传递到后续算术表达式里，减少求解器需要处理的变量空间，加快验证速度。

3. 禁用整数相关的冗余处理 #

如果默认策略还在固执地试整数实例，可以直接关闭整数域的格罗比纳基处理，强制求解器聚焦实数域：

(check-sat-using (then simplify (using-params qfnra-nlsat :smt.arith.nl.gb false)) )

:smt.arith.nl.gb false这个参数会关闭整数相关的非线性处理逻辑，让求解器完全投入到实数代数恒等式的证明中。

为什么这些战术有效 #

原问题的核心是验证实数域的代数恒等式，Z3默认策略会优先尝试整数实例化找反例，但对于恒等式来说，这种尝试完全是浪费时间。选择专门处理实数非线性算术的战术，能直接跳过整数实例化步骤，通过符号化简和代数计算快速得出unsat结果，证明原语句的有效性。

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