如何查找建模/檢查Z3中可滿足性所需的內存和時間（NET API）

Question

我正在使用Z3和Yices解決一些研究問題的時間不到一年。使用這些求解器，我總是需要評估性能，特別是兩件事：建模/檢查（可滿足性）所需的時間和空間（內存）。在Z3的情況下，我發現沒有線索直接找到它們。我嘗試了「統計」（使用Z3 NET API提供的「DisplayStatistics」功能），並找到如下所示的輸出（例如）：

num。衝突：122

num。決定：2245

num。傳播：27884（二進制：21129）

num。重新啓動：1

num。最終檢查：1

num。分鐘。 lits：52

num。添加等式：3766

num。 mk bool var：2782

num。 del bool var：658

num。 mk enode：1723

num。 del enode：78

num。 mk從句：3622

num。 del子句：1517

num。 mk bin子句：3067

num。 mk lits：18935

num。 ta衝突：28

num。添加行：5091

num。樞軸：328

num。 assert lower：2597

num。 assert upper：3416

num。 assert diseq：1353

num。 bound prop：787

num。固定等式：697

num。偏移等式：866

num。 pseudo nl .: 34

num。 EQ。適配器：820

我不知道如何解釋這些值以瞭解使用的內存/時間。有一些方法可以找到運行時間（使用計時器類，如秒錶）。但是，在空間需求的情況下，我沒有找到任何方法。如果我可以得到建模所需的布爾變量（低級別，SAT解算器）的數量對我來說可以很好地工作。

這將是偉大的，如果任何人都可以告訴我的解決方案。

Answer 1

您正在使用哪個版本的Z3？最新版本（Z3 3.2）包含內存消耗統計信息。它將顯示爲max. heap size。這就是說，評估Z3性能的最好方法是使用z3.exe。 Z3可執行文件將報告時間和內存消耗。此外，一些性能改進尚未通過API獲得。

對於多個應用程序，文本界面是理想的選擇。也就是說，您的應用程序通過管道使用SMT 2.0命令與Z3進程通信。主要優點是：使用不同的SMT解算器並比較它們非常容易;很容易殺死Z3並重新啓動它;你可以創建幾個不同的進程;如果Z3死了你的應用程序不會死。當然，這種解決方案對於執行數千個簡單查詢或需要與Z3緊密集成的應用程序（例如Scala^Z3）並不適用。