2

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

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

你能帮助我吗？

4

1 回答 1

6

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

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

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

相关问题：

于 2013-07-25T14:31:17.273 回答