1

我有几个 SMTLIB2 示例，z3 通常会在 10 毫秒内找到 unsat，但是，当我添加一个请求以生成 unsat 核心时，check-sat 会持续几分钟而不会返回。这种行为是可以预期的吗？请求 unsat 核心是否不仅仅打开检测记录依赖项，并更改 z3 运行的过程和选项？是否可以设置更多选项，以便在使用 unsat 核心生成时看到与不使用时相同的行为？

我在 Scientific Linux 6.3 上使用 Z3 4.3.1（稳定分支）。

这些示例在 AUFNIRA 中，尽管有几个不涉及实数并且可能不是非线性的。

谢谢，

保罗。

4

1 回答 1

5

使用“答案文字”（又名假设）跟踪未饱和核心。当我们启用 unsat 核心提取并使用断言时，例如

(assert  (! (= x 10) :named a1))

Z3 将在内部为 name 创建一个新的布尔变量a1，并断言

(assert  (=> a1 (= x 10)))

调用时check-sat，它假定所有这些辅助变量都为真。也就是说，Z3 试图表明问题是 unsat/sat 以这些假设为模。对于可满足的实例，它将像往常一样以模型终止。对于不可满足的实例，只要生成仅包含这些假定布尔变量的引理，它将终止。引理的形式(or (not a_i1) ... (not a_in))是a_i's 是假定的布尔变量的子集。据我所知，这种技术是由 MiniSAT 求解器引入的。此处对其进行了描述（第 3 节）。我真的很喜欢它，因为它实现起来很简单，而且我们基本上可以免费获得 unsat 核心生成。

然而，这种方法有一些缺点。首先，一些预处理步骤不再适用。如果我们只是断言

(assert (= x 10))

Z3 将替换x为10无处不在。我们说 Z3 正在执行“价值传播”。如果断言的形式为，则不应用此预处理步骤

(assert  (=> a1 (= x 10)))

这只是一个示例，许多其他预处理步骤都会受到影响。在求解期间，一些简化步骤也被禁用。如果我们检查 Z3 源文件smt_context.cpp，我们会发现如下代码：

   void context::simplify_clauses() {
        // Remark: when assumptions are used m_scope_lvl >= m_search_lvl > m_base_lvl. Therefore, no simplification is performed.
        if (m_scope_lvl > m_base_lvl)
            return;
        ...
   }

当使用“答案文字”/假设时，条件m_scope_lvl > m_base_lvl)始终为真。因此，当我们启用 unsat 核心生成时，我们可能会真正影响性能。似乎没有什么是真正免费的:)

于 2013-02-21T19:36:56.237 回答