如何将扫雷场景的布尔公式转换为CNF供SAT Solver使用？

你当前推导的三子句CNF仅覆盖了「3个邻格中至少有2个雷」的约束，还存在缺陷：

• 这三个子句无法排除「3个邻格都是雷」的非法场景：当1、2、3都为真（全是雷）时，三个子句全部成立，但此时邻格雷数为3，不符合(1,1)单元格数值为2的要求。
• 补充修正：需要新增一个子句约束「最多有2个雷」，也就是排除三个都是雷的情况，最终完整CNF为：
  {{1,2,-3}, {1,-2,3}, {-1,2,3}, {-1,-2,-3}}

你原来的三个子句已经可以排除所有雷数小于2（0个雷、1个雷）的场景，补充第四个子句后就刚好覆盖了「恰好2个雷」的所有约束。

• 不要做场景硬编码：当前逻辑仅适配角落、数值为2的单元格，需要通用化不同位置（角落、边缘、内部）、不同数值的单元格约束生成逻辑，不需要针对每个场景单独写判断。
• 建立全局知识库：不要每次单独查询单个单元格的约束，把所有已揭开的数值单元格的约束全部合并到全局知识库中，统一求解，避免重复计算。
• 修正判断逻辑：对每个未知格子x，正确的判断逻辑应该是两次查询：
  • 查询全局知识库 ∧ x是否可满足，如果不可满足，说明x一定不是雷，可以安全点开
  • 查询全局知识库 ∧ ¬x是否可满足，如果不可满足，说明x一定是雷，直接标记
• 增加循环迭代逻辑：单次遍历无法处理更新后的约束，应该每次标记/点开新单元格后，把新单元格的约束加入全局知识库，再次迭代求解，直到没有新的可确定单元格为止。
• 增加约束去重、剪枝逻辑：移除知识库中重复的子句，缩小SAT求解的输入规模，提升运行效率。

不能，原因有两点：

1. 扫雷本身存在无确定解的场景：当剩余未知格子的约束存在多组可满足的赋值时（比如只剩两个格子，必有一个雷，没有其他约束），SAT求解无法给出唯一结论，必须通过猜测才能继续，这类场景任何确定性逻辑都无法100%求解。
2. 你当前的伪代码逻辑覆盖不全：仅处理了角落数值为2的场景，且没有加入全局总雷数的约束（加入后可以解决部分多解场景），连基础的全场景覆盖都没有达到，更无法完成所有可确定的扫雷求解。

内容的提问来源于stack exchange，提问作者philuix