Z3：用量詞建模

Question

我想通過z3來證明(∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0)。否定它是：∀i(0≤i<k→a[i]>0)∧a[k]>0∧∃i(0≤i≤k∧¬(a[i]>0))。首先，我k的值設置爲5，而忽略部分a[k]>0，並嘗試：

from z3 import * 
i = Int('i')` 
a = Array('a',IntSort(),IntSort()) 
solver = Solver() 
solver.add(ForAll(i, Implies(And(i >= 0,i < 5),a[i] > 0))) 
solver.add(Exists(i, And(i >= 0,i <= 5, Not(a[i] > 0)))) 
print solver.check() 
print solver.model() 

輸出是：

sat 
[i!0 = 5, 
a = [else -> k!8!10(k!9(Var(0)))], 
k!8 = [else -> k!8!10(k!9(Var(0)))], 
k!9 = [else -> If(Var(0) >= 4, If(Var(0) >= 5, 5, 4), 0)], 
k!8!10 = [0 -> 7720, 4 -> 1, else -> -38]] 

我不知道輸出的意思，我想其型號應該是i = 5。然後，我加入a[5] > 0，我認爲它應該是不滿意的。代碼如下：

from z3 import * 
i = Int('i') 
a = Array('a',IntSort(),IntSort()) 
solver = Solver() 
solver.add(ForAll(i, Implies(And(i >= 0,i < 5),a[i] > 0))) 
solver.add(Exists(i, And(i >= 0,i <= 5, Not(a[i] > 0)))) 
solver.add(a[5] > 0) 
print solver.check() 
print solver.model() 

，輸出是：

unsat 

那麼，怎樣才能通過我證明z3py (∀i(0≤i<k→a[i]>0)∧a[k]>0)→∀i(0≤i≤k→a[i]>0)，什麼是輸出的含義是什麼？

Answer 1

這對我來說有點不清楚，你試圖對你的查詢做什麼。你爲什麼要「設定」k的值？根據問題的開始，這似乎不符合你試圖證明的一般情況，但也許現在你所感興趣的是特例。

您已將您的有效性問題正確地轉換爲可滿足性問題：如果原始公式有效，則公式的否定可以滿足。

在Z3的第一個響應中，確實得到了一個模型;這表明了你試圖證明的（較弱的）第一含義的反例。如果你考慮這個反例的示例需要什麼，你必須選擇將（存在的）存在變量實例化爲5.這就是模型中i！0的意義。它是一個新的（自由）名稱，代表您的模型的元素，存在的變量被分配到該元素。在Z3做有趣的工作之前，存在量詞被「skolemised」掉了（存在界限的變量被一個新的常量所取代），看看這個另一種方式（更準確地說，就這個工具的作用而言） ，所以它實際上解決一個查詢等效於查詢公式的satifiability：

∀i(0≤i<k→a[i]>0)∧a[k]>0∧(0≤ i!0 ≤k∧¬(a[ i!0 ]>0)) 

當你加強查詢回原來的蘊涵的否定，你從Z3得到不飽和度這意味着這個否定公式是不可滿足的，所以你感興趣的含義是有效的;你已經證明 ∀i（0≤i< 5→A [1]> 0）∧a[5]> 0）→∀i（0≤i≤5→A [1]> 0）

您如果您在問題中跳過設置k爲5，應該得到相同的結果。

對於來自Z3的第一個響應中的其他信息，模型必須不僅包含（skolemised）i的值，還包含問題中的數組a。數組被表示爲函數，它可以由這種模型中的個案來定義; 「其他」案例是這裏所使用的每個功能中唯一的案例。 Var（0）是該函數（僅有的第一個參數）的語法。在這個模型中，數組是通過兩個其他函數的組合間接定義的，它們似乎用來標識與模型相關的部分索引集合;在這種情況下，它是0,4和5），以及k！8！10（它定義了這些索引到值的映射）。特別是，在這個模型中，數組存儲7720在索引0處，1在索引4處，而-38在索引5處（沒有其他索引由k的情況產生！9的定義;從概念上講，我會理解這是因爲這個模型中的數組在其他指數中是未定義的）。