python - Z3 可以用来预处理问题吗？

Question

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

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

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

Answer 1

是的，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 将所有内容粘合在一起。

• 一小部分策略会产生低于(只有 sat 结果可信)或高于(只有 unsat 结果可信)的近似值。它们通常用于模型或证明查找。 Z3在显示结果目标时，会提示结果是精确的(sat和unsat可信)。