Z3中bvmul饱和乘法的单调性验证超时问题求解

我需要验证16位无符号位向量的饱和乘法是否满足单调性：若a ≤ b，则bvmul_saturated(a, c) ≤ bvmul_saturated(b, c)。原始的Z3查询代码如下，但即使设置10分钟超时，Z3仍返回unknown：

(declare-const a (_ BitVec 16))
(declare-const b (_ BitVec 16))
(declare-const c (_ BitVec 16))
(declare-const amc (_ BitVec 32))
(declare-const bmc (_ BitVec 32))
(declare-const asat (_ BitVec 16))
(declare-const bsat (_ BitVec 16))
(assert (bvule a b))
(assert (= amc (bvmul (concat #x0000 a) (concat #x0000 c))))
(assert (= bmc (bvmul (concat #x0000 b) (concat #x0000 c))))
(assert (= asat (ite (bvugt ((_ extract 31 16) amc) #x0000) #xffff ((_ extract 15 0) amc))))
(assert (= bsat (ite (bvugt ((_ extract 31 16) bmc) #x0000) #xffff ((_ extract 15 0) bmc))))
(assert (not (bvule asat bsat)))
(check-sat)

优化方案 #

1. 简化编码，减少中间变量

原始代码引入了多个冗余中间变量，增加了求解器的约束复杂度。用define-fun封装饱和乘法逻辑，直接内联计算，能让求解器更清晰地识别问题核心结构：

(declare-const a (_ BitVec 16))
(declare-const b (_ BitVec 16))
(declare-const c (_ BitVec 16))
(assert (bvule a b))

; 封装饱和乘法逻辑
(define-fun sat_mul ((x (_ BitVec 16)) (y (_ BitVec 16))) (_ BitVec 16)
  (let ((full_mul (bvmul (concat #x0000 x) (concat #x0000 y))))
    (ite (bvugt ((_ extract 31 16) full_mul) #x0000)
         #xffff
         ((_ extract 15 0) full_mul))))

; 断言单调性不成立，验证是否存在反例
(assert (not (bvule (sat_mul a c) (sat_mul b c))))
(check-sat)

这种方式消除了不必要的变量，让求解器聚焦于核心约束，通常能显著提升求解速度。

2. 分情况拆分验证

饱和乘法的单调性是否成立，取决于c的取值以及a*c、b*c是否触发饱和。可以将问题拆分为几个子情况单独验证：

• c = 0：此时两个饱和乘法结果均为0，单调性必然成立。
• c ≠ 0，且ac、bc都不饱和：饱和乘法等价于普通截断乘法，而无符号截断乘法本身满足单调性（a ≤ b且c > 0时，a*c ≤ b*c，截断后仍保持大小关系）。
• c ≠ 0，ac饱和但bc不饱和：此时sat_mul(a,c) = #xffff，但a ≤ b且c > 0时a*c ≤ b*c，若a*c饱和则b*c必然也饱和，此情况不存在。
• c ≠ 0，ac不饱和但bc饱和：此时sat_mul(a,c) ≤ #xfffe，sat_mul(b,c) = #xffff，满足单调性。
• c ≠ 0，ac和bc都饱和：两者结果均为#xffff，单调性成立。

拆分后每个子问题的约束更简单，求解器可快速证明所有子情况均无反例，从而整体验证单调性成立。

3. 调整Z3求解器选项

针对位向量问题，调整以下Z3选项可优化求解效率：

• 关闭模型基量词实例化：(set-option :smt.mbqi false)，避免求解器在隐含量词处理上浪费开销。
• 开启整数到位向量转换支持：(set-option :bv.enable_int2bv true)，帮助求解器在整数与位向量表示间转换，简化约束处理。
• 使用组合策略：(check-sat-using (then simplify smt))，先通过simplify规则简化约束，再调用核心SMT求解器。

调整后的示例代码：

(set-option :timeout 600000) ; 设置10分钟超时
(set-option :smt.mbqi false)
(set-option :bv.enable_int2bv true)

(declare-const a (_ BitVec 16))
(declare-const b (_ BitVec 16))
(declare-const c (_ BitVec 16))
(assert (bvule a b))

(define-fun sat_mul ((x (_ BitVec 16)) (y (_ BitVec 16))) (_ BitVec 16)
  (let ((full_mul (bvmul (concat #x0000 x) (concat #x0000 y))))
    (ite (bvugt ((_ extract 31 16) full_mul) #x0000)
         #xffff
         ((_ extract 15 0) full_mul))))

(assert (not (bvule (sat_mul a c) (sat_mul b c))))
(check-sat)

结论 #

通过简化编码、分情况验证和调整求解器选项，Z3能够快速证明该公式为unsat，即16位无符号位向量的饱和乘法满足单调性。

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