Z3实数算术统计 [英] Z3 real arithmetic and statistics

问题描述

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

Given a problem that is encoded using Z3's reals, which of the statistics that Z3 /smt2 /st produces might be helpful in order to judge if the reals engine "has problems/does lots of work"?

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

In my case, I have two mostly equivalent encodings of the problem, both using reals. The "small" difference in the encoding, however, makes a big difference in runtime, namely, that encoding A takes 2:30min and encoding B 13min. The Z3 statistics show that conflicts and quant-instantiations are mostly equivalent, but others are not, for example grobner, pivots and nonlinear-horner.

这两种不同的统计数据可作为 gist 提供.

The two different statistics are available as a gist.

编辑(针对 Leo 的评论):

EDIT (to address Leo's comment):

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

The SMT2-encoding generated by both versions is ~30k lines and the assertions where reals are used are sprinkled all over the code. The main difference is that encoding B uses lots of underspecified real-typed constants from the range 0.0 to 1.0 that are bounded by inequalities, e.g. 0.0 < r1 < 1.0 or 0.0 < r3 < 0.75 - r1 - r2, whereas in encoding A lots of these underspecified constants have been replaced with fixed real values from the same range, e.g., 0.1 or 0.75 - 0.01. Both encodings use non-linear real arithmetic, e.g. r1 * (1.0 - r2).

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

A few random examples from the two encodings are available as a gist. All occurring variables are underspecified reals as described above.

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

PS: Does introducing aliases for fixed real values, e.g.,

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

造成重大的绩效损失?

推荐答案

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

The new nonlinear arithmetic solver is only used on problems that contain only arithmetic. Since your problem uses quantifiers, the new nonlinear solver will not be used. Thus, Z3 will use the old approach based on a combination of: Simplex (pivots stat), Groebner Basis (groebner stat), and Interval Propagation (horner stat). This is not a complete method. Moreover, based on the fragments you posted in gist, Groebner basis will not be very effective. This method is usually effective on problems that contain a lot of equalities. So, it is probably just overhead. You can disable it by using option NL_ARITH_GB=false. Of course, this is just a guess based on the problem fragment you posted.

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

The differences between encoding A and B are substantial. Encoding A is essentially a linear problem, since several constants were fixed to real values. Z3 was always complete for linear arithmetic problems. So, this should explain the difference in performance.

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

Regarding your question about aliases, the preferred way to introduce aliases is:

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

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

Z3 also contains a preprocessor that eliminates variables using linear equations. This preprocessor is disabled by default in problems that contain quantifiers. This design decision is motivated by program verification tools that make extensive use of triggers/patterns in quantifiers. The variable elimination process may modify the careful designed triggers/patterns, and affect the total run-time. You can use the new tactic/strategy framework in Z3 to force it to apply this preprocessor. You can replace the command

(check-sat)

与

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

此策略是告诉 Z3 执行简化程序，然后求解方程(并消除变量)，然后执行默认求解器引擎 smt.您可以在以下教程中找到有关战术和策略的更多信息.

This strategy is telling Z3 to execute the simplifier, then solve equations (and eliminate variables) and then execute the default solver engine smt. You can find more about tactics and strategies in the following tutorial.

这篇关于Z3实数算术统计的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！