我正在使用 Z3 SMT 求解器来解决我在逻辑 QF_BV 中使用 SMTLIB 2 语言表达的问题。
该模型无法满足，我试图让求解器产生一个 unsat-core。
我的模型由几个“强制性”约束组成，我使用assert语句指定它们。
我想要考虑用于 unsat-core 生成的断言已使用(assert (! (EXPR) :named NAME))构造指定。
unsat正如预期的那样，Z3 给了我一个。然而，Z3 似乎总是转储一个由所有命名断言组成的“微不足道”的 unsat-core。
我知道存在我的命名断言的一个子集，它是一个 unsat-core。我使用 Yices SMT 求解器找到了这个核心，它经常给我相对较小的未饱和核心。Yices 模型与 Z3 模型相同（几乎是从 SMT2 到 Yices 输入语言的逐行翻译）。
产生“好”的 unsat 核心是求解器特有的功能，还是我可以做出任何通用的建议/更改来帮助 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