10個の問題

1. 最初に「b」が正解となる問題はどれか？
（a）2；（b）3；（c）4；（d）5；（e）6

2. 唯一連続して同じ答えになる問題の組み合わせは？
（a）2，3；（b）3，4；（c）4，5；（d）5，6；（e）6，7；

3. この問題の答えと同じ答えの問題はどれか？
（a）1；（b）2；（c）4；（d）7；（e）6

4. 答えが「a」の問題の数はいくつか？
（a）0；（b）1；（c）2；（d）3；（e）4

5. この問題の答えと同じ答えの問題はどれか？
（a）10；（b）9；（c）8；（d）7；（e）6

6. 答えが「a」の問題の数は、どの答えの問題の数と同じか？
（a）b；（b）c；（c）d；（d）e；（e）以上のどれでもない

7. アルファベット順で、この問題の答えと次の問題の答えは何文字違うか？
（a）4；（b）3；（c）2；（d）1；（e）0。（※aとbは1文字違い）

8. 答えが母音字（a, e）である問題の数はいくつか？
（a）2；（b）3；（c）4；（d）5；（e）6。（※母音字はaとe）

9. 答えが子音字（b, c, d）である問題の数は？
（a）素数；（b）階乗数；（c）平方数；（d）立方数；（e）5の倍数

10. この問題の答えは？
（a）a；（b）b；（c）c；（d）d；（e）e

難点の分析

この問題は、10個の問題とそれぞれ5つの選択肢（A～E）がある一種の自己参照パズルです。各問題の回答が他の問題の回答に依存しており、相互に制約を形成するため、直感的に解くのが困難です。特に難しい点としては：

• 条件の相互依存性

  • 例えば、Q3の回答は他の特定の問題の回答と一致しなければならない。

  • Q6の条件は、Aの回答数が特定の別の回答数と等しくなるという制約を持つ。

  • Q9は、特定の数（素数や平方数など）に回答数が一致する必要がある。

• 組み合わせの爆発的増加

  • 各問題に5つの選択肢があるため、単純な全探索では (5^{10} = 9,765,625) 通りの組み合わせを考える必要があり、計算量が膨大。

• 非線形性の導入

  • Q7のように、アルファベット順の距離を考慮した制約（絶対値）を含む。

  • Q9のように、回答の個数が特定の数学的条件（素数、平方数、階乗数など）を満たす必要がある。

これらの点を考慮すると、単純な探索では解くのが難しく、Z3のような制約ソルバーを使って系統的に解くのが有効です。次はフールソースコードです。

from z3 import *

# 選択肢 A, B, C, D, E を整数 1〜5 で表す
answers = A, B, C, D, E = range(1, 6)

# 10 個の問題に対応する整数変数を作成
q = {i: Int(f'q{i}') for i in range(1, 11)}
solver = Solver()

# すべての解答は 1 以上 5 以下（A〜E のいずれか）である必要がある
for x in q.values():
    solver.add((x >= 1) & (x <= 5))

# ある質問の最初に B が出現する位置を決める関数
def first_b(idx):
    expressions = []
    for i in range(1, idx):  # idx より前のすべての質問で B でないことを確認
        expressions.append(q[i] != B)
    expressions.append(q[idx] == B)  # idx の位置では B である必要がある
    return And(expressions)

# ある特定のインデックスだけが隣と等しく、他は異なる制約を作成
def only_equals(idx):
    expressions = []
    for i in range(1, 10):
        if i == idx:
            expressions.append(q[i] == q[i + 1])  # idx の位置だけが次と等しい
        else:
            expressions.append(q[i] != q[i + 1])  # 他の部分はすべて異なる
    return And(expressions)

# 特定の解答の出現回数をカウント
def count_answer(ans):
    return Sum([x == ans for x in q.values()])
    
# A の出現回数が指定値と等しいことを保証
def count_a_equals(value):
    return count_answer(A) == value

# ある値がリストに含まれるかチェックするヘルパー関数
def is_in(e, values):
    return Or([e == v for v in values])

# Q1 の解答によって B が最初に現れる位置を決める
solver.add(
    [Implies(q[1] == ans, first_b(idx)) for ans, idx in zip(answers, [2, 3, 4, 5, 6])]
)

# Q2 の解答によって、指定のインデックスだけが隣と等しくなるように制約を追加
solver.add(
    [Implies(q[2] == ans, only_equals(idx)) for ans, idx in zip(answers, [2, 3, 4, 5, 6])]
)

# Q3 の解答によって、Q3 が特定のインデックスと等しくなる制約を追加
solver.add(
    [Implies(q[3] == ans, q[3] == q[idx]) for ans, idx in zip(answers, [1, 2, 4, 7, 6])]
)

# Q4 の解答によって、A の出現回数を制約
solver.add(
    [Implies(q[4] == ans, count_a_equals(idx)) for ans, idx in zip(answers, [0, 1, 2, 3, 4])]
)

# Q5 の解答によって、Q5 が特定のインデックスと等しくなる制約を追加
solver.add(
    [Implies(q[5] == ans, q[5] == q[idx]) for ans, idx in zip(answers, [10, 9, 8, 7, 6])]
)

# Q6 の解答によって、特定の解答の出現回数を制約
solver.add(
    Implies(q[6] == A, count_answer(A) == count_answer(B)),
    Implies(q[6] == B, count_answer(A) == count_answer(C)),
    Implies(q[6] == C, count_answer(A) == count_answer(D)),
    Implies(q[6] == D, count_answer(A) == count_answer(E)),
    Implies(q[6] == E, And(
        count_answer(A) != count_answer(B),
        count_answer(A) != count_answer(C),
        count_answer(A) != count_answer(D),
        count_answer(A) != count_answer(E),
    ))    
)

# Q7 の解答によって、Q7 と Q8 の差を制約
solver.add(
    [Implies(q[7] == ans, Abs(q[7] - q[8]) == val) for ans, val in zip(answers, [4, 3, 2, 1, 0])]
)

# Q8 の解答によって、A と E の合計出現回数を制約
count_ae = count_answer(A) + count_answer(E)
solver.add(
    [Implies(q[8] == ans, count_ae == val) for ans, val in zip(answers, [2, 3, 4, 5, 6])]
)

# Q9 の解答によって、B, C, D の合計出現回数を特定の値のいずれかにする
count_bcd = count_answer(B) + count_answer(C) + count_answer(D)
solver.add(
    [Implies(q[9] == ans, is_in(count_bcd, vals)) for ans, vals in 
         zip(answers, [[2, 3, 5, 7], [1, 2, 6], [1, 4, 9], [1, 8], [1, 5, 10]])]
)

# 制約を満たす解を求める
solver.check()
m = solver.model()

# 解を A〜E の文字に変換して出力
for i, x in q.items():
    print(f"Q{i} = {'ABCDE'[int(str(m[x])) - 1]}")

Q1 = C
Q2 = D
Q3 = E
Q4 = B
Q5 = E
Q6 = E
Q7 = D
Q8 = C
Q9 = B
Q10 = A

コードの解析

このコードでは、Implies() を使用して、各問題の答えが特定の値である場合に成立する制約を作成しています。Implies() は「論理含意（implication）」を表し、形式的には次のような意味を持ちます。

\[ \text{Implies}(P, Q) \]

これは 「もし P が真ならば、Q も真である」 という条件を表します。

Z3 では、Implies(P, Q) は以下の論理式と等価です。

\[ \neg P \vee Q \]

これは 「P が偽であるか、Q が真である」 ことを意味します。Implies(P, Q) の真理値表以下のようです。

\( P \)	\( Q \)	\( \text{Implies}(P, Q) \equiv \neg P \vee Q \)
False	False	True
False	True	True
True	False	False
True	True	True

Implies(P, Q) は 「もし P が真ならば Q も真である」 ことを意味します。

• P が False の場合、Q の値に関係なく True となります。（これは、偽からは何でも導ける という論理法則に基づいています。）

• P が True で Q が False のときだけ Implies(P, Q) は False になります。

この性質を活用することで、Z3 において「特定の条件を満たすときにのみ別の条件を適用する」制約を作成することができます。

次のコードでは、Implies を使って x の値によって y の値に制約を加えています。

• Implies(x >= 3, y <= 2)

  • 「もし x >= 3 ならば y <= 2」という制約。

  • x が 3 または 4 のとき、y は 1 または 2 でなければならない。

• Implies(x <= 2, y >= 3)

  • 「もし x <= 2 ならば y >= 3」という制約。

  • x が 1 または 2 のとき、y は 3 または 4 でなければならない。

制約 Implies(x >= 3, y <= 2) と Implies(x <= 2, y >= 3) により、x と y の組み合わせは以下のようになります。

x の範囲	制約	y の取り得る値
x >= 3	y <= 2	1, 2
x <= 2	y >= 3	3, 4

その結果、出力される解はの 8 通りになります。

x, y = Ints('x y')
s = Solver()
s.add(1 <= x, x <= 4)
s.add(1 <= y, y <= 4)
s.add(Implies(x >= 3, y <= 2))
s.add(Implies(x <= 2, y >= 3))

while s.check() == sat:
    m = s.model()
    print(m)
    s.add(Or([v() != m[v] for v in m]))

[x = 3, y = 1]
[x = 4, y = 2]
[x = 4, y = 1]
[x = 2, y = 3]
[x = 2, y = 4]
[x = 1, y = 4]
[x = 1, y = 3]
[x = 3, y = 2]