在Z3中使用證明目標減少使用子句的數量

Question

我正在試驗優化Z3的用法以證明關於一階理論的事實。目前，我在Python中指定了一階理論，將量詞拼湊在那裏，並將所有的子句以及否定證明目標發送給Z3。我有以下想法，我希望能夠優化結果：我只想將理論中的公式發送到Z3，即相關的以證明目標。我不會詳細討論這個概念，但我認爲直覺很簡單：我的理論是公式的聯合，我只想發送可能影響證明目標真值的連詞。

我的問題是如下：這可以提高效率，還是Z3已經使用類似的方法？我猜不會，因爲我不認爲Z3總是認爲最後的斷言是證明目標，所以它沒有辦法優化它。

Answer 1

是的，刪除不相關的事實可以產生很大的不同。假設我們有一個不可滿足的公式F_1 and F_2 and (not G)。此外，讓我們假設F_1 and (not G)是不可滿足的，並且F_2是可滿足的。 F_2就是你所說的無關緊要的東西。如果在將配方發送到Z3之前有一個便宜的方法來刪除F_2，它可能會有很大的不同。

Z3有「無視」無關事實的啓發式，但它們只是啓發式。就我們的例子而言，最壞的情況是F_2，這對Z3來說確實很難滿足。 Z3基本上試圖建立一個滿足輸入公式的解釋/解決方案（在我們的工作示例中公式爲F_1 an F_2 and (not G)）。當Z3表明不可能構建解釋時，公式是不可滿足的。實際上，公式F_2與Z3無關，只要它能夠快速表明它是可滿足的，並且F_2的解釋/解決方案不會衝突F_1 and (not G)。如果情況並非如此，Z3會浪費大量資源F_2。