Z3Py 例題 部分和問題

問題

集合 {2,3,5,8,13,21,34} の部分集合で， 和が50になるものはあるか?

回答

example_coin2.py

from z3 import *

X = [2, 3, 5, 8, 13, 21, 34]
a = [Bool("a%s" % i) for i in range(len(X))]

s = Solver()
s.add(Sum([X[i]*a[i] for i in range(len(X))]) == 50)

print(s.check())
if s.check() == sat:
    m = s.model()
    subset = []
    for i in range(len(X)):
        if m[a[i]] == True:
            subset.append(X[i])

print(subset)

出力

sat
[3, 5, 8, 13, 21]

解説

Bool("a")で、ブーリアン型の変数を定義できる。
Sum()で、入力したものの総和を計算します。（配列でなくてもOK）
例）Sum([a, b, c])　→　a + b + c
Sum()の詳細

他の例題

Z3Py個人的ポータル へ