量詞與非量詞

假設我有一個數組，我想計算數組索引0，1和2這個數組 -

(declare-const cpuA (Array Int Int)) 
(assert (or (= (select cpuA 0) 0) (= (select cpuA 0) 1))) 
(assert (or (= (select cpuA 1) 0) (= (select cpuA 1) 1))) 
(assert (or (= (select cpuA 2) 0) (= (select cpuA 2) 1)))

或者否則我可以使用forall構造作爲指定相同的 -

現在我想了解他們之間的區別。第一種方法可以快速執行並提供簡單易讀的模型。相比之下，第二個選項的代碼量非常少，但程序需要時間來執行。而且解決方案也很複雜。

我想使用第二種方法，因爲我的代碼會變得更小。但是，我想找到一個可讀的簡單模型。

來源

2012-04-04 Raj

量詞推理通常非常昂貴。在你的例子中，量化公式等同於你提供的三個斷言。但是，這不是Z3如何決定/解決你的公式。 Z3使用稱爲基於模型的量化器實例（MBQI）的技術來解決您的公式。該技術可以決定許多片段（請參閱http://rise4fun.com/Z3/tutorial/guide）。它主要對本指南中描述的片段有效。它支持未解釋的函數，算術和位矢量理論。它對數組和數據類型的支持也有限。這足以解決你的例子。由Z3生成的模型似乎更復雜，因爲使用相同的引擎來決定更復雜的碎片。該模型應該看起來像一個小功能程序。你可以找到這種方法在下面的文章是如何工作的更多信息：

需要注意的是，陣理論是代表/模擬無界或主要用大陣列。也就是說，陣列的實際大小不知道或者太大。大，我的意思是你的公式中的數組訪問次數（即selects）遠小於數組的實際大小。我們應該問自己：「我們真的需要用於建模/解決問題X的數組嗎？」。您可以考慮以下替代方案：

（Uninterpreted）函數而不是數組。您的例子也可以編碼爲：

（聲明芬CPUA（INT）智力）

（斷言（或（=（CPUA 0）0）（=（CPUA 0）1）））
（斷言（或（=（CPUA 1）0）（=（CPUA 1）1）））
（斷言（或（=（CPUA 2）0）（=（CPUA 2）1）））
程序化API。我們已經看到很多使用數組（和函數）來提供緊湊編碼的例子。一個緊湊和優雅的編碼不一定更容易解決。實際上，這通常是相反的。您可以使用Z3的編程API實現兩全其美（性能和緊湊）。在下面的鏈接中，我使用一個「變量」爲「數組」的每個位置編碼了您的示例。宏/函數用於編碼約束，例如：表達式是0或1。 http://rise4fun.com/Z3Py/JF

來源

2012-04-05 21:02:33

親愛的萊昂納多，我又回來同樣的問題。我正在嘗試優化座標解算器的代碼。你能告訴我什麼時候使用常量以及何時使用未解釋的函數是好的。例如，我的代碼中有大約30-40個未解釋的函數。當我將一些函數替換爲多個常量（例如（xA 0）替換爲xA0等等）時，我的運行時間減少了，但對於其他我沒有得到的。在它們之間進行選擇的關鍵規則是什麼？它依賴於你在代碼中使用它們多少？ – Raj 2012-05-31 08:44:10

波動是表現是非常普遍的。即使我們進行小的修改，例如對斷言重新排序，我們也會觀察到波動。任何細微的修改都可能會改變Z3遍歷搜索空間的順序。作爲一個經驗法則，我們應該儘可能避免量詞。如果我們可以使用單一理論對問題進行編碼，我們通常會獲得更好的性能。當然，我們總是有例外。你觀察到什麼樣的性能波動？它是2倍，10倍，100倍的數量級？ – 2012-05-31 18:41:22

量詞與非量詞

回答

相關問題