爲Z3 SAT求解

Question

XOR條款我使用Z3來解決問題，可滿足包括與每個22個投入幾百XOR條款。爲了以DIMACS形式對XOR子句進行編碼，我使用了Tseitin編碼。我的轉換將XOR分解爲更小的CNF子句，每個子句最多5個文字。到目前爲止，Z3無法設計SAT解決方案。

什麼可以/我應該做些什麼來改善我的編碼？

我已經看過高斯消元法，但這種可能沒有幫助，因爲XOR表達式不具有相同的輸入變量。

Answer 1

Z3有兩個SAT求解器引擎，您可以使用 策略框架啓用更高效的引擎。例如，看教程Z3 - strategies

還有就是說明了位向量公式中使用的策略的一部分：

(declare-const x (_ BitVec 16)) 
(declare-const y (_ BitVec 16)) 
(assert (= (bvor x y) (_ bv13 16))) 
(assert (bvslt x y)) 
(check-sat-using (then simplify solve-eqs bit-blast sat)) 
(get-model) 

這就是說，它是比較容易產生基於CDCL SAT硬盤 實例使用異或的求解器。 例如：

Randal E. Bryant: A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking 2008: 145-149 

Z3的更有效的解算器坐着（由上面的例子中的稱呼）具有用於檢測並用異或（等價）傳播一些 數據結構。