Z3Py 例題 コイン問題（制約充足問題）

問題

1円硬貨，5円硬貨，10円硬貨を合計で15枚，それぞれを1枚以上持っている．
金額の合計は90円である． それぞれの硬貨を何枚持っているか?

回答

example01_coin.py

from z3 import *

coin__1yen = Int("coin__1yen")
coin__5yen = Int("coin__5yen")
coin_10yen = Int("coin_10yen")

s = Solver()
s.add(coin__1yen >= 1)
s.add(coin__5yen >= 1)
s.add(coin_10yen >= 1)
s.add((coin__1yen + coin__5yen + coin_10yen) == 15)
s.add((coin__1yen + 5 * coin__5yen + 10 * coin_10yen) == 90)

print(s.check())
if s.check() == sat:
    print(s.model())

出力

sat
[coin__5yen = 3, coin_10yen = 7, coin__1yen = 5]

解説

【基本的な順序】
Int()等で変数を定義し、s=Solver()にs.add()で条件・制約を定義する。
s.check()で解があるかを確認する。（たぶん、ここで演算をしている）
解がある場合、「sat」が返ってき、解がない場合は「unsat」が返ってくる。
「sat」が返ってきた場合、s.model()で条件を満たす解の1つが取得できる。
（一つしか出てこないため、条件を満たす解が見つかった時点で探索を終了すると思われる）

他の例題

Z3Py個人的ポータル へ