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