我正在使用 Z3 SMT 求解器来解决我用 SMTLIB 2 语言在逻辑 QF_BV 中表达的问题。
模型无法满足，我正在尝试让求解器生成 unsat-core。
我的模型包含几个“强制性”约束，我使用 assert 语句指定。
已使用(assert (! (EXPR) :named NAME)) 构造指定了我要考虑用于生成 unsat-core 的断言。
正如预期的那样，Z3 给了我一个unsat。然而，Z3 似乎总是转储一个由所有命名断言组成的“微不足道”的 unsat-core。
我知道存在我的命名断言的一个子集，它是一个 unsat-core。我使用 Yices SMT 求解器找到了这个核心，它经常给我相对较小的未饱和核心。 Yices 模型与 Z3 模型相同（几乎是从 SMT2 到 Yices 输入语言的逐行翻译）。
产生“好”的 unsat-cores 是求解器特有的功能，还是我可以做出任何通用的建议/更改来帮助 Z3 给我一个更好的内核？
【问题讨论】：
标签： z3
Z3 和 Yices 1.x 使用相同的方法来计算未饱和内核。跟踪用于证明不可满足性的所有断言。但是，每个系统构建的证明可能完全不同。在 Z3 和 Yices 提供的功能之上，还有用于计算最小未饱和核心的算法。这是reference。
编辑：默认情况下，Z3 在尝试解决问题之前会使用几个预处理步骤。其中一些步骤可能会影响未饱和核心的生成。特别是，它使用问题中的方程消除了常数。我们说 Z3 “解决”了方程并消除了变量。在您的script 中，您可以通过禁用此步骤来获得更小的内核。我们可以通过使用选项来实现这一点
(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
【讨论】：
#s。