0

我想用 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 求解时间。谢谢。

4

1 回答 1

3

为了解决这个问题，Z3 将使用 Brute-force 方法，它基本上会尝试所有可能的组合。它无法找到我们（作为人类）立即看到的“智能”证据。在我的机器上，求解大小为 100 的数组大约需要 17 秒，大小为 50 的数组需要 2.5 秒，大小为 10 的数组需要 0.1 秒。

但是，如果我们使用量词对问题进行编码，它可以立即证明任何数组大小，我们甚至不需要指定固定的数组大小。在这种编码中，我们说对于所有iin[0, N)和。然后，我们说我们想在st中找到and 。Z3马上就回来了。这是使用 Z3 Python API 编码的问题。它也可以在rise4fun 在线获得。a1[i] > 0a2[i] < 0j1j2[0, N)a1[j1] = a2[j2]unsat

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)一个数组中的索引只有正值，而另一个只有负值。

于 2013-01-14T14:42:13.593 回答