運動会問題

運動会問題#

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 を参考にしました。

from z3 import *

難点#

この問題の難しさは、以下の点にあります。

競技数が不明
各者の合計得点が与えられているが、何競技行われたのかはわからない。
X, Y, Z の制約が曖昧
各順位の得点が X > Y > Z > 0 という制約があるが、具体的な値は不明。
各競技の順位が不明
各競技で誰が 1位, 2位, 3位だったかは与えられていない。
ただし、B が槍投げで 1位だったことは分かっている。

コード#

次のコードを使うことで、この問題を解くことができます。

def try_solve(N_game):
    X = Int('X')
    Y = Int('Y')
    Z = Int('Z')
    
    s = Solver()
    s.add(X > Y, Y > Z, Z > 0)
    
    games = {}
    
    def score(p):
        return Sum(
            [If(games[p, i] == 1, X, If(games[p, i] == 2, Y, Z)) for i in range(N_game)]
        )
    
    for i in range(N_game):
        A_rank = Int(f'A_rank_{i}')
        B_rank = Int(f'B_rank_{i}')
        C_rank = Int(f'C_rank_{i}')
        s.add(A_rank >= 1, A_rank <= 3)
        s.add(B_rank >= 1, B_rank <= 3)
        s.add(C_rank >= 1, C_rank <= 3)
        s.add(Distinct(A_rank, B_rank, C_rank))
        games['A', i] = A_rank
        games['B', i] = B_rank
        games['C', i] = C_rank
    
    s.add(score('A') == 22)
    s.add(score('B') == 9)
    s.add(score('C') == 9)
    s.add(games['B', 0] == 1)

    if s.check() == sat:
        m = s.model()
        print(f'X = {m[X]}')
        print(f'Y = {m[Y]}')
        print(f'Z = {m[Z]}')
        
        members = ['A', 'B', 'C']
        res = {p:[m[games[p, i]].as_long() for i in range(N_game)] for p in members}
        print(res)
        return True
    else:
        return False

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

X = 5
Y = 2
Z = 1
{'A': [2, 1, 1, 1, 1], 'B': [1, 3, 3, 3, 3], 'C': [3, 2, 2, 2, 2]}

説明#

このコードでは、まず try_solve(N_game) を用意し、N_game（競技数）を 2 から順番に試して、最初に解が得られる競技数を見つける という手法を使います。

games は (人, 競技) のペアをキーとして、順位を表す Z3 変数を管理する辞書 です。各順位変数は 1以上3以下 の整数 (>=1 かつ <=3) をとり、また 同じ競技における3人の順位はすべて異なる (Distinct) という制約が課されています。

score 関数は、各競技における順位を基に、特定の人（A, B, C）の合計得点を計算するために使用されます。具体的には、各競技でその人が1位、2位、3位のいずれかになった場合に、その順位に応じた得点（X, Y, Z）を加算していきます。この関数は、指定された人物（p）の競技ごとの得点の合計を計算します。具体的には次のような処理が行われています：

games[p, i]

ここでは、games 辞書から p（人物）のi番目の競技における順位 を取り出します。たとえば、games['A', 0] はAの最初の競技（0番目）の順位です。

If(games[p, i] == 1, X, If(games[p, i] == 2, Y, Z))

ここで順位に応じて得点を決定します。

games[p, i] == 1 の場合は 1位なので得点は X。
games[p, i] == 2 の場合は 2位なので得点は Y。
それ以外（つまり、games[p, i] == 3 の場合）は 3位なので得点は Z。

この部分が If 関数を使用して順位に応じた得点を決めるロジックです。

If は 条件分岐 を実現する Z3 の関数です。次のように使います：

If(condition, value_if_true, value_if_false)

condition が真の場合、value_if_true が返されます。
condition が偽の場合、value_if_false が返されます。

Sum(...)

Sum はリスト内の全ての得点を加算して、合計得点を計算します。[ ... for i in range(N_game)] で すべての競技（N_game は競技数）について繰り返し処理を行い、各競技の得点を加算していきます。

Functionでの改善#

上のコードでは、ネストされた If 関数を使って順位から点数に変換しています。このような変換は、ケースが多くなると式が複雑になります。この場合、Function() を使って値のマッピングを表現することができます。次のコードでは、Z3 の関数 score_func を次のように定義します。最初の引数は関数名、最後の引数は関数の戻り値の型、真ん中の引数は関数の引数の型です。順位から点数に変換する関数の引数と戻り値はすべて IntSort() で表される整数型です。

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

次に、関数の値のマッピング制約条件を Solver に追加します。

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

score() 関数内では、score_func(games[p, i]) を使って順位から点数に変換することができます。又、m[score_func] を使うことで、関数の中身（つまり、関数の評価結果）を取得することができます。

def try_solve(N_game):
    X = Int('X')
    Y = Int('Y')
    Z = Int('Z')
    
    s = Solver()
    s.add(X > Y, Y > Z, Z > 0)
    
    games = {}
    
    score_func = Function('score', IntSort(), IntSort())
    s.add(
        score_func(1) == X,
        score_func(2) == Y,
        score_func(3) == Z,
    )
    
    def score(p):
        return Sum(
            [score_func(games[p, i]) for i in range(N_game)]
        )
    
    for i in range(N_game):
        A_rank = Int(f'A_rank_{i}')
        B_rank = Int(f'B_rank_{i}')
        C_rank = Int(f'C_rank_{i}')
        s.add(A_rank >= 1, A_rank <= 3)
        s.add(B_rank >= 1, B_rank <= 3)
        s.add(C_rank >= 1, C_rank <= 3)
        s.add(Distinct(A_rank, B_rank, C_rank))
        games['A', i] = A_rank
        games['B', i] = B_rank
        games['C', i] = C_rank
    
    s.add(score('A') == 22)
    s.add(score('B') == 9)
    s.add(score('C') == 9)
    s.add(games['B', 0] == 1)
    
    if s.check() == sat:
        m = s.model()
        print(f'X = {m[X]}')
        print(f'Y = {m[Y]}')
        print(f'Z = {m[Z]}')
        
        members = ['A', 'B', 'C']
        res = {p:[m[games[p, i]].as_long() for i in range(N_game)] for p in members}
        print(res)
        print(m[score_func])
        return True
    else:
        return False

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

X = 5
Y = 2
Z = 1
{'A': [2, 1, 1, 1, 1], 'B': [1, 3, 3, 3, 3], 'C': [3, 2, 2, 2, 2]}
[2 -> 2, 3 -> 1, else -> 5]

運動会問題

Contents

運動会問題#

難点#

コード#

説明#

Functionでの改善#