3

SMTLib2 ディレクティブ(get-info all-statistics)は、いくつかの数字を表示します。

num. conflicts:     4
num. propagations:  0 (binary: 0)
num. qa. inst:      23

さまざまな公理化とエンコーディングをテストするために、ある Z3 の実行が別の Z3 の実行よりも優れている/効率的であると宣言するのに適切な数値を知りたいです。

名前から推測するとnum. qa. inst、量指定子のインスタンス化の数は良い指標 (低いほど良い) ですが、他のものはどうでしょうか?

4

1 に答える 1

6

量指定子のインスタンス化の数は、公理化が生成するインスタンスが多すぎるかどうかを確認するための良い尺度です。QI_PROFILE=true を使用することもできます。各量指定子の統計が生成されます。属性 :qid を使用して量指定子に名前を付けることができます。DEFAULT_QID=true を使用することもでき、Z3 は行番号に基づいて名前を生成します。QI_PROFILE_FREQ= は、インスタンスが生成されるたびに統計を表示します。これらのオプションは、インスタンス化のループを検出するのに役立ちます。

「num. conflicts」は、Z3 が横断する検索空間のサイズを見積もるのに役立ちます。検索空間のサイズが小さい場合、公理化は「より良い」と言えます。

乾杯、レオ

于 2011-07-27T15:57:14.433 に答える