运动会得分谜题：竞赛数目未知时如何求解

运动会得分谜题：竞赛数目未知时如何求解#

本章的内容#

本章的问题有一处与前面不同：不知道一共举行了几项竞赛。遇到这种情况，就按 2、3、4 的顺序依次试下去，把最先解出的项数作为答案。竞赛的项数决定变量的个数，不同的项数对应不同的约束集合，因此没法把各种情形写进同一组变量里。

  • 把未知的数目放在外层循环中穷举

  • 由名次得到分数的两种写法，即 If 与 Function

  • 用 m[score_func] 查看模型中函数的内容

3 个人参加运动会，参赛者只有这 3 人。每项竞赛给第 1 名、第 2 名、第 3 名分别记分，分数在所有竞赛中始终固定，即第 1 名总是 X 分，第 2 名总是 Y 分，第 3 名总是 Z 分。

分数是满足 X > Y > Z > 0 的整数。现在所有竞赛都已结束，结果是

  • A 总共 22 分

  • B 在标枪中得了第 1 名，总共 9 分

  • C 总共 9 分

那么，100 米赛跑的第 2 名是谁？

※ 本题参考了 https://sist8.com/3ath。

难点在哪里#

  • 竞赛数目未知：3 人的合计分数是已知的，但一共举行了几项竞赛并没有写出来

  • X、Y、Z 未知：只知道 X > Y > Z > 0 这个大小关系

  • 各项竞赛的名次未知：除了 B 在标枪中得第 1 名之外，谁得了第几名并不清楚

这些都是值未知的量，因此可以直接交给 Z3 作为变量，只写出条件即可。只有竞赛数目会改变变量的个数，因此要用循环来试。分数 X、Y、Z 对所有竞赛相同，无论几项竞赛，这三个变量始终只有三个。

改变竞赛数目求解#

try_solve(n) 是假定竞赛举行了 n 次来求解的函数。有解时显示结果并返回 True，无解时返回 False。项数一改，这道题就变成一个全新的约束问题，之前求出的分数与名次都不再沿用。

from z3 import *


def try_solve(n_games):
    """假设项目数为 n_games 来求解。有解就显示并返回 True"""
    X, Y, Z = Ints('X Y Z')          # 第 1 名、第 2 名、第 3 名的得分
    solver = Solver()
    solver.add(X > Y, Y > Z, Z > 0)

    # games['A', i] 是“A 在第 i 个项目中的名次”
    games = {}
    for i in range(n_games):
        for p in 'ABC':
            games[p, i] = Int(f'{p}_rank_{i}')
            solver.add(games[p, i] >= 1, games[p, i] <= 3)
        solver.add(Distinct(games['A', i], games['B', i], games['C', i]))

    def score(p):
        """p 的总得分：按名次加上 X、Y、Z"""
        return Sum([If(games[p, i] == 1, X, If(games[p, i] == 2, Y, Z))
                    for i in range(n_games)])

    solver.add(score('A') == 22)
    solver.add(score('B') == 9)
    solver.add(score('C') == 9)
    solver.add(games['B', 0] == 1)   # 第 0 个项目（标枪）中 B 是第 1 名

    if solver.check() != sat:
        print(f"项目数 {n_games}: 无解")
        return False

    m = solver.model()
    print(f"项目数 {n_games}: 第1名={m[X]}分, 第2名={m[Y]}分, 第3名={m[Z]}分")

    ranks = {p: [m[games[p, i]].as_long() for i in range(n_games)] for p in 'ABC'}
    for i in range(n_games):
        name = '标枪' if i == 0 else f'项目{i}'
        print('  ' + name + ': ' + ', '.join(f'{p}=第{ranks[p][i]}名' for p in 'ABC'))
    return True


for n in range(2, 10):
    if try_solve(n):
        break

项目数 2: 无解
项目数 3: 无解
项目数 4: 无解
项目数 5: 第1名=5分, 第2名=2分, 第3名=1分
  标枪: A=第2名, B=第1名, C=第3名
  项目1: A=第1名, B=第3名, C=第2名
  项目2: A=第1名, B=第3名, C=第2名
  项目3: A=第1名, B=第3名, C=第2名
  项目4: A=第1名, B=第3名, C=第2名

竞赛数为 2、3、4 时都没有解，到 5 项竞赛才首次解出，此时的分数为第 1 名 5 分、第 2 名 2 分、第 3 名 1 分，即每项竞赛 8 分，5 项共 40 分，恰好等于 22+9+9。

再看名次，A 在标枪以外的 4 项竞赛中都是第 1 名，B 在这 4 项中都是第 3 名，而 C 都是第 2 名，因此 100 米赛跑的第 2 名是 C。

用 If 可以写成名次为 1 时取 X、为 2 时取 Y、其余取 Z，缺点是嵌套一深就不易读。三个名次只需要两层嵌套；名次再多，嵌套层数就跟着增加，读到某一层对应哪个名次会越来越吃力。

用 Function 改写#

由名次到分数的转换，也可以用 Function() 作为表交给 Z3。嵌套的 If 消失之后，代码也随之变短。两者表达的是同一个映射，区别只在约束的形式：一组等式，还是一串条件。

score_func = Function('score', IntSort(), IntSort())

各个参数的含义如下。

  • 'score'：函数的名字，供显示用

  • 最后的 IntSort()：返回值的类型

  • 中间的 IntSort()：参数的类型

名次与分数都是整数，因此两者都取 IntSort()。

接着把第 1 名取 X 分、第 2 名取 Y 分、第 3 名取 Z 分这个对应关系作为约束追加进去。

solver.add(
    score_func(1) == X,
    score_func(2) == Y,
    score_func(3) == Z,
)

这样 score_func(名次) 就得到对应的分数。与 If 的写法相比，多的是一条函数声明与三条等式，少的是逐层嵌套。

def try_solve(n_games):
    """用 Function 重写的版本"""
    X, Y, Z = Ints('X Y Z')
    solver = Solver()
    solver.add(X > Y, Y > Z, Z > 0)

    # 把名次 → 得分 的对应关系当作函数持有
    score_func = Function('score', IntSort(), IntSort())
    solver.add(score_func(1) == X, score_func(2) == Y, score_func(3) == Z)

    games = {}
    for i in range(n_games):
        for p in 'ABC':
            games[p, i] = Int(f'{p}_rank_{i}')
            solver.add(games[p, i] >= 1, games[p, i] <= 3)
        solver.add(Distinct(games['A', i], games['B', i], games['C', i]))

    def score(p):
        return Sum([score_func(games[p, i]) for i in range(n_games)])

    solver.add(score('A') == 22)
    solver.add(score('B') == 9)
    solver.add(score('C') == 9)
    solver.add(games['B', 0] == 1)

    if solver.check() != sat:
        print(f"项目数 {n_games}: 无解")
        return False

    m = solver.model()
    print(f"项目数 {n_games}: 第1名={m[X]}分, 第2名={m[Y]}分, 第3名={m[Z]}分")

    ranks = {p: [m[games[p, i]].as_long() for i in range(n_games)] for p in 'ABC'}
    for i in range(n_games):
        name = '标枪' if i == 0 else f'项目{i}'
        print('  ' + name + ': ' + ', '.join(f'{p}=第{ranks[p][i]}名' for p in 'ABC'))

    # 从模型里取出函数本身，就能看到定义好的对应关系
    print('  score_func:', m[score_func])
    return True


for n in range(2, 10):
    if try_solve(n):
        break

项目数 2: 无解
项目数 3: 无解

项目数 4: 无解
项目数 5: 第1名=5分, 第2名=2分, 第3名=1分
  标枪: A=第2名, B=第1名, C=第3名
  项目1: A=第1名, B=第3名, C=第2名
  项目2: A=第1名, B=第3名, C=第2名
  项目3: A=第1名, B=第3名, C=第2名
  项目4: A=第1名, B=第3名, C=第2名
  score_func: [1 -> 5, 3 -> 1, else -> 2]

用 m[score_func] 可以取出函数的内容，显示出来的 [1 -> 5, 3 -> 1, else -> 2] 表示第 1 名 5 分、第 3 名 1 分、其余即第 2 名 2 分，这份表可以逐项核对。Z3 只列出必须区分的取值，剩下的用 else 概括，因此表比逐项列举要短。

小结#

结果

竞赛数

2、3、4 无解，5 项竞赛时才有解

分数

第 1 名 5 分、第 2 名 2 分、第 3 名 1 分，满足 X > Y > Z > 0

100 米赛跑的第 2 名

C，因为 C 在标枪以外的所有竞赛中都是第 2 名

  • 未知的个数放在外层循环里由小到大试

  • 由名次到分数的转换，用 If 与 Function 都能写。表一旦变大，Function 更易读

  • 用 m[函数] 可以确认模型所决定的函数内容