93步最优解：非局部水晶交换谜题的精确证明

谜题与规则

《Order of the Sinking Star》中的水晶交换谜题要求玩家在11×11棋盘上，通过最少的指令数将全部16颗水晶移动到目标位置。指令会交换玩家与所选行或列中最近的水晶，无视距离；只有空射线才允许普通单位行走。两扇门仅在16颗水晶全部就位时允许玩家通过。这个设定看似简单，却因指令的“非局部”特性——交换效果依赖于全局排列——而变得极其复杂。

广度优先搜索（BFS）与成本有界搜索：BFS 是一种盲目搜索策略，按步数（或成本）递增的顺序逐层扩展状态，因此首次到达目标状态时所用的步数即为最短步数。成本有界 BFS 在此基础上增加一个上界（本例中为 93），只扩展成本不超过该上界的状态，并利用可采纳启发式进行剪枝：若某状态的成本下界加上已用成本超过上界，则直接舍弃。这样既能保证完备性（不漏掉任何更短解），又能大幅减少搜索空间。

精确解与排除更短解

研究者给出了一个显式的93指令解法，并通过精确的、成本有界的广度优先搜索（BFS）排除了所有更短的解。搜索将每个位置表示为17个被占据的单元格（16颗水晶加玩家）和一个活动单元格。为了高效剪枝，设计了一个可采纳的启发式函数：将指令成本分解为压缩核心抽象和残余运动，并加入必要的激活绕行和角落访问条件进行强化。

完整计算保留了605,349,215个被占据集合和1,863,925,136个状态，最终证明93步是最优的。这本质上是一个计算机辅助证明，针对特定实例，并附带了明确的实现信任边界。

可采纳启发式（Admissible Heuristic）：在最短路径搜索中，启发式函数用于估计从当前状态到目标状态的最小剩余成本。若该估计从不高估真实成本，则称为“可采纳的”。可采纳性至关重要：它保证搜索算法（如 A* 或成本有界 BFS）在剪枝时不会错误地排除包含最优解的路径。本文的启发式将指令成本分解为压缩核心抽象和残余运动，并加入激活绕行与角落访问条件，这些条件均经过形式化证明，确保估计值不超过实际所需步数，从而在保持完备性的同时实现高效剪枝。

启发式与搜索优化

启发式的核心思想是将问题分解为两个部分：一个压缩的核心抽象（捕捉水晶交换的全局约束）和残余运动（玩家移动到可执行交换的位置）。通过“激活绕行”条件，搜索能够识别出玩家必须先移动到特定位置才能激活某些交换，从而避免无效分支。角落访问条件则进一步剪除那些无法在剩余步数内访问必要角落的路径。

这些缩减和剪枝条件均经过形式化证明，确保了搜索的完备性。存储方案也经过精心设计，以处理数十亿状态的内存需求。

可复现性与信任边界

作者提供了源代码、执行日志和复现驱动，使整个证明过程可被独立验证。然而，计算机辅助证明的可靠性依赖于实现细节的正确性，因此作者明确指出了信任边界：证明的有效性取决于代码逻辑与形式化描述的一致性。这种透明性对于此类复杂搜索证明至关重要。

对谜题设计与AI求解的启示

这项工作的意义不仅在于解决了一个具体谜题。它展示了如何将非局部约束转化为可处理的搜索问题，并通过精确的启发式设计实现指数级剪枝。对于游戏设计者，这提示了指令交换机制的深度可能远超表面；对于AI求解器开发者，这种“抽象+残余”的启发式构造思路可迁移到其他组合优化问题。

此外，93步的精确解也为玩家提供了理论上的最优路径，或许能激发社区对更多关卡的最优解探索。