コイン数最適化問題

コイン数最適化問題#

from z3 import *
from helper.z3 import all_solutions

この問題では、異なる種類のコインを使用して特定の金額を作る際に、必要なコインの枚数を最小化することを目的とします。例えば、134セントを作るために、使用するコインの総数を最小限に抑える最適な組み合わせを求めます。

  • 利用可能なコインの種類: 1セント, 2セント, 5セント, 10セント, 25セント, 50セント

  • 目標金額: 134セント

  • 目的: 使用するコインの総数を最小にする

Solverで全解を探索#

次のプログラムは通常の Solver を使って、コインの合計枚数が 8 以下のすべての解を求めます。all_solutions() は、本書で提供する関数であり、すべての可能な解を取得できます。

coins = [1, 2, 5, 10, 25, 50]
total = 134
max_coins = 8

x = [Int(f'n_{c}') for c in coins]
total_expr = Sum([c*n for c, n in zip(coins, x)])
count_expr = Sum(x)
s = Solver()
for c in x:
    s.add(c >= 0)
s.add(total_expr == total)
s.add(count_expr <= max_coins)

for m in all_solutions(s):
    print(m.eval(count_expr), {v:m[v] for v in x})

8 {n_1: 4, n_2: 0, n_5: 1, n_10: 0, n_25: 1, n_50: 2}
8 {n_1: 2, n_2: 1, n_5: 0, n_10: 3, n_25: 0, n_50: 2}
8 {n_1: 0, n_2: 2, n_5: 2, n_10: 2, n_25: 0, n_50: 2}
7 {n_1: 0, n_2: 2, n_5: 0, n_10: 3, n_25: 0, n_50: 2}
7 {n_1: 2, n_2: 1, n_5: 1, n_10: 0, n_25: 1, n_50: 2}
8 {n_1: 1, n_2: 4, n_5: 0, n_10: 0, n_25: 1, n_50: 2}
6 {n_1: 0, n_2: 2, n_5: 1, n_10: 0, n_25: 1, n_50: 2}
8 {n_1: 2, n_2: 1, n_5: 1, n_10: 0, n_25: 3, n_50: 1}
8 {n_1: 0, n_2: 2, n_5: 1, n_10: 0, n_25: 5, n_50: 0}
7 {n_1: 0, n_2: 2, n_5: 1, n_10: 0, n_25: 3, n_50: 1}
8 {n_1: 0, n_2: 2, n_5: 0, n_10: 3, n_25: 2, n_50: 1}

Optimizeを使う#

Optimize は、Z3の最適化モジュールであり、制約を満たしつつ目的関数を最小化または最大化する機能を提供します。通常の Solver は、与えられた制約を満たす解を見つけることが主な目的ですが、Optimize を使用すると、追加の最適化条件を適用し、最適な解を求めることができます。

Optimize の使い方は Solver と似ていますが、minimize() または maximize() を用いて最小化または最大化する目的関数を設定します。

opt = Optimize()
for c in x:
    opt.add(c >= 0)
    
opt.add(total_expr == total)
target = opt.minimize(count_expr)

opt.check()
m = opt.model()
print(m.eval(count_expr), {v:m[v] for v in x})

6 {n_1: 0, n_2: 2, n_5: 1, n_10: 0, n_25: 1, n_50: 2}
Contents