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 はブルート フォース アプローチを使用します。基本的に、考えられるすべての組み合わせを試します。私たち（人間として）がすぐに目にする「賢い」証拠を見つけることはできません。私のマシンでは、サイズ 100 の配列を解くのに約 17 秒、サイズ 50 の配列を解くのに約 2.5 秒、サイズ 10 の配列を解くのに 0.1 秒かかります。

ただし、量指定子を使用して問題をエンコードすると、任意の配列サイズを即座に証明できます。固定の配列サイズを指定する必要さえありません。このエンコーディングでは、 for all iin [0, N)、a1[i] > 0およびa2[i] < 0. 次に、stでj1andを見つけたいと言います。Z3 はすぐに戻ります。これは、Z3 Python API を使用してエンコードされた問題です。また、rise4fun でオンラインでも入手できます。j2[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 に答える