用尽量少的硬币付款：借助 Optimize 直接求出最优解

用尽量少的硬币付款：借助 Optimize 直接求出最优解#

本章的内容#

Z3 要回答的问题有两类。

  • 约束满足问题：找出满足条件的一个解

  • 优化问题：在满足条件的解里挑出最好的一个

本章用两种方法解同一个关于硬币枚数的问题，再比较两者的差别。

  • 用 Solver 收集解再比较，这时只能自己数出枚数

  • 用 Optimize 直接求出枚数最少的解

  • 用 lower() 与 upper() 确认它确实是真正的最优值

问题#

用尽量少的硬币付出 134 美分，应该如何组合。

  • 可用的硬币：1、2、5、10、25、50 美分

  • 要凑出的金额：134 美分

  • 目的：使所用的硬币枚数尽量少

“合计为 134 美分”是约束，“枚数最少”是目的，两者在 Z3 中要分开写出。约束用于筛出全部可行解，目的用于在可行解之间排序；混在一处，就分不清哪一条是必须满足的条件，哪一条只是优劣的判据。两者的分工是本章首先要说明的要点，也是后面选用 Optimize 的理由。

先用 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 并不按枚数多少的顺序搜索，这次 6 枚的组合最后才出现，而这个顺序并没有任何保证

  • 把全部解收集起来逐一比较，耗时随解的数量增长；去掉 max_coins 的上限之后，解达到 11,713 种，逐个比较已经难以完成

  • 上限取 8 枚也是事先给定的值，并没有证明少于 6 枚的付款方式不存在

用于寻找最好解的工具，就是 Optimize。

用 Optimize 直接求出枚数最少的解#

Optimize 在满足条件的解中，寻找使目标函数最小或最大的解，这里的目标函数就是枚数。用法与 Solver 几乎相同，只需再加上一个 minimize()。差别在于求解过程：Optimize 记录当前找到的最优可行解，并据此排除不可能更优的部分。

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 枚组合。这一段去掉了枚数的上限，约束只剩“合计为 134 美分”，最少的枚数因此由优化过程求出。

minimize() 返回的是目标函数的句柄，借助它就可以确认最优值能确定到什么程度，即 Z3 所能保证的范围有多宽。

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() 给出的是最优值落在这个范围内的保证。已找到一个 6 枚的解，最优值不会超过 6，这是上界；求解器又证明了不存在更少的可行解，最优值不会小于 6，这是下界。第一种情形是不加“不少于 7 枚”这条约束，此时上下界都是 6，因此 Z3 表明了不存在用少于 6 枚付款的方法。

第二种情形是加上“不少于 7 枚”这条约束，6 枚的解被排除在外。Optimize 重新寻找最优值，剩下的最好解是 7 枚，上下界也随之移到 7。

用 Solver 只能从已找到的解里挑出较好者，无法判断是否还有更好的解。Optimize 给出上下界，上下界一致时就能断定这是最优值，这也是它与 Solver 最大的差别。

Solver

Optimize

目的

找出一个满足条件的解

找出使目标函数最优的解

追加约束

solver.add()

opt.add()

优化

不可

opt.minimize() 与 opt.maximize()

得到的结果

其中任意一个，未必最优

最优的那一个

最优性的保证

没有

可用 lower() 与 upper() 确认

写成函数，再换一种硬币#

同一形式的问题写成函数之后可以反复使用，不必每次重写；下面用日元把同一个问题再算一次，确认代码与币种无关。

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 找出一个解或者全部解，但无法判断它究竟是不是最优

  • Optimize 用 minimize() 与 maximize() 指定目标函数，再求出最优解

  • lower() 与 upper() 一致时，这个值就是真正的最优值

  • 收集全部解的做法，解一多就难以应付，本题去掉上限之后共有 11,713 种解