1

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

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

这两种不同的统计数据可作为要点提供。


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

两个版本生成的 SMT2 编码约为 30k 行，使用实数的断言遍布整个代码。主要区别在于编码 B 使用了从范围0.0到1.0由不等式限制的大量未指定的实类型常量，例如0.0 < r1 < 1.0or 0.0 < r3 < 0.75 - r1 - r2，而在编码 A 中，许多这些未指定的常量已被同一范围内的固定实数值替换，例如,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))

造成重大的绩效处罚？

4

1 回答 1

5

新的非线性算术求解器仅用于仅包含算术的问题。由于您的问题使用量词，因此不会使用新的非线性求解器。因此，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。您可以在以下教程中找到更多关于战术和策略的信息。

于 2012-06-11T15:09:10.780 回答