如何在z3py中实现公共子表达式消除？

你观察到的现象是对的：Z3的默认转换流程（比如simplify+bit-blast+tseitin-cnf）不会自动对全局范围内的公共子表达式做消除，导致重复的子结构被多次展开成CNF子句。要实现公共子表达式消除（CSE），可以通过两种方式解决：

方法1：手动提取公共子表达式 #

最直接的方式是手动将重复出现的子表达式赋值给一个新变量，然后在原公式中用这个变量替代所有对应位置。这样Tseitin转换时会将这个公共子表达式只编码一次。

修改后的代码示例：

from z3 import *

a, b, c, d, e = Bools('a b c d e')
bc = And(b, c)  # 提取公共子表达式

solver = Solver()
# 用bc替代所有And(b,c)的位置
solver.add(Xor(Xor(And(a, bc), And(d, bc)), And(e, bc)))

goal = Goal()
goal.add(solver.assertions())
t = Then('simplify', 'bit-blast', 'tseitin-cnf')

cnf = t(goal)[0]
print(cnf)

运行后输出会看到And(b,c)对应的子句只生成一次，所有引用都指向同一个中间变量，避免了重复编码。

方法2：使用Z3简化器的CSE选项 #

Z3的simplify策略支持通过elim_common_subexpr参数启用公共子表达式消除，在简化阶段就合并重复的子结构。你可以调整策略链，先启用CSE的简化，再进行后续转换：

from z3 import *

a, b, c, d, e = Bools('a b c d e')

solver = Solver()
solver.add(Xor(Xor(And(a, And(b, c)), And(d, And(b, c))), And(e, And(b, c))))

goal = Goal()
goal.add(solver.assertions())
# 在simplify阶段启用公共子表达式消除
t = Then(Simplify(elim_common_subexpr=True), 'bit-blast', 'tseitin-cnf')

cnf = t(goal)[0]
print(cnf)

这种方式不需要手动修改原公式，由Z3自动识别并合并全局公共子表达式，同样能减少重复的CNF子句。

需要注意的是，Z3的CSE并非在所有场景下都会自动触发，尤其是当子表达式被嵌套在复杂结构中时，手动提取的方式更可靠。

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