得到一个“好"未饱和核心与 z3(逻辑 QF_BV) [英] Getting a "good" unsat-core with z3 (logic QF_BV)

问题描述

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

I am using the Z3 SMT solver to solve a problem that I have expressed in the logic QF_BV, using the SMTLIB 2 language.

该模型无法满足，我正试图让求解器产生一个 unsat-core.

The model is unsatisfiable, and I am trying to get the solver to produce an unsat-core.

我的模型包含几个强制"约束，我使用 assert 语句指定这些约束.

My model consists of several 'mandatory' constraints, which I specify using assert statements.

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

The assertions that I want to be considered for unsat-core generation, have been specified using the (assert (! (EXPR) :named NAME)) construct.

Z3 给了我一个 unsat.然而，Z3 似乎总是转储一个由所有命名断言组成的微不足道"未饱和核心.

Z3 gives me an unsat, as expected. However, Z3 always seems to dump a 'trivial' unsat-core consisting of ALL the named assertions.

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

I know that there exists a subset of my named assertions, which is an unsat-core. I found this core using Yices SMT solver, which frequently gives me relatively smaller unsat-cores. The Yices model is the same as the Z3 model (pretty much a line-by-line translation from SMT2 to the Yices input language).

生成好"的 unsat-cores 是求解器特定的功能，还是我可以提出任何通用建议/更改来帮助 Z3 为我提供更好的内核?

Is producing "good" unsat-cores a solver-specific feature, or are there any generic suggestions/changes I could make to help Z3 give me a better core?

推荐答案

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

Z3 and Yices 1.x use the same approach for computing unsat cores. The track all assertions that were used in the proof of unsatisfiability. However, the proofs built by each system may be quite different. There are algorithms for computing minimal unsat cores on top of the capabilities provided by Z3 and Yices. Here is a reference.

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

by default, Z3 uses several pre-processing steps before it tries to solve a problem. Some of these steps may affect the generation of the unsat core. In particular, it eliminates constants using the equations in the problem. We say Z3 "solves" the equations and eliminate the variables. In your script, you can get a smaller core by disabling this step. We can accomplish that by using the option

(set-option :auto-config false)

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

Z3 will execute a very general configuration. For bit-vector problems it is usually a good idea to disable "relevacy propagation":

(set-option :relevancy 0)

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

Finally, we can now enable/disable the variable elimination step, and see the effect on the unsat core size.

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

这篇关于得到一个“好"未饱和核心与 z3(逻辑 QF_BV)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！