2

いくつかの研究問題を解決するために、Z3 と Yices と一緒に 1 年足らず働いています。これらのソルバーを使用して、常にパフォーマンスを評価する必要があります。特に、モデリング/チェックに必要な時間とスペース (メモリ) (充足可能性) の 2 つです。Z3の場合、それらを直接見つける手がかりは見つかりませんでした。「統計」(Z3 NET API が提供する関数「DisplayStatistics」を使用) を試してみたところ、(例) 以下に示すような出力が見つかりました。

番号。競合: 122

番号。決定: 2245

番号。伝播: 27884 (バイナリ: 21129)

番号。再起動: 1

番号。最終チェック: 1

番号。分。点灯: 52

番号。追加された式: 3766

番号。mk ブール変数: 2782

番号。デル ブール変数: 658

番号。mk エノード: 1723

番号。削除ノード: 78

番号。mk 句: 3622

番号。デル節: 1517

番号。mk bin 節: 3067

番号。mk 点灯: 18935

番号。ta 競合: 28

番号。行を追加: 5091

番号。ピボット: 328

番号。下をアサート: 2597

番号。アサートアッパー：3416

番号。Diseq をアサート: 1353

番号。バインドされた小道具: 787

番号。固定式: 697

番号。オフセット式: 866

番号。疑似nl.: 34

番号。式 アダプター: 820

これらの値を解釈して、使用されたメモリ/時間を理解する方法がわかりません。実行時間を見つける方法がいくつかあります (Stopwatch などのタイマー クラスを使用)。しかし、スペースが必要な場合は、方法が見つかりませんでした。モデリングに必要なブール変数 (低レベル、SAT ソルバー) の数を取得できれば、非常にうまく機能します。

誰かが私に解決策を示すことができれば、それは素晴らしいことです。

4

1 に答える 1

2

Z3のどのバージョンを使用していますか? 最新バージョン (Z3 3.2) には、メモリ消費統計が含まれています。として表示されmax. heap sizeます。そうは言っても、Z3 のパフォーマンスを評価する最良の方法は、 を使用することz3.exeです。Z3 実行可能ファイルは、時間とメモリ消費を報告します。さらに、一部のパフォーマンスの改善は、API ではまだ利用できません。

いくつかのアプリケーションでは、テキスト インターフェイスが理想的なオプションです。つまり、アプリケーションはパイプ経由で SMT 2.0 コマンドを使用して Z3 プロセスと通信します。主な利点は次のとおりです。さまざまなSMTソルバーを使用して比較するのは非常に簡単です。Z3 を強制終了して再起動するのは簡単です。いくつかの異なるプロセスを作成できます。Z3 が停止しても、アプリケーションは停止しません。もちろん、このソリューションは、何千もの簡単なクエリを実行するアプリケーションや、Z3 との緊密な統合を必要とするアプリケーション (例: Scala^Z3) には適していません。

于 2011-12-30T16:16:56.467 に答える