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 に答える