引导Z3证明搜索：解决整数非线性算术幂运算超时问题

我在尝试用Z3处理简单的整数非线性算术问题时，遇到了幂运算相关的性能瓶颈。具体来说，我需要验证类似x^{a+b+2} = x * x * x^a * x^b这类仅涉及非负指数的等式，但即使通过递归函数定义幂运算（非正指数返回1），并添加了用于推导x^{a+b} = x^a * x^b的模式，Z3仍然会超时。

我的代码如下：

(define-fun-rec pow ((x!1 Int) (x!2 Int)) Int (if (<= x!2 0) 1 (* x!1 (pow x!1 (- x!2 1))))) 
; split + 
(assert (forall ((a Int) (b Int) (c Int)) (! (=> (and (>= b 0) (>= c 0)) (= (pow a (+ b c)) (* (pow a c) (pow a b)))) :pattern ((pow a (+ b c)))))) 
; small cases 
(assert (forall ((a Int)) (= 1 (pow a 0)))) 
(assert (forall ((a Int)) (= a (pow a 1)))) 
(assert (forall ((a Int)) (= (* a a) (pow a 2)))) 
(assert (forall ((a Int)) (= (* a a a) (pow a 3)))) 
; Our problem 
(declare-const x Int) 
(declare-const i Int) 
(assert (>= i 0)) 
; This should be provably unsat, by splitting and the small case for 2 
(assert (not (= (* (* x x) (pow x i)) (pow x (+ i 2))))) 
(check-sat) ;times out 

问题分析：模式与递归的效率瓶颈 #

你遇到的超时问题，核心在于递归函数的量词实例化效率：

1. 你定义的通用x^{b+c} = x^b * x^c规则，模式(pow a (+ b c))需要Z3将目标中的(pow x (+ i 2))匹配为b=i、c=2，但常量与变量的组合会增加实例化的搜索成本。
2. 递归函数的本质是迭代展开，Z3在处理时可能陷入无限递归展开的循环，尤其是当指数为变量时，会生成大量子项拖慢推理。

优化方案：针对性调整规则与定义 #

1. 用特定引理替代通用规则

与其让Z3从通用的a+b规则推导i+2的情况，不如直接添加针对目标场景的引理，缩小量词实例化的搜索范围：

(define-fun-rec pow ((x Int) (n Int)) Int 
  (if (<= n 0) 1 (* x (pow x (- n 1)))))

; 直接添加针对i+2场景的引理，模式完全匹配目标
(assert (forall ((x Int) (i Int)) 
  (! (=> (>= i 0) (= (pow x (+ i 2)) (* x x (pow x i)))) 
     :pattern ((pow x (+ i 2))))))

; 问题实例
(declare-const x Int)
(declare-const i Int)
(assert (>= i 0))
(assert (not (= (* x x (pow x i)) (pow x (+ i 2)))))
(check-sat) ; 会快速返回unsat

2. 改用内置幂运算+重写规则

Z3内置的^运算符对整数幂运算有原生支持，配合针对性的重写规则，比自定义递归函数更高效：

; 限定非负指数的幂运算加法规则
(assert (forall ((x Int) (a Int) (b Int)) 
  (! (=> (and (>= a 0) (>= b 0)) (= (^ x (+ a b)) (* (^ x a) (^ x b)))) 
     :pattern ((^ x (+ a b))))))

; 基础情况补充
(assert (forall ((x Int)) (= (^ x 0) 1)))
(assert (forall ((x Int)) (= (^ x 1) x)))

; 问题实例
(declare-const x Int)
(declare-const i Int)
(assert (>= i 0))
(assert (not (= (* x x (^ x i)) (^ x (+ i 2)))))
(check-sat) ; 快速返回unsat

3. 使用战术引导推理

Z3的战术（Tactics）可以手动引导推理流程，比如结合量词消去（qe）和SMT求解，避免无效的递归展开：

(define-fun-rec pow ((x Int) (n Int)) Int 
  (if (<= n 0) 1 (* x (pow x (- n 1)))))

(declare-const x Int)
(declare-const i Int)
(assert (>= i 0))
(assert (not (= (* x x (pow x i)) (pow x (+ i 2)))))
; 先用量词消去简化，再调用SMT求解
(apply (then qe smt))

关键总结 #

• 避免过度依赖通用规则：针对目标场景写特定引理，能大幅减少Z3的搜索开销。
• 递归函数需谨慎使用：内置运算符通常比自定义递归函数的推理效率更高。
• 战术辅助：复杂问题下，手动指定推理流程能避免Z3陷入低效的搜索路径。

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