Z3的ctx-solver-simplify化简不充分，子句顺序为何影响结果？

核心原因 #

ctx-solver-simplify战术的内部化简逻辑是按子句顺序单向遍历，仅检查当前子句是否被之前处理过的子句蕴含，或当前子句是否蕴含后续子句（部分场景），不会全局扫描所有子句的蕴含关系。这种顺序依赖的设计是为了平衡化简效果和性能，避免过度遍历带来的开销。

具体例子解析 #

1. 双不等式析取场景

   • 当子句顺序为(or (> b 1.0) (> b 2.0))时，Z3先处理> b 1.0，后续检查> b 2.0时，发现> b 2.0蕴含> b 1.0，但由于前面的子句已经被处理，战术不会反向合并，因此保留原结构（仅做了语法转换，把>转为(not (<= ...))）。
   • 交换顺序为(or (> b 2.0) (> b 1.0))时，先处理> b 2.0，后续检查> b 1.0时，发现> b 2.0蕴含> b 1.0，直接移除冗余的> b 1.0，得到化简结果(> b 1.0)。

2. 混合布尔变量与不等式场景

   • 当布尔变量a放在开头(or a (> b 2.0) (> b 1.0))时，a与后续不等式无蕴含关系，战术遍历到a后，不会再对后面的两个不等式做合并优化。
   • 把a放在末尾时，前面两个不等式先被处理，战术识别出> b 2.0蕴含> b 1.0，合并为> b 1.0，再与a组成析取，得到(or (> b 1.0) a)。

解决方法 #

1. 手动调整子句顺序
   将更强的约束（能蕴含其他子句的）放在析取式的前面，比如把> b 2.0放在> b 1.0之前，确保战术优先处理强约束，触发冗余子句消除。

2. 结合sort-clauses战术自动排序
   使用then组合战术，先对析取子句按约束强度排序，再执行ctx-solver-simplify，这样无需手动调整顺序：

   (declare-const b Real)
   (assert (or (> b 1.0) (> b 2.0)))
   (apply (then sort-clauses ctx-solver-simplify))
   

   执行后会自动化简为(> b 1.0)，不受原顺序影响。

   对混合布尔变量的场景同样有效：

   (declare-const a Bool)
   (declare-const b Real)
   (assert (or a (> b 2.0) (> b 1.0)))
   (apply (then sort-clauses ctx-solver-simplify))
   

   会得到(or a (> b 1.0))。

3. 调整simplify战术选项
   若不想依赖ctx-solver-simplify，可以尝试使用基础的simplify战术并开启冗余子句消除选项:som true（Set of Monomials）：

   (simplify (or (> b 1.0) (> b 2.0)) :som true)
   

   也能得到(> b 1.0)，但对于复杂公式，ctx-solver-simplify结合排序的效果更稳定。

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