z3 - 如何解释统计数据 Z3

Question

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

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

你能帮帮我吗？

Answer 1

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

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

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

相关问题:

• Z3 statistics: what does time measure?
• Z3 real arithmetic and statistics
• Which statistics indicate an efficient run of Z3?