Не могу сгенерировать модель с Z3 - PullRequest
Новая
       4

Не могу сгенерировать модель с Z3

3 голосов
/ 29 января 2012

У меня есть следующий пример кода для проблемы с рюкзаком в файле с именем "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)".

Может ктоскажите мне, почему это не работает?

Спасибо.

1 Ответ

5 голосов
/ 29 января 2012

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
...