我正在使用Z3 SMT求解器来解决我在逻辑QF_BV中使用SMTLIB 2语言表达的问题.
该模型是不可满足的,我试图让求解器产生一个不满足的核心.
我的模型由几个"强制"约束组成,我使用assert语句指定.
我想要使用(assert (! (EXPR) :named NAME))构造来指定我想要用于不良核心生成的断言.
unsat正如预期的那样,Z3给了我一个.然而,Z3似乎总是抛弃一个由所有命名的断言组成的"琐碎的"不饱和核心.
我知道我的命名断言中存在一个子集,这是一个不可靠的核心.我使用Yices SMT求解器找到了这个核心,它经常给我相对较小的不饱和核心.Yices模型与Z3模型相同(几乎是从SMT2到Yices输入语言的逐行转换).
产生"好"的不良核心是解决者特有的功能,还是我可以做出任何通用的建议/改变来帮助Z3给我一个更好的核心？
Z3和Yices 1.x使用相同的方法计算不良核心.跟踪所有用于证明不可满足性的断言.但是,每个系统构建的证明可能完全不同.有一些算法可以在Z3和Yices提供的功能之上计算最小不饱和核心.这是一个参考.
编辑:默认情况下,Z3在尝试解决问题之前使用了几个预处理步骤.这些步骤中的一些可能影响不饱和核的产生.特别是,它使用问题中的方程式消除常数.我们说Z3"解决"方程并消除变量.在脚本中,您可以通过禁用此步骤来获得更小的核心.我们可以通过使用该选项来实现
(set-option :auto-config false)
Z3将执行非常通用的配置.对于位向量问题,禁用"相关传播"通常是个好主意:
(set-option :relevancy 0)
最后,我们现在可以启用/禁用变量消除步骤,并查看对不良核心大小的影响.
(set-option :solver true) ;; Z3 will generate the core C0 C1 C2
(set-option :solver false) ;; Z3 will generate the core C1 C2