Z3 实数算术和统计

Question

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

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

两种不同的统计数据可作为gist 使用。

编辑（以解决 Leo 的评论）：

两个版本生成的 SMT2 编码约为 30k 行，并且使用实数的断言散布在整个代码中。的主要区别在于编码乙使用大量尚未得以实时类型的常量从范围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).

来自两种编码的一些随机示例可作为要点。如上所述，所有出现的变量都是未指定的实数。

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 基础不会很有效。这种方法通常对包含很多等式的问题有效。所以，这可能只是开销。您可以使用 option 禁用它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。您可以在以下教程中找到有关战术和策略的更多信息。