使用z3（逻辑QF_BV）获得“良好”不饱和核心

Question

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

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

我的模型由几个'强制性'约束组成，我使用assert语句指定。

我希望用于不饱和核心生成的断言已使用(assert (! (EXPR) :named NAME))构造指定。如预期的那样，Z3给我unsat。然而，Z3似乎总是倾倒一个由所有命名断言组成的“微不足道”的不足核心。

我知道存在我命名断言的一个子集，它是一个不可核心的。我发现这个核心使用Yices SMT解算器，它经常给我相对较小的不饱和核心。 Yices模型与Z3模型相同（几乎是从SMT2到Yices输入语言的逐行翻译）。

正在生产“良好”不饱和核心的解算器特定功能，还是有任何通用的建议/更改，我可以帮助Z3给我一个更好的核心？

Answer 1

Z3和Yices 1.x使用相同的方法计算不饱和核。跟踪所有用于证明不可满足性的论断。但是，每个系统建立的证明可能完全不同。除Z3和Yices提供的功能之外，还有用于计算最小不饱和内核的算法。这是一个reference。

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

(set-option :auto-config false) 

Z3将执行非常一般的配置。对于位向量问题，它通常是一个好主意，禁用“relevacy传播”：

(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