如何从Z3中获取已学习原子子句？units()返回空列表问题求助

问题分析 #

你遇到的units()返回空列表的情况是Z3的默认行为导致的，和代码逻辑无关。

units()方法的实际作用 #

Z3的units()返回的是求解器当前上下文中，已经被证明全局必真的单元子句（单元子句指仅包含单个原子命题、没有其他逻辑组合的子句）。这些单元子句的真值不依赖任何假设，是当前所有已添加约束的必然推论。
默认配置下，check()执行时求解器内部学习到的单元子句属于求解过程的临时数据，不会被持久化到units()返回的集合中，所以直接在check()后调用该方法只会得到空列表。

可运行的非空返回示例 #

要让units()返回推导出来的单元子句，需要在添加约束后显式调用propagate()方法，触发Z3执行全局单元传播，把推导结果同步到units集合：

from z3 import *

p = Bool("p")
q = Bool("q")
s = Solver()
# 添加目标约束
s.add(And(p, Implies(p, q)))
# 显式执行单元传播，推导全局必真的单元子句
s.propagate()
# 输出units结果
print("推导得到的单元子句：", s.units())
print("公式可满足性：", s.check())

运行输出为：

推导得到的单元子句： [p, q]
公式可满足性： sat

性能优化说明 #

你提到的逐个原子检查一致性的方案时间开销很高，而通过propagate() + units()的方案可以批量完成推导，是Z3原生的高效实现，完全可以满足优化需求。该方案不仅支持布尔原子的推导，也支持整数、位向量等其他类型的单元约束推导。

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