z3 行为根据 unsat 核心请求而改变 [英] z3 behaviour changing on request for unsat core

问题描述

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

I have several SMTLIB2 examples which z3 normally finds unsat in 10s of milliseconds, yet, when I add in a request for it to generate unsat cores, the check-sat keeps going for minutes without returning. Is this behaviour to be expected? Does requesting unsat cores do more than just switch on instrumentation recording dependencies, and change which procedures and options z3 runs with? Is it possible to set further options so I see the same behaviour when I'm using unsat core generation as I see when I'm not using it?

我在 Scientific Linux 6.3 上使用 Z3 4.3.1(稳定分支).

I'm using Z3 4.3.1 (stable branch) on Scientific Linux 6.3.

示例在 AUFNIRA 中，但有几个示例不涉及实数，并且可能不是非线性的.

The examples are in AUFNIRA, though several involve no reals and probably are not non-linear.

谢谢，

保罗.

推荐答案

使用答案文字"(又名假设)跟踪未满足的核心.当我们启用 unsat 核心提取并使用诸如

The unsat cores are tracked using "answer literals" (aka assumptions). When we enable unsat core extraction and use assertions such as

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

Z3 将在内部为名称 a1 创建一个新的布尔变量，并声明

Z3 will internally create a fresh Boolean variable for the name a1, and assert

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

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

When, check-sat is invoked, it assumes all these auxiliary variables are true. That is, Z3 tries to show the problem is unsat/sat modulo these assumptions. For satisfiable instances, it will terminate as usual with a model. For unsatisfiable instances, it will terminate whenever it generates a lemma that contains only these assumed Boolean variables. The lemma is of the form (or (not a_i1) ... (not a_in)) where the a_i's are a subset of the assumed Boolean variables. As far as I know, this technique has been introduced by the MiniSAT solver. It is described here (Section 3). I really like it because it is simple to implement and we essentially get unsat core generation for free.

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

However, this approach has some disadvantages. First, some preprocessing steps are not applicable anymore. If we just assert

(assert (= x 10))

Z3 将在任何地方用 10 替换 x.我们说 Z3 正在执行价值传播".如果断言的形式为

Z3 will replace x with 10 everywhere. We say Z3 is performing "value propagation". This preprocessing step is not applied if the assertion is of the form

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

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

This is just an example, many other preprocessing steps are affected. During solving time, some of the simplification steps are also disabled. If we inspect the Z3 source file smt_context.cpp we will find code such as:

   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 核心生成时，我们可能会真正影响性能.似乎没有什么是真正免费的:)

The condition m_scope_lvl > m_base_lvl) is always true when "answer literals"/assumptions are used. So, when we enable unsat core generation, we may really impact the performance. It seems that nothing is really for free :)

这篇关于z3 行为根据 unsat 核心请求而改变的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！