Z3：更好的建模方式？

我有兩個SMT問題實例。第一個是在這裏：Z3：更好的建模方式？

http://gist.github.com/1232766

Z3在我不那麼偉大的機器，這是偉大的約2分鐘返回一個模型，這個問題..我也有這樣一條：

http://gist.github.com/1232769

我已經在這個問題上過夜z3，沒有Z3完成。如果您檢查這些文件的內容，您會看到第二個與第一個相同，除了它有一個額外的斷言來「拒絕」第一個實例返回的模型。（你可以在它們之間做一個「差異」來看看我的意思。）我碰巧知道這個問題有多個令人滿意的模型，我試圖用z3來找到所有令人滿意的模型。

我知道這可能是完全可以預料的，但我很想知道爲什麼第二個問題對Z3來說比第一個問題更爲棘手。有沒有更好的方法來制定第二個問題，所以Z3會有更輕鬆的時間？

謝謝..

來源

2011-09-21 Levent Erkok

這是很難給你一個準確的答案不知道更多關於你的應用程序。正如您所建議的那樣，建模在您使用的邏輯中扮演着重要角色：AUFBV。 Z3使用的策略對整體性能也有很大影響。 Z3配備了幾種內置策略。它有許多參數可以用來影響搜索。 Z3也有策略規範語言。這是一項新功能。我沒有做廣告，因爲它正在進行中，而且在接下來的版本中，語言很可能會發生變化。您可以通過執行命令訪問有關戰略語言的更多信息：

(help check-sat-using) 
(help-strategy)

話雖這麼說，有在Z3一個內置的策略，這似乎是對你問題的有效。這是用於邏輯UFBV的策略。您的問題，使用數組，但他們可以通過將table0成函數有兩個參數來避免：

(declare-fun table0 ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 8))

而且隨着(table0 s65 t)替換形式(select (table0 s65) t)的各項條款，其中t是任意的術語。最後，您還必須在文件的開頭添加命令(set-logic UFBV)。使用此設置，我設法爲您的查詢生成4種不同的模型。我沒有嘗試生成更多。每次通話消耗大約75秒。

來源

2011-09-21 20:26:16

謝謝，切換到v3.2和使用AUFBV幫助。我現在看到約。每分鐘一個解決方案，這是相當不錯的。順便說一句，有沒有更好的方法來連續生成「全部」令人滿意的模型？到目前爲止，我一直在解析第一個模型的結果，並生成一個新程序來添加約束來拒絕原始數據，爲每個新模型重新啓動Z3。如果有一種方法可以說'（get-next-model）'或類似的方法，那麼Z3會返回一個不同的模型（如果存在的話）會更好。 –

我們沒有像get-next-model這樣的命令。但是，可以使用C API自動執行此功能。順便說一句，我相信Philippe Suter（http://lara.epfl.ch/~psuter/）實現了這個功能。 –

Z3：更好的建模方式？

回答

相關問題