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

问题描述

鉴于使用Z3's reals编码的问题，哪些统计信息 Z3 / smt2 / st 产生可能有助于判断reals引擎是否具有问题/做很多工作？

在我的情况下，我有两个主要是等价的问题编码，都使用reals。然而，编码中的小差异在运行时产生了很大的不同，即编码A需要2：30分钟并编码B 13分钟。 Z3统计数据显示，冲突和量化实例化大部分是等效的，但其他的则不是，例如 grobner ， pivotots 和 nonlinear-horner 。

这两种不同的统计信息可以作为 gist 。

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

由两个版本生成的SMT2编码是〜30k行，并且使用reals的断言在代码中遍布。主要的区别在于编码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）
 
（assert（= $ Perms.Zero 0.0））
（assert（= $ Perms.Write 1.0））
 
解决方案
新的非线性算术求解器仅用于仅包含算术的问题。由于您的问题使用量词，所以不会使用新的非线性求解器。因此，Z3将使用基于以下组合的旧方法：Simplex（pivotots stat），Groebner Basis（groebner Basis）和间隔传播（horner stat）。这不是一个完整的方法。 
此外，根据您发布的片段，Groebner的基础不会很有效。这种方法通常对包含大量均等性的问题有效。 
所以，这可能只是开销。您可以使用选项 NL_ARITH_GB = false 禁用它。 
当然，这只是一个基于你发布的问题片段的猜测。
 
 
 
编码 A 和 B 是实质的。编码 A 本质上是一个线性问题，因为几个常量被固定为实际值。 Z3对于线性算术问题始终是完整的。因此，这应该解释性能差异。
 
 
 
关于别名的问题，引入别名的首选方法是：
 
 
 $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ code> 

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

 （check-sat）
  

与

 （check-sat-using（then simplices-eqs smt））
  

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

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"?

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.

The two different statistics are available as a gist.

EDIT (to address Leo's comment):

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).

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

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))

inflict significant performance penalties?

解决方案

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.

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 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)

with

(check-sat-using (then simplify solve-eqs 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屋！