使用z3（邏輯QF_BV）獲得「良好」不飽和核心

Question

我正在使用Z3 SMT求解器來解決我在邏輯QF_BV中使用SMTLIB 2語言表達的問題。

該模型是不可滿足的，我試圖讓解算器產生一個不飽和的核心。

我的模型由幾個'強制性'約束組成，我使用assert語句指定。

我希望用於不飽和核心生成的斷言已使用(assert (! (EXPR) :named NAME))構造指定。如預期的那樣，Z3給我unsat。然而，Z3似乎總是傾倒一個由所有命名斷言組成的「微不足道」的不足核心。

我知道存在我命名斷言的一個子集，它是一個不可核心的。我發現這個核心使用Yices SMT解算器，它經常給我相對較小的不飽和核心。 Yices模型與Z3模型相同（幾乎是從SMT2到Yices輸入語言的逐行翻譯）。

正在生產「良好」不飽和核心的解算器特定功能，還是有任何通用的建議/更改，我可以幫助Z3給我一個更好的核心？

Answer 1

Z3和Yices 1.x使用相同的方法計算不飽和核。跟蹤所有用於證明不可滿足性的論斷。但是，每個系統建立的證明可能完全不同。除Z3和Yices提供的功能之外，還有用於計算最小不飽和內核的算法。這是一個reference。

編輯：默認情況下，Z3在嘗試解決問題之前使用幾個預處理步驟。其中一些步驟可能會影響不飽和核心的產生。特別是，它使用問題中的等式消除了常量。我們說Z3「解決」方程並消除變量。在您的script中，通過禁用此步驟可以獲得更小的內核。我們可以通過使用選項

(set-option :auto-config false) 

Z3將執行非常一般的配置。對於位向量問題，它通常是一個好主意，禁用「relevacy傳播」：

(set-option :relevancy 0) 

最後，我們現在可以啓用/禁用的變量消除一步，看到的不飽和度的核心大小的影響。

(set-option :solver true) ;; Z3 will generate the core C0 C1 C2 
(set-option :solver false) ;; Z3 will generate the core C1 C2