1 z3
我有几个 SMTLIB2 示例，z3 通常在 10 毫秒内发现 unsat，但是，当我添加请求以生成 unsat 核心时，check-sat 会持续运行几分钟而不返回。这种行为是预期的吗？请求 unsat 核心是否不仅仅是打开仪器记录依赖项，并更改 z3 运行的程序和选项？是否可以设置更多选项，以便在使用 unsat 核心生成时看到的行为与不使用时看到的行为相同？
我在 Scientific Linux 6.3 上使用 Z3 4.3.1（稳定分支）。
这些例子在 AUFNIRA 中，尽管有几个不涉及实数并且可能不是非线性的。
谢谢，
保罗。
使用“答案文字”（又名假设）跟踪未饱和核心。当我们启用 unsat 核心提取并使用断言时，例如
(assert (! (= x 10) :named a1))
Z3 将在内部为 name 创建一个新的布尔变量a1，并断言
(assert (=> a1 (= x 10)))
当,check-sat被调用时，它假定所有这些辅助变量都为真。也就是说，Z3 试图表明问题是 unsat/sat modulo 这些假设。对于可满足的实例，它将像往常一样以模型终止。对于不可满足的实例，只要它生成一个只包含这些假定布尔变量的引理，它就会终止。引理的形式(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，我们会发现如下代码：
(assert (! (= x 10) :named a1))
m_scope_lvl > m_base_lvl)当使用“答案文字”/假设时，条件始终为真。因此，当我们启用 unsat 核心生成时，我们可能会真正影响性能。似乎没有什么是真正免费的:)