在Z3中，在數組理論中描述這個最有效的方法是什麼？

Question

我想用Z3來描述下面的問題。

int []array1=new int[100]; 
int []array2=new int[100]; 
array1[0~99]={i0, i1, ..., i99}; (i0...i99 > 0) 
array2[0~99]={j0, j1, ..., j99}; (j0...j99 < 0) 
int i, j; (0<=i<=99, 0<=j<=99) 
does array1[i]==array2[j]? 

這是不可滿足的。

我用Z3到如下描述這個問題：

(declare-const a1 (Array Int Int)) 
(declare-const a2 (Array Int Int)) 
(declare-const a1f (Array Int Int)) 
(declare-const a2f (Array Int Int)) 
(declare-const x0 Int) 
....  
(declare-const x99 Int) 
(assert (> x0 0)) 
.... 
(assert (> x99 0)) 
(declare-const y0 Int) 
....  
(declare-const y99 Int) 
(assert (< y0 0)) 
.... 
(assert (< y99 0)) 
(declare-const i1 Int) 
(declare-const c1 Int) 
(assert (<= i1 99)) 
(assert (>= i1 0)) 

(declare-const i2 Int) 
(declare-const c2 Int) 
(assert (<= i2 99)) 
(assert (>= i2 0)) 
(assert (= a1f (store (store (store (store (store (store (store (store ........ 95 x95) 96 x96) 97 x97) 98 x98) 99 x99))) 
(assert (= a2f (store (store (store (store (store (store (store (store ........ 95 y95) 96 y96) 97 y97) 98 y98) 99 y99))) 

(assert (= c1 (select a1f i1))) 
(assert (= c2 (select a2f i2))) 
(assert (= c1 c2)) 
(check-sat) 

是不是？ 有沒有其他更有效的方法來描述這個使用數組理論？ 我的意思是，更有效的方法需要更少的Z3解決時間。 謝謝。

Answer 1

爲了解決這個問題，Z3將使用暴力方法，它將基本上嘗試所有可能的組合。它無法找到我們（像人類）立即看到的「聰明」證據。 在我的機器，大約需要17秒爲求解大小100的陣列，2.5秒爲大小爲50的陣列，以及0.1秒爲尺寸的陣列10

然而，如果我們使用的量詞編碼問題，它可以即時證明任何數組大小，我們甚至不需要指定固定的數組大小。 在這種編碼中，我們說i中的所有[0, N),a1[i] > 0和a2[i] < 0。然後，我們說我們想要在[0, N) s.t.中找到j1和j2。 a1[j1] = a2[j2]。 Z3會立即返回unsat。這是使用Z3 Python API編碼的問題。 It is also available online at rise4fun。

a1 = Array('a1', IntSort(), IntSort()) 
a2 = Array('a2', IntSort(), IntSort()) 
N = Int('N') 
i = Int('i') 
j1 = Int('j1') 
j2 = Int('j2') 
s = Solver() 
s.add(ForAll(i, Implies(And(0 <= i, i < N), a1[i] > 0))) 
s.add(ForAll(i, Implies(And(0 <= i, i < N), a2[i] < 0))) 
s.add(0 <= j1, j1 < N) 
s.add(0 <= j2, j2 < N) 
s.add(a1[j1] == a2[j2]) 
print s 
print s.check() 

在上面的編碼中，我們使用量詞來總結Z3在您的編碼中無法自行找出的信息。對於[0, N)中的指數，一個數組只有正值，而另一個只有負值。