Posting Puzzle：用 Post 对应问题做成的解谜小游戏
文章摘要
Posting Puzzle 是发布在 itch.io 上的一款免费网页解谜小游戏，外表是温馨的邮局分拣：把信封和邮票配成对，投进邮筒。它的内核却是计算理论里最著名的不可判定问题之一：Post 对应问题（Post’s Correspondence Problem，PCP）。作者 mametter 在 Show HN 里说，做这个游戏是为了庆祝 PCP[3,4] 的所有实例终于全部被解决。
Post 对应问题是什么。 1946 年，逻辑学家 Emil Post 提出了这样一个问题：给你若干张「多米诺骨牌」，每张上面写一个字符串、下面写一个字符串；每种牌可以无限次重复使用，问能否挑出一个牌的序列，使得上面拼起来的字符串和下面拼起来的完全相同。规则简单到小学生都能理解，但 Post 证明了一般情况下不存在能对任意实例判定「有没有解」的算法。它因此成为证明其他问题不可判定时最常用的「跳板」之一。按牌的数量细分：只有 2 种牌时问题可判定，5 种牌时已知不可判定，3 种和 4 种牌的一般情形至今悬而未决。在研究文献里，PCP[3,4] 指的是「3 种牌、每个字符串最长 4 个字符」的这一类实例。
PCP[3,4] 刚刚被「清零」。 游戏页面链接的 GitHub 仓库 Mojashi/pcp-3-4-proofs 说明了背景：2001 到 2002 年间，阿尔伯塔大学的 Ling Zhao 在硕士论文里用自己写的求解器系统地攻打 PCP 难题实例，最后公布了 3,170 个他的求解器也搞不定的 PCP[3,4] 实例。这个仓库为这 3,170 个实例逐一给出了解，或者给出「无解」的证明，证明文件是 Isabelle 定理证明器的形式化理论。仓库在 2026 年 9 月 8 日更新：最后两个悬而未决的实例也被解出，最短解长度分别是 1,584 和 2,712，至此全部 3,170 个实例都有了解或无解证明。仓库也如实注明，其中 5 个实例是通过变换（例如把某个子串替换成更短的串、把牌左右或上下翻转）归约到其他实例来处理的，这些归约的正确性尚未形式化。
游戏怎么玩。 屏幕上有三个编号的托盘，每个托盘里装着一排信封和一排邮票，对应一张 PCP 骨牌的上下两个字符串。按 1、2、3 或点击托盘，就把它的内容同时追加到上下两条队列末尾。同一个位置上如果是「一个信封配一张邮票」，就会被投递出去；如果是两个同类（两个信封或两张邮票），就会被退回，这一步走错了，需要撤销（Z 或 Backspace）再试，R 重置本关，左右方向键切换关卡。把收件箱清空就过关。换成 PCP 的语言：信封和邮票就是二元字母表里的两个符号，只是其中一行的符号被「取反」了，要求上下完全互补，本质上与要求上下相同是一回事。
以第一关为例：托盘 1 是「1 个信封 / 2 张邮票」，托盘 2 是「3 个信封 / 1 张邮票」，托盘 3 是「2 个信封 / 2 个信封」。托盘 3 上下同类，按下去必然被退回，是个诱饵；正确做法是按 1、1、2，上面凑成 5 个信封，下面凑成 5 张邮票，全部配对成功。
十二关，外加一个隐藏关，以及一条故事线。 作者说前六关可以靠手解，后六关是「从文献里借来的困难实例」，手工解不出来。游戏用一段小故事串起关卡：「纽约，1946 年。一位名叫 Post 先生的绅士送来了他的第一封信。『很好投递。』他说。」随着关卡推进，「Post 先生的信越来越长」；到了后半段，「Post 先生的通信变得复杂起来，他建议用他的一台机器」，提示你「这些关你得写个程序来解」，并且允许长按队列粘贴一串托盘编号（例如 3123）作为操作序列。页面源码里标着后四关的「已知最短解」：第 9 关 216 步，第 10 关 452 步，第 11 关 1,584 步，第 12 关 2,712 步。最后两关正是仓库里刚刚被攻克的那两个实例，故事里的说法是：「Post 先生的最后两封信。直到 2026 年之前，没有人能投递它们。」全部通关后还会解锁一个额外关卡。
作者与前身。 页面上写着这个游戏有一个更早的版本，放在 mame.github.io/posting-puzzle。那个旧版只有六关，规则说明写着「请把信件和邮票配对后投进邮筒；清空收件箱里所有未寄出的信件和未使用的邮票即可过关」，致谢里还特别注明它「用 ruby.wasm 编写，没有直接使用任何 JavaScript」，源码在 GitHub 的 mame/posting-puzzle 仓库。GitHub 上的 mame 即 Ruby 核心开发者远藤侑介，以 Quine Relay 这类炫技程序闻名。新版用了 Special Elite 打字机字体营造旧邮局气氛；itch.io 页面的 AI 声明勾选了代码、图像、声音、文本均有 AI 辅助，并说明图片由 ChatGPT 和 Gemini 生成后经过手工修改。
HN 评论精华
这条 Show HN 只有 3 分，唯一的一条评论来自作者 mametter 本人，没有其他用户参与讨论。
作者的说明很短：这是一个关于分拣信封和邮票的小谜题，「就是给 Post 对应问题套了一层邮政外皮」。一共十二关，前六关可以手解，后六关取自文献里的实例，手解不出来。「如果你以前没接触过这个问题，这是一个感受它的方式：规则就是它的全部，而它在一般情况下是不可判定的。」他最后附上了 pcp-3-4-proofs 仓库的链接，说明游戏是为庆祝 PCP[3,4] 的每个实例终于都有了结论而做的。
由于讨论几乎为零，这里补充一点游戏之外值得一提的背景：Posting Puzzle 最有意思的设计，是把「不可判定」这件抽象的事变成了可以亲手体验的难度曲线。前几关几步就能解完，而第 11、12 关的最短解分别要按 1,584 次和 2,712 次托盘，这两个解直到 2026 年 9 月才被找到。规则从头到尾没有变过，变的只是三只托盘里那几个字符。