3

「knapsack.smt2」というファイルに、ナップザックの問題に対する次のサンプル コードがあります。これは smt2 形式であると思われ、最新バージョンの Z3 を使用しています。

(declare-const s1 Int)
(declare-const o1 Int)
(declare-const b1 Bool)

(declare-const s2 Int)
(declare-const o2 Int)
(declare-const b2 Bool)

(declare-const s3 Int)
(declare-const o3 Int)
(declare-const b3 Bool)


(declare-const sack-size Int)
(declare-const filled Int)

(assert (< o1 sack-size))
(assert (< o2 sack-size))
(assert (< o3 sack-size))

(assert (>= o1 0))
(assert (>= o2 0))
(assert (>= o3 0))

(assert (=> (not b1)(= o1 o2)))
(assert (=> (not b2)(= o2 o3)))

(assert (=> b1 (= (+ o1 s1) o2)))
(assert (=> b2 (= (+ o2 s2) o3)))
(assert (=> b3 (= (+ o3 s3) filled)))

(assert (=> (not b3) (= o3 filled)))
(assert (<= filled sack-size))

(assert ( = o1 0))


(assert ( = s1 3))
(assert ( = s2 4))
(assert ( = s3 5))
(assert ( = sack-size 20))

(assert ( = filled 13))

(check-sat)
(get-model)

ただし、「z3 -m knapsack.smt2」を実行すると、次のエラー メッセージが表示されます。

>> z3 -m knapsack.smt2
unsat
(error "line 46 column 10: model is not available")

ここで、46 行目は最後の行「(get-model)」です。

これが機能しない理由を誰か教えてもらえますか?

ありがとう。

4

1 に答える 1

5

Z3 は、充足可能なインスタンスのモデルを生成します。あなたの式は満足できません。制約の使用

(assert ( = o1 0))
(assert ( = s1 3))
(assert ( = s2 4))
(assert ( = s3 5))
(assert ( = filled 13))

制約を使用o1 = 0しs1 = 3てs2 = 3_s3 = 5filled = 13

(assert (=> (not b1)(= o1 o2)))
(assert (=> b1 (= (+ o1 s1) o2)))

o2 = 0またはがありo2 = 3ます。

使用する

(assert (=> (not b2)(= o2 o3)))
(assert (=> b2 (= (+ o2 s2) o3)))

私たちはそれを持っているo3 = o2か、o3 = o2 + 3 使用しています

(assert (=> b3 (= (+ o3 s3) filled)))
(assert (=> (not b3) (= o3 filled)))

私たちはそれを持っていますo3 = 8かo3 = 13

今、私たちは対立を見ることができます

o2 = 0 or o2 = 3
o3 = 8 or o3 = 13
o3 = o2 or o3 = o2 + 3

しようとo2 = 0すると、満たされない式が得られます

o3 = 8 or o3 = 13
o3 = 0 or o3 = 3

しようとo2 = 3すると、満たされない式が得られます

o3 = 8 or o3 = 13
o3 = 3 or o3 = 6
于 2012-01-29T02:27:32.727 に答える