每个 Griductive 谜题都做出一个大胆的承诺：你永远不需要猜测。 每个格子都可以仅通过逻辑推导确定，每个谜题只有唯一的正确答案。
这不是一个设计目标——而是一个数学保证，由运筹学和芯片验证领域同一类求解器来强制执行。这篇文章将解释其中的原理。
为什么唯一解如此重要
如果一个谜题有两个合法解，那必然存在至少一个格子，在该格子上嫌疑人和无辜者都能满足所有线索。在那个格子上，无论你怎么推理都无法确定正确答案——你只能猜。猜测违背了演绎解谜的核心契约。
因此，生成器不只是生产碰巧只有一个解的谜题。它会在谜题发布之前证明不存在第二个解。
五阶段生成流水线
每个 Griductive 谜题都经过五个阶段的流水线构建。以下是每个阶段的工作内容。
第一阶段：生成随机解
生成器首先创建一个合法的解方案网格——为每个格子随机分配嫌疑人或无辜者。这是玩家最终将要推导出的真实答案。
此时还没有任何线索。棋盘只是一个满足基本结构约束（网格尺寸、嫌疑人数量在合理范围内）的随机配置。
第二阶段：构建线索池
接下来，生成器穷举所有在解方案上为真的可能线索。
Griductive 拥有超过 26 种不同的线索类型——计数、比较、空间、存在性、唯一性、连通性等等。对于每种类型，生成器测试所有合法的参数组合。一个 4×4 的网格可以产生数千条候选线索。只有在解方案上求值为真的线索才会被保留。
这就是生成器的原材料：一个庞大的真实陈述池，其中大多数是冗余的。
第三阶段：选择最小线索集（最难的部分）
这是真正的核心工作。生成器需要从线索池中选出一个小子集，使得：
- 线索是充分的 —— 它们共同将解空间约束到恰好一个合法棋盘。
- 没有冗余线索 —— 移除任何一条线索都会导致存在多个解。
生成器使用贪心约束满足方法：
- 从没有任何线索开始。解空间完全开放——许多棋盘都可能是合法的。
- 为每条候选线索评分，看它能缩小多少解空间。一条能消除 80% 剩余可能性的线索比只能消除 10% 的得分更高。
- 选择得分最高的线索加入集合。
- 用更新后的线索集重新求解约束模型。
- 重复直到求解器确认只剩下一个解。
- 剪枝：遍历最终集合，移除任何对保持唯一性不必要的线索。这保持了谜题的简洁，避免给玩家多余的信息。
最终结果是一个紧凑、公平的线索集——刚好足以完整解开谜题，没有浪费任何一条线索。
第四阶段：评估难度
线索集确定后，生成器在 0–100 的范围内为谜题的难度评分。四个因素共同决定：
- 简单线索占比（35%） —— 有多少线索是直接的计数或身份陈述。简单线索越多，谜题越容易。
- 复杂线索占比（30%） —— 有多少线索需要多步或空间推理。这些需要更深的推理链。
- 信息稀缺度（20%） —— 相对于网格大小，给出的线索有多少。线索越少，可用信息越少。
- 网格规模（15%） —— 更大的网格本身就更难追踪。一个 5×5 的谜题格子数几乎是 3×3 的三倍。
每种线索类型还有一个基于其推理难度的内在复杂度评分。像"Julia 是嫌疑人"这样的线索简单到不能再简单。而"Julia 是第 3 行中唯一一个恰好有 1 个嫌疑人邻居的人"这样的线索需要交叉比对多个格子，评分要高得多。
第五阶段：生成提示并格式化输出
最后，生成器构建提示序列——一个推荐的求解顺序，一步一步引导卡住的玩家通过谜题。提示按依赖深度排序：可以立即推导的格子排在前面，需要长串前置推理的格子排在后面。
最终谜题被打包为游戏所需的全部数据：元信息、线索集、提示序列和难度分数。
求解器：如何证明唯一性
流水线的核心是 Google OR-Tools CP-SAT——一个结合了约束传播、整数规划和 SAT 求解的约束编程求解器。
谜题如何变成数学问题
网格上的每个格子被建模为一个布尔变量：嫌疑人（1）或无辜者（0）。每条线索变成这些变量上的一个或多个数学约束。
例如：
- "第 3 行恰好有 2 个嫌疑人" 变为：
cell[3,0] + cell[3,1] + cell[3,2] + cell[3,3] = 2 - "A 列所有嫌疑人是相连的" 变为：一个连通性约束，确保 A 列中的嫌疑人格子形成一条没有间断的连续链。
- "第 1 行的嫌疑人比 B 列多" 变为：
sum(row_1) > sum(col_B)
如何验证唯一性
组装好线索集后，生成器向 CP-SAT 提出一个精确的问题："在这些约束下，是否存在多于一个的合法赋值？"
CP-SAT 不只是找到一个解——它可以枚举所有解。如果求解器只找到一个，谜题就是合法的。如果找到两个或更多，生成器会回到第三阶段添加更多线索。
这是一个形式化证明，不是启发式方法。CP-SAT 穷举整个解空间。如果它说只有一个解，那就确实只有一个——没有例外。
为什么不直接暴力搜索？
一个 5×5 的网格有 25 个格子，每个格子有 2 种可能的值。那就是 2²⁵ = 3300 万种可能的棋盘。逐一检查所有棋盘既慢又无法扩展。
CP-SAT 之所以快得多，是因为约束传播：当一条线索说"第 3 行恰好有 2 个嫌疑人"时，求解器会立即缩小第 3 行每个格子的搜索空间，而不需要逐个检查每种组合。复杂线索会叠加这种效果。在实际运行中，CP-SAT 可以在毫秒内证明一个 5×5 谜题的唯一性。
可能出什么问题（以及我们如何预防）
"如果线索有歧义怎么办？"
每种线索类型都有严格的数学定义。"邻居"始终指周围最多 8 个格子（包括对角线）。"相连"始终指一条相邻格子的连续链。"之间"始终指同一行或同一列的格子，不包括端点。
这些定义直接内置在约束模型中——没有自然语言解释的环节，歧义无从产生。游戏内的术语详解参考说明向玩家精确展示了每个空间关键词的含义。
"如果求解器有 bug 怎么办？"
CP-SAT 求解器是由 Google 优化团队维护的、经过充分测试的成熟工具。但我们不仅仅依赖信任。每个生成的谜题都会经过独立验证：
- 自动求解器会尝试逐步解开每个谜题，模拟人类玩家的过程。如果它无法仅通过逻辑推理达到完整解答，该谜题会被拒绝。
- 提示合理性检查验证序列中的每个提示在逻辑上是有效的——被提示的格子确实可以从线索和已揭示的格子中推导出来，而不是依赖隐藏信息。
"如果线索生成遗漏了边界情况怎么办？"
每种线索类型都有形式化的求值函数，经过已知谜题配置的测试。线索池生成阶段只保留在实际解方案上求值为真的线索——一条在解方案上为假的线索永远不会出现在谜题中。
最终结果
当你打开一个 Griductive 谜题时，以下这些步骤都已经完成了：
- 生成了一个随机解方案。
- 数千条候选线索被逐一验证。
- 一个最小的、无冗余的子集被选出。
- 形式化求解器证明了恰好只有一个解满足这些线索。
- 自动求解器独立验证了该谜题可以通过纯逻辑推理解开。
- 计算了难度分数并生成了提示序列。
每个谜题，每一天，涵盖所有四种网格尺寸。没有例外。
如果你卡住了，一定有一条线索你还没有充分利用。如果你觉得存在两个可能的答案，重新阅读线索——逻辑会给出裁决。如果你想要证据，推理图会展示从线索到解答的完整推理链。
未来展望：会讲故事的线索
目前，Griductive 的线索读起来像精确的逻辑陈述——清晰且无歧义，但确实有点冷冰冰的。"第 3 行恰好有 2 个嫌疑人"完成了它的使命，但不太能让你感觉自己真的在办案。
我们正在积极改变这一点。目标是在保持底层逻辑精确性的同时，让线索的表达方式更加丰富多样。想象一下与节日活动绑定的线索，或者以特定犯罪现场的证人证词形式呈现的线索。不再是冰冷的公式，而是读起来像真正来自调查现场的一份证据。
核心约束没有改变：每条线索必须保持一致、无歧义且可被形式化验证。求解器不在乎一条线索听起来像数学教科书还是黑色电影的台词——它只关心逻辑内容。正是这种分离让更丰富的表达成为可能，同时不会损害正确性。
同样的保证。同样的严谨。但谜题不再像方程式，而更像值得破解的案件。
不需要猜测。不需要运气。数学保证。