Z3 实数算术与统计

Question

给定一个使用 Z3 的实数编码的问题，Z3 /smt2 /st 产生的哪些统计数据可能有助于判断实数引擎是否“有问题/做了很多工作”？

在我的例子中，我有两个基本等效的问题编码，都使用实数。然而，编码的“小”差异在运行时产生了很大的差异，即编码 A 需要 2:30 分钟，编码 B 需要 13 分钟。 Z3 统计显示conflicts 和quant-instantiations 大部分是等价的，但其他不是，例如grobner、pivots 和nonlinear-horner。

这两种不同的统计数据以gist 的形式提供。

编辑（针对 Leo 的评论）：

两个版本生成的 SMT2 编码约为 30k 行，并且使用实数的断言遍布整个代码。主要区别在于编码 B 使用了从0.0 到1.0 范围内的大量未指定的实类型常量，这些常量受到不等式的限制，例如0.0 < r1 < 1.0 或 0.0 < r3 < 0.75 - r1 - r2，而在编码中，许多这些未指定的常量已被同一范围内的固定实数值替换，例如 0.1 或 0.75 - 0.01。两种编码都使用非线性实数算术，例如r1 * (1.0 - r2).

两种编码中的一些随机示例可用作gist。如上所述，所有出现的变量都是未指定的实数。

PS：是否为固定实数值引入别名，例如，

(define-sort $Perms () Real)
(declare-const $Perms.$Full $Perms)
(declare-const $Perms.$None $Perms)
(assert (= $Perms.Zero 0.0))
(assert (= $Perms.Write 1.0))

造成严重的性能损失？

Answer 1

新的非线性算术求解器仅用于仅包含算术的问题。由于您的问题使用量词，因此不会使用新的非线性求解器。因此，Z3 将使用基于以下组合的旧方法：Simplex (pivots stat)、Groebner Basis (groebner stat) 和 Interval Propagation (horner stat)。这不是一个完整的方法。 此外，根据您在 gist 中发布的片段，Groebner 基础不会很有效。这种方法通常对包含大量等式的问题有效。 所以，它可能只是开销。您可以使用选项NL_ARITH_GB=false 禁用它。 当然，这只是根据您发布的问题片段的猜测。

编码A 和B 之间的差异很大。编码A 本质上是一个线性问题，因为有几个常数被固定为实数值。 Z3 对于线性算术问题总是完整的。所以，这应该可以解释性能上的差异。

关于您关于别名的问题，引入别名的首选方式是：

(define-const $Perms.$Zero $Perms 0.0)
(define-const $Perms.$Write $Perms 1.0)

Z3 还包含一个使用线性方程消除变量的预处理器。 默认情况下，在包含量词的问题中禁用此预处理器。这种设计决策是由在量词中广泛使用触发器/模式的程序验证工具推动的。变量消除过程可能会修改精心设计的触发器/模式，并影响总运行时间。您可以使用 Z3 中的新战术/策略框架来强制它应用此预处理器。你可以替换命令

(check-sat)

与

(check-sat-using (then simplify solve-eqs smt))

此策略告诉 Z3 执行简化器，然后求解方程（并消除变量），然后执行默认求解器引擎 smt。 您可以在以下tutorial找到更多关于战术和策略的信息。