10個の質問パズル ― 自己参照クイズを Implies で解く

10個の質問パズル ― 自己参照クイズを Implies で解く#

この章で学ぶこと#

10個の質問が、お互いの答えを参照しているパズルを解きます。

各質問の答えを 1〜5 の整数変数で表す
「答えが○○なら、この条件が成り立つ」を Implies() で書く
全探索では 5¹⁰ ≈ 976万通りになる問題を、制約として書き下す

Implies()（含意）の使い方がこの章の中心です。

問題#

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

どこが難しいか#

条件が互いに依存している：Q3 の答えは別の質問の答えと一致しなければならず、Q6 の条件は「a の答えの個数」と「他の答えの個数」の比較です。
組み合わせが多い：1問5択が10問なので、素直に全探索すると \(5^{10} = 9{,}765{,}625\) 通りになります。
普通の等式ではない条件がある：Q7 は答えの差の絶対値、Q9 は答えの個数が素数・平方数・階乗数・5の倍数のどれか、という条件です。

人手では手に負えないので、条件をそのまま Z3 に渡します。

方針#

質問 \(i\) の答えを、整数変数 q[i] で表します。値は 1〜5 で、1=a、2=b、3=c、4=d、5=e です。

各質問は「もし Q_i の答えが○○なら、この条件が成り立つ」という形をしています。これは Implies() そのものです。たとえば Q4 は

solver.add([Implies(q[4] == ans, count_a() == value) for ans, value in zip(choices, [0, 1, 2, 3, 4])])

と書けます。「Q4 の答えが a(1) なら、a の個数は 0」「b(2) なら 1」…をまとめて追加しています。

Q10「この問題の答えは？(a)a (b)b …」は、どの選択肢を選んでも矛盾しません（自分自身を指しているだけだから）。そこで制約は追加しません。

from z3 import *

# 選択肢 a〜e を整数 1〜5 で表す（Z3 の変数ではなく、ただの番号）
a, b, c, d, e = range(1, 6)
choices = [a, b, c, d, e]

# 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(1 <= x, x <= 5)


def first_b(idx):
    """「最初に b が正解になるのは質問 idx」という条件"""
    return And([q[i] != b for i in range(1, idx)] + [q[idx] == b])


def only_equals(idx):
    """「隣り合って同じ答えになるのは idx と idx+1 の組だけ」という条件"""
    return And([q[i] == q[i + 1] if i == idx else q[i] != q[i + 1]
                for i in range(1, 10)])


def count_answer(ans):
    """答えが ans である質問の数"""
    return Sum([x == ans for x in q.values()])


def is_in(expr, values):
    """expr が values のどれかに等しい"""
    return Or([expr == v for v in values])


# Q1: 最初に b が正解になる質問
solver.add([Implies(q[1] == ans, first_b(idx)) for ans, idx in zip(choices, [2, 3, 4, 5, 6])])

# Q2: 唯一、隣り合って同じ答えになる組
solver.add([Implies(q[2] == ans, only_equals(idx)) for ans, idx in zip(choices, [2, 3, 4, 5, 6])])

# Q3: この質問と同じ答えの質問
solver.add([Implies(q[3] == ans, q[3] == q[idx]) for ans, idx in zip(choices, [1, 2, 4, 7, 6])])

# Q4: a の個数
solver.add([Implies(q[4] == ans, count_answer(a) == value) for ans, value in zip(choices, [0, 1, 2, 3, 4])])

# Q5: この質問と同じ答えの質問
solver.add([Implies(q[5] == ans, q[5] == q[idx]) for ans, idx in zip(choices, [10, 9, 8, 7, 6])])

# Q6: a の個数が、どの答えの個数と同じか
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: この質問と次の質問の答えは、アルファベット順で何文字違うか
solver.add([Implies(q[7] == ans, Abs(q[7] - q[8]) == diff) for ans, diff in zip(choices, [4, 3, 2, 1, 0])])

# Q8: 母音（a, e）の個数
solver.add([Implies(q[8] == ans, count_answer(a) + count_answer(e) == value)
            for ans, value in zip(choices, [2, 3, 4, 5, 6])])

# Q9: 子音（b, c, d）の個数が、素数・階乗数・平方数・立方数・5の倍数のどれか
consonants = count_answer(b) + count_answer(c) + count_answer(d)
solver.add([Implies(q[9] == ans, is_in(consonants, values)) for ans, values in
            zip(choices, [[2, 3, 5, 7],      # 素数
                          [1, 2, 6],         # 階乗数 (1!, 2!, 3!)
                          [1, 4, 9],         # 平方数
                          [1, 8],            # 立方数
                          [5, 10]])])        # 5の倍数

# Q10 は自己参照なので制約を追加しない

if solver.check() == sat:
    m = solver.model()
    answers = [m[q[i]].as_long() for i in range(1, 11)]
    print("答え:", "".join("abcde"[v - 1] for v in answers))
    for i, v in enumerate(answers, 1):
        print(f"Q{i} = {'abcde'[v - 1]}")
else:
    print("解なし")

答え: cdebeedcba
Q1 = c
Q2 = d
Q3 = e
Q4 = b
Q5 = e
Q6 = e
Q7 = d
Q8 = c
Q9 = b
Q10 = a

答えは cdebeedcba の1通りだけでした。

Q1	Q2	Q3	Q4	Q5	Q6	Q7	Q8	Q9	Q10
c	d	e	b	e	e	d	c	b	a

Q9 の「5の倍数」は 5 と 10 です（1 は5の倍数ではないので入れていません）。

解が1つしかないことは、見つけた答えを禁止する制約を足して、もう一度 check() すれば確かめられます（unsat なら他の答えはありません）。

Implies とは#

Implies(P, Q) は**「P が真ならば Q も真」**という条件です。Z3 では

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

と同じ意味になります。

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

P が偽なら、Q が何であっても全体は真です（偽からは何でも導ける、という論理の決まりです）。
P が真で Q が偽のときだけ、全体が偽になります。

この性質のおかげで、「特定の条件のときだけ別の条件を適用する」という書き方ができます。

小さい例で確かめてみます。x と y は 1〜4 で、次の2つの制約を置きます。

Implies(x >= 3, y <= 2) … x が 3 か 4 なら、y は 1 か 2
Implies(x <= 2, y >= 3) … x が 1 か 2 なら、y は 3 か 4

`x`	`y` の取り得る値
1, 2	3, 4
3, 4	1, 2

組み合わせは \(2 \times 2 \times 2 = 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([d() != m[d] for d in m]))   # 見つけた解を禁止して次の解を探す

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

8通りの解がすべて出ました。Implies が「条件付きの制約」として働いていることが分かります。

なお、このパズルのように選択肢ごとに条件が変わる問題では、Implies を選択肢の数だけ並べるのが定石です。zip(choices, [...]) を使うと、選択肢と条件の対応が1行で書けます。

まとめ#

自己参照パズルは「各質問の答えを変数にする」だけで、普通の制約問題に変わる
「答えが○○なら…」は Implies() で書く。選択肢の数だけ並べる
数え上げ（Sum([x == ans for x in q.values()])）や絶対値（Abs）、「どれかに含まれる」（Or）も制約として使える
全探索なら 976万通り、制約として書けば Z3 が一瞬で解く