z3的內存使用情況

我正在使用z3來解決線性混合自動機的可達性問題。我在有限的內存下運行實驗。我對內存使用感到困惑。有一種情況z3可以在有限的內存下給出綁定2500的內存。但是，當綁定設置爲2000時，z3的內存使用超過了最大許可。這是什麼原因？z3的內存使用情況

來源

2013-01-07 Dingbao Xie

請提供更多信息。產生這種行爲的案例/問題是什麼？你能提供一個鏈接嗎？你是如何設定界限的？你在使用API或命令行工具嗎？ –

這種情況是溫度控制系統自動機的可達性分析。首先，我將自動機的有界行爲編碼爲SMT問題，然後使用z3來解決它。事實上，綁定2500下的這個自動機的約束數大於綁定2000下的約束數。我通過命令行使用z3：'z3 -st tcs_2000.smt2'。綁定2000和2500的這個自動機的smt2文件在這裏：http：//seg.nju.edu.cn/BACH/Demo/tcs_2000.smt2 http://seg.nju.edu.cn/BACH/Demo/tcs_2000 .smt2 –

SMT2文件中的約束數量較少並不一定意味着Z3將使用較少的內存來解決問題。例如，一個小但不可滿足的問題可能需要更多的內存，而不是一個大的可滿足的問題。

設置自動機展開的下界可能會將可滿足的問題（在2500邊界處）變成不可滿足的問題（在2000邊界處），這反過來使Z3的問題變得更加困難，甚至儘管限制較少。因此，Z3會使用更多的時間和/或內存。

解決此問題可能需要對問題進行不同編碼或在解算器上使用不同的選項，例如調整啓發式方法，以便更頻繁地獲得「幸運」並更早地找到解決方案。

來源

2013-01-07 16:56:52

感謝您的回覆。事實上，這個自動機是無法訪問的。約束2500下的自動機的行爲包含約束2000下的行爲。對於不可滿足的有界模型檢查問題，是不是越小的約束意味着解決時間越少？ –

通常，但並非總是如此。這很大程度上取決於求解器中的啓發式算法。你能否指出差異有多大？ –

例如，問題A是a-> b，a或b，更大的問題B是a-> b，b-> c，a或b或c。 –

z3的內存使用情況

回答

相關問題