如何解释统计数据 Z3 [英] How to interpret statistics Z3

问题描述

我在 Z3 中得到以下统计数据.

I get the following statistics in Z3.

(:added-eqs            24529
 :binary-propagations  43837
 :bv-bit2core          7115
 :bv-conflicts         156
 :bv-diseqs            10395
 :bv-dynamic-diseqs    10028
 :bv->core-eq          10401
 :conflicts            409
 :decisions            4840
 :del-clause           84926
 :final-checks         2
 :max-generation       4
 :memory               5.69
 :minimized-lits       467
 :mk-clause            88358
 :propagations         90195
 :quant-instantiations 3388
 :restarts             3
 :time                 0.83)

我想知道每个结果行使用的指标是什么.

I'd like to know what the metrics used for each result row.

你能帮我吗?

推荐答案

免责声明:我觉得以正确的方式解释统计数据是一门艺术，而 Z3 开发人员可能是唯一真正知道如何进行去做.无论如何，这就是我所知道的……或相信:

Disclaimer: I have the feeling that interpreting the statistics the right way is quite an art, and that the Z3 developers are probably the only ones who really know how to do that. Anyway, here is what I know ... or believe:

quant-instantiations 表示实例化的量词的数量.实例化越少越好，但您当然不想让您的模式/触发器过于严格，因为这样 Z3 将无法证明任何事情.

quant-instantiations indicates the number of instantiated quantifiers. The fewer instantiations the better, but you of course don't want to make your patterns/triggers too strict because Z3 then won't be able to prove anything.

conflicts 表示在理论子求解器中发生的分配，并且没有使公式成立.如果公式可以满足且冲突次数较多，基本上意味着证明者尝试了很多不满足公式的赋值，即证明者没有设法在目标方向上探索搜索空间.

conflicts indicate assignments that happen in the theory subsolvers and that did not make the formula true. If the formula can be satisfied and the number of conflicts is high, it basically means that the prover tried lots of assignments that did not satisfy the formula, i.e., that the prover did not manage to explore the search space in the direction of the goal.

相关问题:

• Z3 统计:时间衡量什么?
• Z3 实数算术和统计
• 哪些统计数据表明 Z3 有效运行?

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