運動会の得点パズル ― 競技数が分からない問題を解く

運動会の得点パズル ― 競技数が分からない問題を解く#

この章で学ぶこと#

この章の問題は、何競技行われたのか分からないという点が厄介です。こんなときは、競技数を 2, 3, 4, … と小さい順に試して、最初に解けたものを答えにします。

  • 分からない数を、外側のループで総当たりする

  • 順位から得点への変換（If と Function の2通り）

  • 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 にそのまま変数として持たせて、条件だけを書けばよくなります。競技数だけは変数の数が変わるので、ループで試します。

競技数を変えながら解く#

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点（1競技あたり8点、5競技で40点＝22+9+9）です。

順位を見ると、A は槍投げ以外の4競技で1位、B は槍投げ以外で3位、そして C は槍投げ以外のすべての競技で2位 です。つまり 100メートル走の2位は C です。

If を使うと「もし順位が1なら X、2なら Y、それ以外なら Z」と書けます。ネストが深くなると読みにくくなるのが難点です。

Function で書き直す#

順位から得点への変換は、Function() で「表」として持たせることもできます。ネストした 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(順位) が得点になります。

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 が作った表を、そのまま確認できます。

まとめ#

結果

競技数

2, 3, 4 は解なし。5競技で解ける

得点

1位 5点、2位 2点、3位 1点（X > Y > Z > 0 を満たす）

100メートル走の2位

C（C は槍投げ以外のすべての競技で2位）

  • 分からない「個数」は、外側のループで小さい順に試す

  • 順位→得点の変換は If でも Function でも書ける。表が大きくなるなら Function が読みやすい

  • m[関数] で、モデルが決めた関数の中身を確認できる