5

对 SMT 求解器进行新的研究多次受到以下事实的阻碍：可用问题需要大量与决策过程没有直接关系的技巧和预处理技术。这些通常未发布或需要时间来正确实施和优化，此外还使得对不同求解器的比较和理解非常困难。

是否可以使用 Z3 作为预处理器来处理问题并将其以预处理形式（z3 本身用于解决问题的形式）转储出来？

我没有看到任何命令行选项，但我猜测可能有某种方法可以通过策略、通过 python 接口甚至编写一些额外的代码来实现这一点。

4

1 回答 1

4

是的，Z3 可以用作预处理器。该命令apply允许用户应用策略并将其转储为 SMT 2.0 基准。这是一个示例（也可在http://rise4fun.com/Z3/eutO在线获得）：

(declare-const x Real)
(declare-const y Real)

(assert (forall ((n Real)) (or (< x n) (< n y))))
(assert (= (< x y) (< x 100.0)))

(apply (then qe nnf) :print false :print-benchmark true)

在上面的示例中，qe（量词消除）和 nnf（否定-范式）策略应用于输入问题。

一些额外的点：

  • 几种策略只能产生令人满意的结果。因此，结果基准的模型不一定是原始公式的模型。我们可以要求 Z3 转储相关的“模型转换器”（选项:print-model-converter true）。模型转换器对 Z3 用于将结果公式的模型转换为原始公式的模型的步骤进行编码。但是，没有打印模型转换器的标准，Z3 无法阅读这些描述。当然，我们可以使用编程 API 将所有内容粘合在一起。

  • 一小部分策略会产生低于（只有饱和结果可以信任）或高于（只有未饱和结果可以信任）的近似值。它们通常用于模型或证明查找。当 Z3 显示结果目标时，它会告知结果是精确的（sat 和 unsat 可以信任）。

于 2012-12-04T18:50:01.353 回答