一类猜数问题的解法

Table of Contents

背景

今天雨荷向我分享了一道知乎上的问题1,这类问题的通用设定是:

  1. 有一群人,大家有一定的共识,但是每个人只能看到部分的全局信息。
  2. 每个人在对当前的环境观察经过推理之后进行一个行为,这个行为所有人可见。

通常的问题形式为:

  1. 预测在某个轮数之后的状态。
  2. 给定某个轮数之后的状态,预测初始状态。

这类问题广泛地出现在中学的数学竞赛中,手动推理有一定的脑力负担,这里试图给一个能够暴力搜索求解的通用模板。

红眼睛蓝眼睛

问题描述

在我个人的认知中,此类问题最早由陶哲轩的博客2 推广至大众,问题设定如下:

  • 岛上有1000个人,100个人为蓝眼睛,900人为红眼睛(岛民不知道岛上有多少蓝眼睛)。
  • 假设每个岛民都拥有足够强的推理能力。
  • 岛民不能互相交流,也不能看到自己眼睛颜色,但可以看到别人眼睛的颜色。
  • 每个人在知道自己眼睛颜色的当天夜里会自杀。

所有岛民都相安无事地生活着,但是有一天有一个旅行者告诉大家:你们当中有蓝眼睛。请问接下来会发生什么。

解法

答案是前99天无事发生,然后第100天所有蓝眼睛自杀,随后红眼睛全部自杀,原因如下:

  1. 如果岛上只有一个蓝眼睛,那么他第一天晚上会自杀,因为他发现了自己是蓝眼睛。
  2. 如果岛上有两个蓝眼睛,那么第一天无人自杀,因为他们都无法确定自己眼睛的颜色,但是在第2天,他们都会自杀,因为他们发现另外一个蓝眼睛没有在第一天自杀,因此对方都不是唯一的蓝眼睛。
  3. 如果岛上有 \(k\) 个蓝眼睛,那么前 \(k\) 天都不会有人自杀,但是在第 \(k\) 天,他们发现在 \(k-1\) 天无人自杀之后可以确定自己的眼睛颜色,因此在第 \(k\) 天自杀。

那么这位旅行者带来了什么额外信息呢?这个信息不是大家都知道吗?

实际上并不是,在岛上只有一个蓝眼睛的情况下,这位蓝眼睛是不知道岛上有蓝眼睛的。 在岛上有两个蓝眼睛的情况下,其中一个蓝眼睛是不知道另一位蓝眼睛知道岛上有蓝眼睛,因此彼此都没有自杀。 以此类推……

此类问题的通用解法是:每一轮大家的行为都蕴含着一定信息量,用前一轮大家的行为来剪枝掉当前可能的状态集合,结合问题的设定中的共有知识来确定下一轮大家的行为。

补注

这个问题被广泛地用于解释mutual knowledge和common knowledge的区别。 前者的定义为:人群中的每一个人都知道这个命题 \(p\) : \(\forall i, \mathrm{Know}_{i}(p)\) 后者的定义为:

  1. \(\mathrm{Know}_{i}^{0}(p) = \mathrm{Know}_{i}(p)\)
  2. \(\mathrm{Know}_{i}^{k}(p) = \mathrm{Know}_{i}(\forall j, \mathrm{Know}^{k-1}_{j}(p))\)
  3. Common Knowledge即对一个命题 \(p\) 有 \(\forall i, \wedge_{k=0}^{\infty} \mathrm{Know}_{i}^{k}(p)\)

首长在大一的时候曾经用这个例子来说明为什么要有gfw,有的事情可能大家都知道,但是彼此都知道彼此知道这件事情又是另一回事。

猜数

问题描述

有三个足够聪明的学生,每个人头上有一个正整数,其中一个数为另外两个数的和,每个人能看见其它人头上的数,但看不见自己的(这些信息是公共知识)。 轮流问每个学生是否能猜出自己头上的数:

  • 学生1:不能
  • 学生2:不能
  • 学生3:不能
  • 学生1:不能
  • 学生2:不能
  • 学生3:能,是144

要求反推出学生1和学生2头上的数。

解法

很显然,每个学生的反应对其它学生而言都带来了新的信息,因为每个学生实际上只有两种选择:另外两个学生头上的数之和或者之差,我们可以在这两种情况下分别带入之前的学生的视角,如果不能重复之前学生所做的选择,就可以排除当前选项。

假设三个数为 \(x, y, z\) ,其中 \(x + y = z\) 且 \(x \leq y < z\) 。 我们可以推理得出,一定是 \(z\) 先被推理出来,原因在后面会提到。

因此令 \(z=144\), 搜索 \(x\in [1, 64)\) 和 \(y=144-x\) , 验证逻辑链是否合法。

验证算法是一个递归算法:

  1. 如果当前三个数中有一个不大于0,当前行为链非法。
  2. 如果行为链长度为0,则合法。
  3. 假设另外两个数是 \(x\) 和 \(y\) , 当前数为 \(z\) ,那么将 \(z = x + y\) 和 \(z=\max(\{x, y\}) - \min(\{x, y\})\) 带入历史的行为链进行验证。
    1. 如果当前学生预测是:能猜出。如果两个 \(z\) 对应的行为链其中只有一个合法,那么当前行为链合法(因为能唯一确定 \(z\) 是什么),否则不合法。
    2. 如果当前预测是:不能猜出。那么两个 \(z\) 对应的行为链其中只有一个合法,那么当前行为链不合法,否则合法。

我的大脑可以用来逻辑推理的栈深度比较低,因此用程序模拟该过程(经雨荷提醒,该问题手推的搜索空间也不算很大)。

# guess game
# x + y = z
# x <= y < z
# suppose z=144

from typing import Tuple, List


class Trace:
    """Record logical inference trace"""

    def __init__(self, number, who, pred, valid, clues=None) -> None:
        self._number = number
        self._who = who
        self._pred = pred
        self._valid = valid
        if clues is None:
            self._clues = []
        else:
            self._clues = clues

    def tostring(self, indent_level=0) -> str:
        ret = "    " * indent_level
        ret += "{}, {}, pred={}, valid={}\n".format(
            self._number, self._who, self._pred, self._valid)
        ret += "".join([clue.tostring(indent_level=indent_level+1)
                       for clue in self._clues])
        return ret

    def __str__(self) -> str:
        return self.tostring()


def other_two(number: List[int], exclude: int) -> List[int]:
    return list(_ for i, _ in enumerate(number) if i != exclude)


def is_valid(number: List[int]) -> bool:
    return all(_ > 0 for _ in number)


def replace_idx_with_val(arr, index, val) -> List[int]:
    ret = arr.copy()
    ret[index] = val
    return ret


def verify(number: List[int], history: List[Tuple[int, bool]]):
    """verify whether the guessing history is valid"""
    if not is_valid(number):
        return False, Trace(number, "god", None, False)
    if len(history) == 0:
        return True, Trace(number, "god", None, True)
    me, pred = history[-1]
    x, y = other_two(number, me)
    valid0, trace0 = verify(replace_idx_with_val(
        number, me, x + y), history[:-1])
    valid1, trace1 = verify(replace_idx_with_val(
        number, me, max(x, y) - min(x, y)), history[:-1])
    if pred:
        valid = False
        if valid0 != valid1:
            valid = True
    else:
        valid = True
        if valid0 != valid1:
            valid = False
    return valid, Trace(number, "player-{}".format(me), pred, valid, clues=[trace0, trace1])


if __name__ == "__main__":
    for i in range(72):
        for order in [[0, 1, 2], [1, 0, 2]]:
            j = 144 - i
            valid, trace = verify([i, j, 144], [
                (order[0], False), (order[1], False), (order[2], False), (order[0], False), (order[1], False), (order[2], True)])
            if valid:
                print(i, j, 144)
                print(trace)

一共搜索出五组解: \((32,112,144)\) , \((36,108,144)\) , \((48,96,144)\) , \((54,90,144)\) , \((64,80,144)\) , 其中 \((36,108,144)\) 在交换学生1和学生2头上的数之后依然成立。

逻辑链如下(以 \(64,80,144\) 为例):

[64, 80, 144], player-2, pred=True, valid=True
    [64, 80, 144], player-1, pred=False, valid=True
        [64, 208, 144], player-0, pred=False, valid=True
            [352, 208, 144], player-2, pred=False, valid=True
                [352, 208, 560], player-1, pred=False, valid=True
                    [352, 912, 560], player-0, pred=False, valid=True
                        [1472, 912, 560], god, pred=None, valid=True
                        [352, 912, 560], god, pred=None, valid=True
                    [352, 208, 560], player-0, pred=False, valid=True
                        [768, 208, 560], god, pred=None, valid=True
                        [352, 208, 560], god, pred=None, valid=True
                [352, 208, 144], player-1, pred=False, valid=True
                    [352, 496, 144], player-0, pred=False, valid=True
                        [640, 496, 144], god, pred=None, valid=True
                        [352, 496, 144], god, pred=None, valid=True
                    [352, 208, 144], player-0, pred=False, valid=True
                        [352, 208, 144], god, pred=None, valid=True
                        [64, 208, 144], god, pred=None, valid=True
            [64, 208, 144], player-2, pred=False, valid=True
                [64, 208, 272], player-1, pred=False, valid=True
                    [64, 336, 272], player-0, pred=False, valid=True
                        [608, 336, 272], god, pred=None, valid=True
                        [64, 336, 272], god, pred=None, valid=True
                    [64, 208, 272], player-0, pred=False, valid=True
                        [480, 208, 272], god, pred=None, valid=True
                        [64, 208, 272], god, pred=None, valid=True
                [64, 208, 144], player-1, pred=False, valid=True
                    [64, 208, 144], player-0, pred=False, valid=True
                        [352, 208, 144], god, pred=None, valid=True
                        [64, 208, 144], god, pred=None, valid=True
                    [64, 80, 144], player-0, pred=False, valid=True
                        [224, 80, 144], god, pred=None, valid=True
                        [64, 80, 144], god, pred=None, valid=True
        [64, 80, 144], player-0, pred=False, valid=True
            [224, 80, 144], player-2, pred=False, valid=True
                [224, 80, 304], player-1, pred=False, valid=True
                    [224, 528, 304], player-0, pred=False, valid=True
                        [832, 528, 304], god, pred=None, valid=True
                        [224, 528, 304], god, pred=None, valid=True
                    [224, 80, 304], player-0, pred=False, valid=True
                        [384, 80, 304], god, pred=None, valid=True
                        [224, 80, 304], god, pred=None, valid=True
                [224, 80, 144], player-1, pred=False, valid=True
                    [224, 368, 144], player-0, pred=False, valid=True
                        [512, 368, 144], god, pred=None, valid=True
                        [224, 368, 144], god, pred=None, valid=True
                    [224, 80, 144], player-0, pred=False, valid=True
                        [224, 80, 144], god, pred=None, valid=True
                        [64, 80, 144], god, pred=None, valid=True
            [64, 80, 144], player-2, pred=False, valid=True
                [64, 80, 144], player-1, pred=False, valid=True
                    [64, 208, 144], player-0, pred=False, valid=True
                        [352, 208, 144], god, pred=None, valid=True
                        [64, 208, 144], god, pred=None, valid=True
                    [64, 80, 144], player-0, pred=False, valid=True
                        [224, 80, 144], god, pred=None, valid=True
                        [64, 80, 144], god, pred=None, valid=True
                [64, 80, 16], player-1, pred=False, valid=True
                    [64, 80, 16], player-0, pred=False, valid=True
                        [96, 80, 16], god, pred=None, valid=True
                        [64, 80, 16], god, pred=None, valid=True
                    [64, 48, 16], player-0, pred=False, valid=True
                        [64, 48, 16], god, pred=None, valid=True
                        [32, 48, 16], god, pred=None, valid=True
    [64, 80, 16], player-1, pred=False, valid=False
        [64, 80, 16], player-0, pred=False, valid=True
            [96, 80, 16], player-2, pred=False, valid=True
                [96, 80, 176], player-1, pred=False, valid=True
                    [96, 272, 176], player-0, pred=False, valid=True
                        [448, 272, 176], god, pred=None, valid=True
                        [96, 272, 176], god, pred=None, valid=True
                    [96, 80, 176], player-0, pred=False, valid=True
                        [256, 80, 176], god, pred=None, valid=True
                        [96, 80, 176], god, pred=None, valid=True
                [96, 80, 16], player-1, pred=False, valid=True
                    [96, 112, 16], player-0, pred=False, valid=True
                        [128, 112, 16], god, pred=None, valid=True
                        [96, 112, 16], god, pred=None, valid=True
                    [96, 80, 16], player-0, pred=False, valid=True
                        [96, 80, 16], god, pred=None, valid=True
                        [64, 80, 16], god, pred=None, valid=True
            [64, 80, 16], player-2, pred=False, valid=True
                [64, 80, 144], player-1, pred=False, valid=True
                    [64, 208, 144], player-0, pred=False, valid=True
                        [352, 208, 144], god, pred=None, valid=True
                        [64, 208, 144], god, pred=None, valid=True
                    [64, 80, 144], player-0, pred=False, valid=True
                        [224, 80, 144], god, pred=None, valid=True
                        [64, 80, 144], god, pred=None, valid=True
                [64, 80, 16], player-1, pred=False, valid=True
                    [64, 80, 16], player-0, pred=False, valid=True
                        [96, 80, 16], god, pred=None, valid=True
                        [64, 80, 16], god, pred=None, valid=True
                    [64, 48, 16], player-0, pred=False, valid=True
                        [64, 48, 16], god, pred=None, valid=True
                        [32, 48, 16], god, pred=None, valid=True
        [64, 48, 16], player-0, pred=False, valid=False
            [64, 48, 16], player-2, pred=False, valid=True
                [64, 48, 112], player-1, pred=False, valid=True
                    [64, 176, 112], player-0, pred=False, valid=True
                        [288, 176, 112], god, pred=None, valid=True
                        [64, 176, 112], god, pred=None, valid=True
                    [64, 48, 112], player-0, pred=False, valid=True
                        [160, 48, 112], god, pred=None, valid=True
                        [64, 48, 112], god, pred=None, valid=True
                [64, 48, 16], player-1, pred=False, valid=True
                    [64, 80, 16], player-0, pred=False, valid=True
                        [96, 80, 16], god, pred=None, valid=True
                        [64, 80, 16], god, pred=None, valid=True
                    [64, 48, 16], player-0, pred=False, valid=True
                        [64, 48, 16], god, pred=None, valid=True
                        [32, 48, 16], god, pred=None, valid=True
            [32, 48, 16], player-2, pred=False, valid=False
                [32, 48, 80], player-1, pred=False, valid=True
                    [32, 112, 80], player-0, pred=False, valid=True
                        [192, 112, 80], god, pred=None, valid=True
                        [32, 112, 80], god, pred=None, valid=True
                    [32, 48, 80], player-0, pred=False, valid=True
                        [128, 48, 80], god, pred=None, valid=True
                        [32, 48, 80], god, pred=None, valid=True
                [32, 48, 16], player-1, pred=False, valid=False
                    [32, 48, 16], player-0, pred=False, valid=True
                        [64, 48, 16], god, pred=None, valid=True
                        [32, 48, 16], god, pred=None, valid=True
                    [32, 16, 16], player-0, pred=False, valid=False
                        [32, 16, 16], god, pred=None, valid=True
                        [0, 16, 16], god, pred=None, valid=False

P.S. 今天苏炳添破了黄种人的男子百米记录,祝贺他!

Footnotes:

Author: expye(Zihao Ye)

Email: expye@outlook.com

Date: 2021-08-01 Sun 00:00

Last modified: 2021-10-25 Mon 21:58

Licensed under CC BY-NC 4.0