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 的题目数与答案为其他选项的题目数
组合数目很多：10 道题各 5 个选项，直接穷举有 \(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 时 a 的个数为 0，答案为 b 时为 1，这些对应关系一并追加。

Q10 问的是本题的答案，无论选哪个选项都不矛盾，由于它只指向自身，因此不追加约束。

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，只有这一种。

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 的倍数，因此没有算入。

可以用反证的方式确认上面的唯一性：追加一条禁止该答案的约束，再调用一次 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，加入两条约束。

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 落在 1〜2 时要求 y 落在 3〜4，反之亦然，每种情形各有 4 种组合。

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, [...]) 就能把选项与条件的对应写成一行：两个列表长度相同，按位置配成五对，顺序不能错开。顺序一旦错开，选项与条件就会跨项配对，约束仍能求解，但解的语义已经错了。

小结#

自指谜题只要把各题的答案设为变量，就变成了普通的约束问题
若答案为某某则这样的条件用 Implies() 写出，按选项的个数逐个列出
计数时写 Sum([x == ans for x in q.values()])，绝对值用 Abs，属于其中某个用 Or，这些都可以作为约束使用
穷举需要 976 万种，写成约束之后 Z3 一瞬间就能解出

10 个问题的谜题：用 Implies 解自指的选择题

目录

10 个问题的谜题：用 Implies 解自指的选择题#

本章的内容#

问题#

难点在哪里#

思路#

什么是 Implies#

小结#