如何为基于SAT求解器的迷宫生成正确的CNF公式？

一、现有CNF约束的问题与修正 #

1. formula_1：2×2区域至少一堵墙 #

你当前的约束大概率只覆盖了2×2区域的外框墙，但核心要求是不能出现无任何内部墙的2×2空白块。正确的CNF子句应该针对每个2×2单元格组（(i,j)、(i,j+1)、(i+1,j)、(i+1,j+1)），确保内部至少有一堵墙：

对于每个0 ≤ i < n-1，0 ≤ j < n-1：
(wall_right(i,j) ∨ wall_down(i,j) ∨ wall_right(i+1,j) ∨ wall_down(i,j+1))

这里wall_right(i,j)指单元格(i,j)右侧的墙，wall_down(i,j)指单元格(i,j)下方的墙。这个子句直接避免了四个单元格形成完全连通的2×2区域。

2. formula_2：无孤立水平墙 #

孤立水平墙指的是一段水平墙没连到垂直墙或迷宫边界，你之前的约束可能没考虑边界情况和两端的连接。修正后的约束：

# 非边界的水平墙段
对于0 < i < n-1，0 ≤ j < n-1：
(¬wall_right(i,j) ∨ wall_down(i,j) ∨ wall_down(i,j-1) ∨ wall_up(i,j) ∨ wall_up(i,j-1))

# 最顶部的水平墙段（i=0）
对于0 ≤ j < n-1：
(¬wall_right(0,j) ∨ wall_down(0,j) ∨ wall_down(0,j-1))

# 最底部的水平墙段（i=n-1）
对于0 ≤ j < n-1：
(¬wall_right(n-1,j) ∨ wall_up(n-1,j) ∨ wall_up(n-1,j-1))

逻辑很简单：如果这段水平墙存在，那它的上下两端至少得连到垂直墙或者边界，不能悬在半空。

3. formula_3：无孤立垂直墙 #

和水平墙逻辑一致，孤立垂直墙是没连到水平墙或边界的垂直墙段，修正约束：

# 非边界的垂直墙段
对于0 ≤ i < n-1，0 < j < n-1：
(¬wall_down(i,j) ∨ wall_right(i,j) ∨ wall_right(i-1,j) ∨ wall_left(i,j) ∨ wall_left(i-1,j))

# 最左侧的垂直墙段（j=0）
对于0 ≤ i < n-1：
(¬wall_down(i,0) ∨ wall_right(i,0) ∨ wall_right(i-1,0))

# 最右侧的垂直墙段（j=n-1）
对于0 ≤ i < n-1：
(¬wall_down(i,n-1) ∨ wall_left(i,n-1) ∨ wall_left(i-1,n-1))

4. formula_4：无孤立1×1方块 #

你之前的约束方向是对的（防止单元格被四面墙完全封死），但要确保子句正确：

对于每个0 ≤ i < n，0 ≤ j < n：
(¬wall_up(i,j) ∨ ¬wall_down(i,j) ∨ ¬wall_left(i,j) ∨ ¬wall_right(i,j))

这个子句保证每个单元格至少有一个方向没有墙，不会变成完全孤立的死块。

二、SAT求解器使用的核心问题（大迷宫失效的关键） #

1. 缺失连通性约束 #

这是20×20迷宫效果差的致命问题！你现有的四个约束只保证了局部结构，但没确保整个迷宫是单连通的（所有单元格都能从起点到达）。解决方式有两种：

• 可达性变量建模：定义reach(i,j)表示单元格(i,j)能从起点（比如(0,0)）到达，添加以下约束：
  • 起点必可达：reach(0,0)
  • 相邻单元格可达性传递：如果单元格(i,j)可达，且和(k,l)之间没墙，那么(k,l)也必须可达。转化为CNF：

    # 向下可达
    对于0 ≤ i < n-1，0 ≤ j < n：
    (¬reach(i,j) ∨ ¬wall_down(i,j) ∨ reach(i+1,j))
    (¬reach(i+1,j) ∨ ¬wall_down(i,j) ∨ reach(i,j))
    
    # 向右可达（同理处理上下左方向）
    对于0 ≤ i < n，0 ≤ j < n-1：
    (¬reach(i,j) ∨ ¬wall_right(i,j) ∨ reach(i,j+1))
    (¬reach(i,j+1) ∨ ¬wall_right(i,j) ∨ reach(i,j))
    

  • 所有单元格必须可达：reach(i,j)对所有(i,j)成立
• 增量求解：先跑现有约束得到一个解，检查迷宫是否连通；如果不连通，添加约束排除这个不连通的解，重复直到得到连通的迷宫。这种方式避免了直接添加大量子句，效率更高。

2. 变量建模错误 #

如果你的代码里把相邻单元格的墙当成独立变量（比如单元格(i,j)的右侧墙和(i,j+1)的左侧墙是两个变量），会导致墙的状态矛盾，生成的迷宫逻辑混乱。必须共享墙变量：wall_right(i,j)就是单元格(i,j+1)的左侧墙，只用一个变量表示，避免不一致。

3. 求解效率问题 #

20×20迷宫的变量数量不少（仅墙变量就有20×20×2=800个，因为左右、上下墙共享），加上可达性变量400个，子句数量会非常多。优化建议：

• 用高效的SAT求解器：比如pysat库的Glucose3或Cadical，别用自己写的简单回溯求解器
• 减少冗余约束：比如formula_1和其他约束的重叠部分可以合并
• 变量排序：按单元格顺序、墙类型排序变量，帮助求解器更快剪枝

三、额外的迷宫约束（可选） #

如果需要标准迷宫，还可以添加：

• 边界封闭约束：最外层单元格的外框必须是墙（除了指定的入口和出口）
• 入口出口约束：指定起点和终点的墙不存在（比如(0,0)左侧无墙，(n-1,n-1)右侧无墙）

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