z3 - 使用 z3 获得 "good"unsat-core(逻辑 QF_BV)

Question

我正在使用 Z3 SMT 求解器解决我在逻辑 QF_BV 中表达的问题，使用 SMTLIB 2 语言。

该模型是不可满足的，我试图让求解器产生一个不满足的核心。

我的模型包含几个“强制”约束，我使用 assert 指定这些约束。声明。

我想考虑生成 unsat-core 的断言，已使用 (assert (! (EXPR) :named NAME)) 指定。构造。

Z3 给了我一个 unsat ，正如预期的那样。但是，Z3 似乎总是转储由所有命名断言组成的“微不足道”未满足核心。

我知道存在我命名的断言的一个子集，它是一个 unsat-core。我使用 Yices SMT 求解器找到了这个核心，它经常给我相对较小的未饱和核心。 Yices 模型与 Z3 模型相同(几乎是从 SMT2 到 Yices 输入语言的逐行翻译)。

生产“好”的未饱和核心是求解器特定的功能，还是我可以提出任何通用建议/更改来帮助 Z3 为我提供更好的核心？

Answer 1

Z3 和 Yices 1.x 使用相同的方法来计算 unsat 核心。跟踪用于证明不可满足性的所有断言。但是，每个系统构建的证明可能大不相同。在 Z3 和 Yices 提供的功能之上，有一些算法可以计算最小未饱和内核。这是一个 reference .

编辑:默认情况下，Z3 在尝试解决问题之前使用几个预处理步骤。其中一些步骤可能会影响未饱和核心的生成。特别是，它使用问题中的方程来消除常数。我们说 Z3 “求解”了方程并消除了变量。在您的 script ，您可以通过禁用此步骤来获得更小的内核。我们可以通过使用选项来实现

(set-option :auto-config false)

Z3 将执行一个非常通用的配置。对于位向量问题，禁用“相关性传播”通常是个好主意:

(set-option :relevancy 0)

最后，我们现在可以启用/禁用变量消除步骤，并查看对 unsat 核心大小的影响。

(set-option :solver true) ;; Z3 will generate the core C0 C1 C2
(set-option :solver false) ;; Z3 will generate the core C1 C2