Z3使用什麼方法來解決無量化位元矢量公式（QF_BV）？

Question

特別是，它使用DPLL（T）嗎？它是否使用低於/超過近似值？它是否處理字級的線性算術？非線性算術呢？

我在紙Efficiently Solving Quantified Bit-Vector Formulas中只發現了一個「簡化類似於MathSAT/Boolector中的簡化」的表面提及。

非常有趣的是，什麼方法可以幫助Z3在smtcomp的QF_BV部分獲得第一名。

Answer 1

DPLL（T）完全不用於解決QF_BV問題。 關於「有效解決定量比特向量公式」的論文的評論大約是Z3 2.x. QF_BV是關於問題編碼的。預處理有很大的不同。 我從零開始爲Z3 3.0構建了一個新的預處理堆棧和SAT解算器。 新的預處理器比Z3 2.x中使用的預處理器快得多，並執行更積極的簡化。 沒有魔法或花哨的技巧。在預處理步驟之後，Z3位將所有內容進行轟擊並調用新的SAT求解器。 Z3不使用位向量的下/近似，或者字級算術推理或對非線性算子的特殊支持。順便說一句，少數求解者考慮到的一件事是，一些簡化可能會在本地減小公式的大小，但會在全局範圍內增加它，因爲它們會破壞共享。 Z3也使用預處理步驟，試圖增加線性和非線性位向量算法中的共享量。