SMT2Lib添加非负性断言后求解器不终止的优化方案咨询

我们基于SMT2Lib开发加权均值函数求解器，使用CVC5或Z3运行。添加断言(assert (> tau0_max 0))（确保分母非负）后程序无法终止。场景不适用整数类型，希望使用有理数，目前采用SMT2Lib提供的实数类型，求参数调整或函数声明的替代方案。

原SMT2代码如下：

(set-option :produce-assignments true)
(set-option :produce-models true)
(set-option :produce-proofs true)

(set-logic ALL)
;define data points x_0 x_1 x_2
(declare-fun x (Int) Real)
(declare-fun n () Int)

(define-fun sqr ((x Real)) Real (* x x))
(define-fun max ((x Real) (y Real)) Real (ite (> x y) x y))
;(define-fun c0 ((i Int)) Real 1.0)

(define-fun miu () Real (/ (+ (x 0) (+ (x 1) (+ (x 2) (+ (x 3) (+ (x 4) (+ (x 5) (+ (x 6) (+ (x 7) (+ (x 8) (+ (x 9) (x 10))))))))))) 11.0))
(define-fun miu_c0 () Real (/ (+ (x 0) (+ (x 1) (+ (x 2) (+ (x 3) (+ (x 4) (+ (x 5) (+ (x 6) (+ (x 7) (+ (x 8) (+ (x 9) (+ (x 10) (x 11)))))))))))) 12.0))

(define-fun tau0 ((i Int)) Real (sqr (- (x i) miu_c0)))

(define-fun tau0_max () Real (max (tau0 0) (max (tau0 1) (max (tau0 2) (max (tau0 3) (max (tau0 4) (max (tau0 5) (max (tau0 6) (max (tau0 7) (max (tau0 8) (max (tau0 9) (max (tau0 10) (tau0 11)))))))))))))

(assert (> tau0_max 0))

(define-fun c1 ((i Int)) Real (- 1.0 (/ (tau0 i) tau0_max)))

(define-fun miu_c1 () Real (/ (+ (* (c1 0) (x 0)) (+ (* (c1 1) (x 1)) (+ (* (c1 2) (x 2)) (+ (* (c1 3) (x 3)) (+ (* (c1 4) (x 4)) (+ (* (c1 5) (x 5)) (+ (* (c1 6) (x 6)) (+ (* (c1 7) (x 7)) (+ (* (c1 8) (x 8)) (+ (* (c1 9) (x 9)) (+ (* (c1 10) (x 10)) (* (c1 11) (x 11))))))))))))) 12.0))

(define-fun tau1 ((i Int)) Real (sqr (- (x i) miu_c1)))

(define-fun tau1_max () Real (max (tau1 0) (max (tau1 1) (max (tau1 2) (max (tau1 3) (max (tau1 4) (max (tau1 5) (max (tau1 6) (max (tau1 7) (max (tau1 8) (max (tau1 9) (max (tau1 10) (tau1 11)))))))))))))

(define-fun c2 ((i Int)) Real (* (c1 i) (- 1.0 (/ (tau1 i) tau1_max))))

(assert (= (c2 0) 1.0))

(check-sat)
(get-model)

1. 展开嵌套max的非线性约束 #

原代码中嵌套的max函数会生成复杂的非线性约束，导致求解器陷入无限搜索。将tau0_max的定义替换为一组线性断言：

• 断言tau0_max大于等于所有tau0(i)
• 断言至少存在一个tau0(i)等于tau0_max
• 同时保留tau0_max > 0的约束

这种方式将非线性的max转换为线性约束的合取，降低求解器的计算负担。

2. 关闭证明生成选项 #

原代码开启的:produce-proofs true选项会强制求解器生成证明过程，大幅增加计算开销。对于只需要模型的场景，关闭此选项能显著提升求解速度。

3. 指定精确的逻辑 #

原代码使用ALL逻辑，求解器需要处理所有理论分支，效率极低。替换为QF_NRA（无量词非线性实数算术），让求解器针对性优化处理当前问题的算术约束。

4. 强制有理数算术模式 #

• Z3：添加命令行参数--rational，或在代码中设置(set-option :precision 53)（确保用有理数而非浮点数近似）
• CVC5：添加命令行参数--rational，强制使用有理数算术而非实数近似

(set-option :produce-assignments true)
(set-option :produce-models true)
; 关闭证明生成以提升性能
;(set-option :produce-proofs true)

; 指定无量词非线性实数算术逻辑
(set-logic QF_NRA)

; 定义数据点x_0到x_11，避免使用Int参数化函数（减少理论混合）
(declare-fun x0 () Real)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun x4 () Real)
(declare-fun x5 () Real)
(declare-fun x6 () Real)
(declare-fun x7 () Real)
(declare-fun x8 () Real)
(declare-fun x9 () Real)
(declare-fun x10 () Real)
(declare-fun x11 () Real)

(define-fun sqr ((x Real)) Real (* x x))

(define-fun miu () Real (/ (+ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) 11.0))
(define-fun miu_c0 () Real (/ (+ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) 12.0))

; 定义各个tau0值
(define-fun tau0_0 () Real (sqr (- x0 miu_c0)))
(define-fun tau0_1 () Real (sqr (- x1 miu_c0)))
(define-fun tau0_2 () Real (sqr (- x2 miu_c0)))
(define-fun tau0_3 () Real (sqr (- x3 miu_c0)))
(define-fun tau0_4 () Real (sqr (- x4 miu_c0)))
(define-fun tau0_5 () Real (sqr (- x5 miu_c0)))
(define-fun tau0_6 () Real (sqr (- x6 miu_c0)))
(define-fun tau0_7 () Real (sqr (- x7 miu_c0)))
(define-fun tau0_8 () Real (sqr (- x8 miu_c0)))
(define-fun tau0_9 () Real (sqr (- x9 miu_c0)))
(define-fun tau0_10 () Real (sqr (- x10 miu_c0)))
(define-fun tau0_11 () Real (sqr (- x11 miu_c0)))

; 声明tau0_max并展开max约束
(declare-fun tau0_max () Real)
(assert (> tau0_max 0))
; tau0_max >= 所有tau0_i
(assert (>= tau0_max tau0_0))
(assert (>= tau0_max tau0_1))
(assert (>= tau0_max tau0_2))
(assert (>= tau0_max tau0_3))
(assert (>= tau0_max tau0_4))
(assert (>= tau0_max tau0_5))
(assert (>= tau0_max tau0_6))
(assert (>= tau0_max tau0_7))
(assert (>= tau0_max tau0_8))
(assert (>= tau0_max tau0_9))
(assert (>= tau0_max tau0_10))
(assert (>= tau0_max tau0_11))
; 至少有一个tau0_i等于tau0_max
(assert (or (= tau0_max tau0_0) (= tau0_max tau0_1) (= tau0_max tau0_2)
            (= tau0_max tau0_3) (= tau0_max tau0_4) (= tau0_max tau0_5)
            (= tau0_max tau0_6) (= tau0_max tau0_7) (= tau0_max tau0_8)
            (= tau0_max tau0_9) (= tau0_max tau0_10) (= tau0_max tau0_11)))

; 定义c1函数对应各个值
(define-fun c1_0 () Real (- 1.0 (/ tau0_0 tau0_max)))
(define-fun c1_1 () Real (- 1.0 (/ tau0_1 tau0_max)))
(define-fun c1_2 () Real (- 1.0 (/ tau0_2 tau0_max)))
(define-fun c1_3 () Real (- 1.0 (/ tau0_3 tau0_max)))
(define-fun c1_4 () Real (- 1.0 (/ tau0_4 tau0_max)))
(define-fun c1_5 () Real (- 1.0 (/ tau0_5 tau0_max)))
(define-fun c1_6 () Real (- 1.0 (/ tau0_6 tau0_max)))
(define-fun c1_7 () Real (- 1.0 (/ tau0_7 tau0_max)))
(define-fun c1_8 () Real (- 1.0 (/ tau0_8 tau0_max)))
(define-fun c1_9 () Real (- 1.0 (/ tau0_9 tau0_max)))
(define-fun c1_10 () Real (- 1.0 (/ tau0_10 tau0_max)))
(define-fun c1_11 () Real (- 1.0 (/ tau0_11 tau0_max)))

(define-fun miu_c1 () Real (/ (+ (* c1_0 x0) (* c1_1 x1) (* c1_2 x2) (* c1_3 x3)
                                 (* c1_4 x4) (* c1_5 x5) (* c1_6 x6) (* c1_7 x7)
                                 (* c1_8 x8) (* c1_9 x9) (* c1_10 x10) (* c1_11 x11))
                              12.0))

; 定义各个tau1值
(define-fun tau1_0 () Real (sqr (- x0 miu_c1)))
(define-fun tau1_1 () Real (sqr (- x1 miu_c1)))
(define-fun tau1_2 () Real (sqr (- x2 miu_c1)))
(define-fun tau1_3 () Real (sqr (- x3 miu_c1)))
(define-fun tau1_4 () Real (sqr (- x4 miu_c1)))
(define-fun tau1_5 () Real (sqr (- x5 miu_c1)))
(define-fun tau1_6 () Real (sqr (- x6 miu_c1)))
(define-fun tau1_7 () Real (sqr (- x7 miu_c1)))
(define-fun tau1_8 () Real (sqr (- x8 miu_c1)))
(define-fun tau1_9 () Real (sqr (- x9 miu_c1)))
(define-fun tau1_10 () Real (sqr (- x10 miu_c1)))
(define-fun tau1_11 () Real (sqr (- x11 miu_c1)))

; 声明tau1_max并展开max约束
(declare-fun tau1_max () Real)
(assert (> tau1_max 0))
(assert (>= tau1_max tau1_0))
(assert (>= tau1_max tau1_1))
(assert (>= tau1_max tau1_2))
(assert (>= tau1_max tau1_3))
(assert (>= tau1_max tau1_4))
(assert (>= tau1_max tau1_5))
(assert (>= tau1_max tau1_6))
(assert (>= tau1_max tau1_7))
(assert (>= tau1_max tau1_8))
(assert (>= tau1_max tau1_9))
(assert (>= tau1_max tau1_10))
(assert (>= tau1_max tau1_11))
(assert (or (= tau1_max tau1_0) (= tau1_max tau1_1) (= tau1_max tau1_2)
            (= tau1_max tau1_3) (= tau1_max tau1_4) (= tau1_max tau1_5)
            (= tau1_max tau1_6) (= tau1_max tau1_7) (= tau1_max tau1_8)
            (= tau1_max tau1_9) (= tau1_max tau1_10) (= tau1_max tau1_11)))

; 定义c2对应的值
(define-fun c2_0 () Real (* c1_0 (- 1.0 (/ tau1_0 tau1_max))))

(assert (= c2_0 1.0))

(check-sat)
(get-model)

• 修改后的代码将参数化函数x(Int)拆分为独立的实数变量，避免整数与实数理论混合，进一步降低求解复杂度
• 所有max相关的非线性约束都被展开为线性断言，让求解器更容易处理
• 运行时记得给求解器加上有理数模式的参数：Z3用z3 --rational <file>.smt2，CVC5用cvc5 --rational <file>.smt2

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