無法生成與Z3

Question

模型

我有一個文件中的揹包問題稱爲「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行是最後一行 「（獲得的模型）」。

有誰能告訴我爲什麼這不起作用？

謝謝。

Answer 1

Z3產生滿足實例的模型。 你的公式不能令人滿意。使用限制

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

我們有o1 = 0和s1 = 3，s2 = 3，s3 = 5和filled = 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