如何配置Z3避免分支以高效证明非负项和的不等式系统？

问题背景 #

给定含N个未解释类型变量a₁..aN的N个不等式系统，每个式子可通过合并同类项重组为非负求和项，且每个不等式包含恒真的自反等式项（如a₁==a₁），理论上无需分支变量相等性即可判定恒成立。但直接用ITE表达式编码后，Z3随N增大耗时呈指数增长，trace显示大量[push][pop]分支操作。

解决方案 #

1. 手动简化表达式，彻底消除冗余ITE分支 #

原不等式系统可通过代数合并直接简化：

• 第k个不等式的原始形式为：
  sum_{i=1}^N (a_k==a_i ? 1 : 0) + sum_{i=1}^{k-1} (a_k==a_i ? -1 : 0) >= 1
• 合并同类项后，所有i<k的a_k==a_i项抵消为0，剩余部分为sum_{i=k}^N (a_k==a_i ?1:0) >=1
• 由于a_k==a_k恒真，这部分的取值为1，因此左边至少为1，不等式恒成立。

基于此，可直接将每个不等式简化为恒真断言，或保留必要的非冗余项，完全消除会触发分支的ITE表达式。

简化后的N=3示例代码

(set-option :auto_config false)
(declare-sort Address 0)
(declare-fun a1 () Address)
(declare-fun a2 () Address)
(declare-fun a3 () Address)
(assert
   (not
      (and
         (<= 1.0 (+ 1.0 (ite (= a1 a2) 1.0 0.0) (ite (= a1 a3) 1.0 0.0)))
         (<= 1.0 (+ 1.0 (ite (= a2 a3) 1.0 0.0)))
         (<= 1.0 1.0)
      )
   )
)
(check-sat)

该版本中Z3无需处理任何分支，可瞬间返回unsat。

2. 调整Z3配置，抑制不必要的分支策略 #

配合表达式简化，可通过以下配置进一步减少分支：

• 禁用模型基于的量词实例化：(set-option :smt.mbqi false)，避免量词相关的分支探索（若通用问题中的量词已提前处理）
• 强制算术表达式左移简化：(set-option :simplify.arith_lhs true)，让Z3自动合并同类项
• 启用ITE提取简化：(set-option :simplify.extract_ite true)，辅助Z3识别并消除冗余ITE项
• 关闭自动配置后手动设置求解器模式：避免Z3启用可能带来分支的默认策略

3. 利用等式自反性直接断言恒真条件 #

对于已明确恒成立的不等式，直接用true替代复杂表达式，例如第k个不等式可直接写为true，彻底跳过求解器对该式的分支处理。

总结 #

核心优化思路是先手动完成表达式的代数简化，消除所有冗余的ITE分支点，再配合Z3的简化配置，从根源上避免指数级的分支探索。对于含复杂算术或量词的通用问题，优先重组为非负项并合并同类项，将恒真部分直接替换为true，可大幅降低求解耗时。

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