Z3的對稱性破壞 - 在UFBV邏輯環境下（新版本）

（這是我第二次嘗試獲得幫助，如果問題/方法沒有意義或不明確，請讓我知道。也會很高興任何小提示或參考，這可以幫助我瞭解Z3與我的SBA的行爲）Z3的對稱性破壞 - 在UFBV邏輯環境下（新版本）

我正在使用UFBV Z3邏輯的關係規範的有界驗證。我正在研究的當前問題需要僞造所有可能的模型（因爲對可達性謂詞的負面使用），這會使解算器的性能在更高的範圍內發揮作用。因爲只有一部分可能的模型確實很有趣（不同構於其他模型），所以我試圖引入對稱破缺技術（在SAT領域中已知）。

然而，在某些情況下，我稱之爲對稱破缺公理可以提高Z3的性能，但解算器的一般性行爲變得不穩定。

我的一種方法（我認爲最有前途的方法）是基於打破關係w.r.t.的對稱性。他們的領域。它引入了關係R中的每個域D和D公理中的每個原子a \，這強制了R^{M}和R^{M [a + 1/a]}的二進制表示的順序，其中M是規範的一個模型。對於同質關係，公理是放鬆的。

設R是子集AxA的關係。我對R寬鬆的對稱性破缺公理是這樣的：

;; SBA(R, A)_upToDiag 
(assert 
(forall ((ai A) (aj A)) 
    (=> 
    (bvult ai aj) 
    (=> 
    (forall ((x A)) 
    (=> 
     (bvult x aj) 
     (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
    ) 
    ) 
    (=> 
    (R ai aj) 
    (R (bvadd ai (_ bv1 n)) aj) 
)))))  

;; SBA(R, A)_diag 
(assert 
(forall ((ai A)) 
    (=> 
    (forall ((x A)) 
    (=> 
     (bvult x ai) 
     (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
    ) 
    ) 
    (=> 
    (R ai ai) 
    (R (bvadd ai (_ bv1 n)) (bvadd ai (_ bv1 n))) 
))))

我的問題是，使用此SBAS的效果並不穩定/一致。它不同於綁定到另一個的形式說明。全部或僅使用一個SBA也會影響性能。

在SAT環境中，所謂的對稱破缺斷言（SBP）方法的成功基於SAT求解器的回溯能力，它（以某種方式）保證，如果求解器回溯，它將修剪搜索空間使用，其中包括SBP。

Z3上下文有什麼區別（如果有的話）？
我該如何執行解決方案才能使用這些公理來修剪搜索空間（當它回溯）？
我的SBA會使用（量詞）模式嗎？

問候，

Aboubakr Achraf埃爾加齊

來源

2012-02-15 Aboubakr Achraf El Ghazi

在Z3 3.2，存在用於處理定量公式兩個主要引擎：E-匹配和MBQI（基於模型的實例化量詞）。電子匹配僅在不可滿足的配方中有效。 Z3將無法表明使用該引擎的公式是可以滿足的。 MBQI更昂貴，但它可以顯示幾類公式（包含量詞）是可滿足的。 Z3 guide描述了這兩個引擎（和其他選項）。爲了在非平凡問題上有效地使用Z3，瞭解這兩種引擎的工作方式非常有用。

對稱性破壞通常是減少搜索空間的非常有效的方法。很難準確地確定問題中發生了什麼。我可以看到下面的解釋對於非穩定的行爲：

MBQI是不好受創建滿足SBAS的典範。雖然SBA修剪搜索空間，但如果問題是可以滿足的，Z3將嘗試構建滿足它們的解釋（模型）。所以，在這種情況下，SBA只是開銷。特別是如果輸入公式很容易滿足，但在添加SBA時變得困難。您可以使用選項MBQI_TRACE=true來確認此假設。 Z3將顯示消息，如：[mbqi] failed k!18。其中k![line-number]是量詞id。您可以使用標籤:qid分配您自己的ID。下面是一個例子：

（斷言（forall的（（X T）（Y T））（（=>（和（亞型XY）（亞型YX））（= XY））！ QID反對稱）））

BTW，您可以使用MBQI=false禁用MBQI模塊。

在未來的Z3版本中，我們計劃添加一個選項來禁用某些量化公式的MBQI。此功能可能對SBA有用。

另一種解釋是電子匹配創建了太多的SBA實例。您可以使用選項QI_PROFILE=true進行確認。 Z3將轉儲信息，諸如：

[quantifier_instances]反對稱：12：1：2.00

第一個數字是生成的實例的數量。如果這是問題的根源，則一種解決方案是爲正在生成太多實例的SBA分配限制性模式。例如，Z3將使用(R ai aj)作爲SBA(R, A)_upToDiag的模式。這種模式可能會創建二次數的實例。另一個實驗是禁用電子匹配。例如，選項

AUTO_CONFIG=false EMATCHING=false MBQI=true

你也可以嘗試在配置以禁用上述相關性傳播，選項：RELEVANCY=0。

最後，另一種選擇是生成您認爲有用的SBA實例，並刪除量化的公式。

來源

2012-02-17 15:23:01

非常感謝你，你的插圖給了我一個改善我的方法的好起點。就我而言，到目前爲止，我正在處理不合格的規格。我將盡快在這裏報告我的調查結果（使用你的建議）。再次感謝你。 – 2012-02-20 19:15:32

順便說一句：對稱破缺公理是一些如何超過約束，這不影響可滿足性。在Z3中整合這個概念有多困難，因此如果求解器遇到衝突（後退軌道），則只考慮像SBAs這樣的約束。 Z3的理論插件框架是否適合？ – 2012-02-20 19:18:28

Z3支持理論插件。 Z3發行版帶有一個例子：'z3-3.2 \ examples \ theory'。主要缺點是您必須移動編程式API（您無法使用理論插件使用SMT 2.0前端）。 – 2012-02-24 18:13:54

Z3的對稱性破壞 - 在UFBV邏輯環境下（新版本）

回答

相關問題