問題
5つの品物の価格と価値が以下の表に示されるようになっているとする． 価格の合計が 15以下で，価値の合計が 19以上になる場合はあるか?
| 品物 | 価格 | 価値 |
|---|---|---|
| 品物0 | 3 | 4 |
| 品物1 | 4 | 5 |
| 品物2 | 5 | 6 |
| 品物3 | 7 | 8 |
| 品物4 | 9 | 10 |
回答
example_knapsack.py
from z3 import *
price = [3, 4, 5, 7, 9]
value = [4, 5, 6, 8, 10]
X = [Int("X%s" % i) for i in range(5)]
s = Solver()
s.add([And(0 <= X[i], X[i] <= 1) for i in range(5)])
s.add(Sum([price[i]*X[i] for i in range(5)]) <= 15)
s.add(Sum([value[i]*X[i] for i in range(5)]) >= 19)
print(s.check())
if s.check() == sat:
print(s.model())
出力
価値の合計が19の場合、
unsat
価値の合計を18の場合、
sat
[X1 = 0, X0 = 1, X4 = 0, X3 = 1, X2 = 1]
解説
s.add(Sum([value[i]*X[i] for i in range(5)]) >= 19) の19が価値の合計に対する制約
ここを変えることで、価値の制限による違いを見ることができる。