少ない枚数で払う ― Optimize で最適化する#
この章で学ぶこと#
Z3 には、答える問題が2種類あります。
制約充足問題：条件を満たす解を1つ見つける
最適化問題：条件を満たす解の中で、一番よいものを探す
この章では、同じ「コインの枚数」の問題を両方の方法で解いて、何が違うのかを見ます。
Solverで解を集めて比べる（枚数を数えるしかない）Optimizeで「枚数が最小の解」を直接求めるlower()/upper()で「これが本当の最良」だと確かめる
問題#
134セントを、できるだけ少ない枚数のコインで払うには、どう組み合わせればよいでしょうか。
使えるコイン：1, 2, 5, 10, 25, 50 セント
作りたい金額：134 セント
目的：使うコインの枚数をできるだけ少なくする
「合計を134セントにすること」が制約で、「枚数を最小にすること」が目的です。Z3 では、この2つを別々に書きます。ここがこの章のポイントです。
まずは Solver で、条件を満たす解をすべて集める#
Solver は「条件を満たす解を見つける」道具です。最少の枚数を知りたいので、今回は条件を満たす解を全部取り出して、枚数を自分で比べてみます。
from z3 import *
from helper.z3 import all_solutions # 本書で用意している「全解を順に返す」関数
coins = [1, 2, 5, 10, 25, 50] # 使えるコインの種類（セント）
total = 134 # 作りたい金額
max_coins = 8 # とりあえず「8枚以下」にしぼっておく
counts = [Int(f"n_{c}") for c in coins] # 各コインの枚数
amount = Sum([c * n for c, n in zip(coins, counts)]) # 合計金額
num_coins = Sum(counts) # 合計枚数
solver = Solver()
for n in counts:
solver.add(n >= 0) # 枚数は 0 以上
solver.add(amount == total) # 合計はちょうど 134 セント
solver.add(num_coins <= max_coins) # 枚数は 8 枚以下
def show(model):
"""解を「8枚: 2セント×2, 5セント×1, ...」の形で表示する"""
used = {c: model.eval(n).as_long() for c, n in zip(coins, counts)}
used = {c: k for c, k in used.items() if k > 0} # 0枚のコインは省く
print(f"{model.eval(num_coins)}枚: " + ", ".join(f"{c}セント×{k}" for c, k in used.items()))
for model in all_solutions(solver):
show(model)
8枚: 2セント×2, 5セント×1, 25セント×5
8枚: 1セント×2, 2セント×1, 10セント×3, 50セント×2
8枚: 1セント×1, 2セント×4, 25セント×1, 50セント×2
8枚: 1セント×4, 5セント×1, 25セント×1, 50セント×2
7枚: 2セント×2, 5セント×1, 25セント×3, 50セント×1
8枚: 2セント×2, 10セント×3, 25セント×2, 50セント×1
8枚: 1セント×2, 2セント×1, 5セント×1, 25セント×3, 50セント×1
7枚: 2セント×2, 10セント×3, 50セント×2
8枚: 2セント×2, 5セント×2, 10セント×2, 50セント×2
7枚: 1セント×2, 2セント×1, 5セント×1, 25セント×1, 50セント×2
6枚: 2セント×2, 5セント×1, 25セント×1, 50セント×2
条件を満たす解は 11通り 見つかりました。一番少ないのは 6枚 の組み合わせです。
ただし、この方法には弱点があります。
Solverは「枚数が少ない順」に探しているわけではありません。今回は最後に出てきましたが、その順番に保証はありません。すべての解を集めて比べるので、解が多いと時間がかかります。実際、
max_coinsの上限を外すと解は 11,713通り になります。上限の8枚も、こちらが勘で決めた数字です。「6枚より少なく払う方法はない」と証明したわけではありません。
「一番よい解を探す」ための道具が Optimize です。
Optimize で「枚数が最少の解」を直接求める#
Optimize は、条件を満たす解の中で目的関数（ここでは枚数）を最小・最大にする解を探します。使い方は Solver とほぼ同じで、minimize() を足すだけです。
opt = Optimize()
for n in counts:
opt.add(n >= 0)
opt.add(amount == total) # 金額の条件は同じ。枚数の上限はもういらない
obj = opt.minimize(num_coins) # 目的関数：合計枚数を最小にする
print(opt.check())
model = opt.model()
show(model)
print("合計:", sum(c * model.eval(n).as_long() for c, n in zip(coins, counts)), "セント")
sat
6枚: 2セント×2, 5セント×1, 25セント×1, 50セント×2
合計: 134 セント
同じ6枚が答えになりました。minimize() は「目的関数のハンドル」を返します。このハンドルを使うと、最良値がどこまでなら確かなのかを確かめられます。
print("最良値の下限:", opt.lower(obj))
print("最良値の上限:", opt.upper(obj))
# 少し悪くして比べてみる（上限を 7 にすると、6 枚の解は選べない）
opt.add(num_coins >= 7)
opt.check()
print("7枚以上の条件で:", opt.lower(obj), opt.upper(obj))
最良値の下限: 6
最良値の上限: 6
7枚以上の条件で: 7 7
lower() と upper() は「最良値はこの範囲にある」という保証です。1つ目の結果では両方とも 6 なので、6枚より少なく払う方法は存在しないと Z3 が示したことになります。
2つ目のように条件を足すと、範囲が 7 に動きます。Optimize は条件が変われば、そのつど最良値を探し直します。
Solver では「見つかった中で一番よいもの」しか言えませんでしたが、Optimize は「これが最良である」と言えます。ここが2つの大きな違いです。
|
|
|
|---|---|---|
目的 |
条件を満たす解を1つ見つける |
目的関数が最良の解を見つける |
制約の追加 |
|
|
最適化 |
できない |
|
得られる答え |
どれか1つ（最良とは限らない） |
最良の1つ |
最良である保証 |
なし |
|
関数にして、コインの種類を変えてみる#
同じ形の問題は、関数にしておくと使い回せます。おまけに、日本円でも試してみましょう。
def min_coin_counts(coin_types, amount):
"""金額 amount を最少枚数で作る組み合わせを返す"""
counts = [Int(f"n_{c}") for c in coin_types]
opt = Optimize()
for n in counts:
opt.add(n >= 0)
opt.add(Sum([c * n for c, n in zip(coin_types, counts)]) == amount)
opt.minimize(Sum(counts))
assert opt.check() == sat
model = opt.model()
return {c: model[n].as_long() for c, n in zip(coin_types, counts) if model[n].as_long() > 0}
print(min_coin_counts([1, 2, 5, 10, 25, 50], 134))
print(min_coin_counts([1, 5, 10, 50, 100, 500], 1340))
{2: 2, 5: 1, 25: 1, 50: 2}
{10: 4, 100: 3, 500: 2}
コインの種類と金額を変えるだけで、同じコードが使えます。1340円なら 500円×2 + 100円×3 + 10円×4 の9枚が最少、と答えが出ました。
まとめ#
制約充足問題は「条件を満たす解を探す」問題、最適化問題は「条件を満たす中で一番よい解を探す」問題
Solverは解を1つ（または全部）見つけるが、最良かどうかは分からないOptimizeはminimize()/maximize()で目的関数を指定し、最良の解を探すlower()とupper()が一致すれば、それが本当の最良値解を全部集める方法は、解が多いとすぐ手に負えなくなる（この問題では上限なしで 11,713通り）