基于SAT的蜂窝数独求解：从CNF编码到DPLL优化实践

简介华中科技大学二零二二级程序设计综合课程设计任务“基于SAT的蜂窝数独游戏求解程序”完整工程包是一个将SAT求解应用于趣味逻辑谜题的典型C项目适合计算机相关专业学生作为课设参考也适合对自动推理与回溯算法感兴趣的学习者深入研读。压缩包共十一个文件其中七个C源文件与一个头文件分别承担DPLL求解核心、CNF公式转换、蜂窝数独棋盘建模、答案输出与计时统计等职责另附实验报告PDF和README说明文档总大小仅一点二三MB结构紧凑、模块边界清晰。已有一百五十人浏览学习。代码经过完整运行测试答辩平均分达九十六分下载后即可编译运行通过阅读源码与实验报告读者能快速掌握将数独条件编码为SAT子句的建模方式理解DPLL分支回溯与冲突处理机制也可在此基础上扩展新功能完成其他数独变种或逻辑谜题的求解。1. 蜂窝数独不是“换了个形状”为什么用 SAT 而不是回溯把蜂窝数独丢给 SAT 求解器第一反应往往是“这不就是给回溯换个马甲嘛”。真正做完华中科技大学这道程序设计综合课程设计之后我才意识到门槛不在 DPLL 本身而在六边形棋盘上那些斜向连续的约束怎么翻译成 CNF 子句。蜂窝数独的每一格有六个邻居行、列、宫都不再是横平竖直的三等份靠手写搜索很容易漏方向而把“每个格子恰好一个数字、同组格子不得重复”直接写成布尔约束交给 SAT 引擎去传播求解逻辑和游戏规则就能彻底解耦。这个题目适合 C 入门到进阶之间的人练手既能写一个最小可用的 DPLL 求解器又能理解现代求解器里为什么要做冲突分析和子句学习。下文按“变量编码 → 源码结构 → 性能调参 → 验证排错”的顺序把完整流程拆开讲。2. 六边形棋盘到 CNF变量编号与约束组生成2.1 用 Cube 坐标给 37 个格子编号SAT 求解器只认识布尔变量和子句所以第一步是决定“哪个变量代表哪种情况”。这里用x_{c,d}表示“第 c 个格子填数字 d”其中 c 是格子的全局编号d 从 0 开始0 对应数字 18 对应数字 9。变量编号统一暴露为 1 基整数取反用负号表示。这样 DPLL 里可以用assign[abs(lit)]直接查赋值。六边形棋盘不采用二维数组的(x,y)而是用更自然的 Cube 坐标。Cube 坐标有三个轴 x、y、z满足x y z 0棋盘半径取 4 时正好 37 个格子。预先生成一张coordToId映射后续生成行列约束时直接查表。#include map #include tuple #include cstdlib std::mapstd::tupleint, int, int, int coordToId; int NC 0; for (int x -4; x 4; x) { for (int y -4; y 4; y) { int z -x - y; if (std::abs(x) 4 || std::abs(y) 4 || std::abs(z) 4) continue; coordToId[{x, y, z}] NC; } } // NC 37这里coordToId的作用是把空间坐标压缩成 0..36 的连续编号后面所有数组大小都依赖这个编号。检查abs(z) 4是 Cube 坐标下六边形是否在棋盘内的判断条件漏掉它会混入形状之外的格子。变量编号函数如下const int ND 9; // 返回 1 基变量编号negtrue 表示生成该变量的负字面量 inline int lit(int cell, int digit, bool neg false) { int v cell * ND digit 1; return neg ? -v : v; }这段代码是最容易踩坑的地方cell 和 digit 都必须是 0 基而变量编号是 1 基所以最后加 1。如果写成cell * 9 digit变量 0 就会混进 DPLL导致assign[0]被当成一个真实变量反复赋值。2.2 每个格子的“恰好一个数字”基数约束蜂窝数独的第一类规则是每个格子必须填且只能填一个数字。拆成两个部分至少一个数字、至多一个数字。至少一个数字是一个 9 元大子句九个候选数字字面量取或至多一个数字则需要写成两两互斥也就是对任意两个数字不允许它们同时为真。// 格子 c 至少一个数字 std::vectorint atLeast; for (int d 0; d ND; d) { atLeast.push_back(lit(c, d)); } solver.addClause(atLeast); // 格子 c 至多一个数字两两互斥 for (int d1 0; d1 ND; d1) { for (int d2 d1 1; d2 ND; d2) { std::vectorint bin; bin.push_back(lit(c, d1, true)); bin.push_back(lit(c, d2, true)); solver.addClause(bin); } }一个格子会产生 1 条 9 元子句和 C(9,2)36 条二元子句整个棋盘固定基数约束是 37 条大子句加上 1332 条互斥子句。对课程设计来说这个规模很小完全没有必要上顺序编码或者位压缩。二元互斥子句对单元传播很友好DPLL 只会受益于这种简单结构。2.3 行、列、斜线与宫约束组统一处理蜂窝数独的其余规则是在同一条直线、同一列斜线或同一个宫的格子中不能出现重复数字。用 SAT 表达就是对任意两个同组格子a和b以及任意数字d不能同时有x_{a,d}和x_{b,d}为真。这一约束不需要 at-least-one因为行长度不固定中心行有 9 格边缘可能只有 1 格。生成这些约束组时固定 Cube 坐标的一维即可得到三个方向的所有平行线。std::vectorstd::vectorint buildLineGroups() { std::vectorstd::vectorint groups; for (int axis 0; axis 3; axis) { for (int v -4; v 4; v) { std::vectorint line; for (int w -4; w 4; w) { int x 0, y 0, z 0; if (axis 0) { x v; y w; z -x - y; } else if (axis 1) { y v; z w; x -y - z; } else { z v; x w; y -z - x; } if (coordToId.count({x, y, z})) { line.push_back(coordToId[{x, y, z}]); } } if (line.size() 2) groups.push_back(line); } } return groups; } // 对任一组任意两格不能填同一个数字 void addGroupAtMostOne(Solver solver, const std::vectorint group) { for (size_t i 0; i group.size(); i) { for (size_t j i 1; j group.size(); j) { for (int d 0; d ND; d) { solver.addClause({ lit(group[i], d, true), lit(group[j], d, true) }); } } } }这里axis 0固定 x 得到一组平行线axis 1固定 yaxis 2固定 z三个方向正好覆盖六边形棋盘的三组主轴。line.size() 2是为了丢掉只包含一个格子的退化线因为单格约束由基数约束已经处理。宫的分组往往是题目配图里直接标好的色块常见做法是在源码里硬编码一个二维数组例如palace[7][6] {...}再逐个加入groups。不要把宫和直线方向混在一起枚举否则重复约束会让子句数膨胀到接近两倍。整个 CNF 的规模大致如下表单位是子句条数约束来源子句数量说明格子 at-least-one37每条 9 元格子 at-most-one1332每条 2 元三方向平行线约 2600与线长度相关宫每宫约 36按 6 格一组计算变量总数固定为 37×9333子句总数稳定在 4000 到 5000 之间。这个规模用裸手写 DPLL 完全可以实时返回结果不需要引入 MiniSat 或 Glucose 这类外部求解器。3. C 求解器源码拆解从 DPLL 主干到输入解析3.1 源码文件如何划分课程设计的 C 源码通常不用单文件堆完我一般拆成三个部分main.cpp负责读题、调用求解、写结果cnf.cpp/h封装变量、子句和约束组生成solver.cpp/h维护 DPLL 主循环、单元传播和回溯。数据流是文本线索 → 添加基数约束、组约束、单子句 →search()→ 根据assign回填棋盘。下面这个solvePuzzle函数把步骤串起来bool solvePuzzle(const std::vectorchar clue, std::vectorint solution, Solver solver) { // 1. 每个格子恰好一个数字 for (int c 0; c NC; c) { solver.addClause(makeAtLeastOne(c)); for (auto bin : makeAtMostOne(c)) solver.addClause(bin); } // 2. 所有直线组和宫组 for (auto g : buildLineGroups()) addGroupAtMostOne(solver, g); for (auto g : buildPalaceGroups()) addGroupAtMostOne(solver, g); // 3. 已知线索 for (int c 0; c NC; c) { if (clue[c] ! .) { solver.addClause({ lit(c, clue[c] - 1) }); } } if (!solver.search()) return false; solution.assign(NC, 0); for (int c 0; c NC; c) { for (int d 0; d ND; d) { if (solver.value(lit(c, d)) 1) { solution[c] d 1; } } } return true; }线索格子的处理是给一条单子句例如已知第 3 格是数字 5就加lit(3, 4)。SAT 求解器会自然传播出其他格子赋值不需要单独写“数字 5 不能出现在同行其他格”这种手工规则因为组内互斥子句已经覆盖。3.2 DPLL 主干单元传播如何避免重复扫描一个课程设计能接受的 DPLL 至少要有两个能力单元传播一次扫完所有子句以及回溯时只撤销当前决策层。朴素实现如果每递归一层都重新扫描全部子句会导致大量无用功。这里的做法是用trail记录每次赋值的字面量配合mark做回滚。struct Solver { int numVars; std::vectorstd::vectorint clauses; std::vectorint assign; // 0未赋值, 1真, -1假 std::vectorint trail; // 记录赋值字面量 void rollback(int mark) { while ((int)trail.size() mark) { int l trail.back(); trail.pop_back(); assign[std::abs(l)] 0; } } bool unitPropagate() { bool changed true; while (changed) { changed false; for (const auto c : clauses) { int unset 0, last 0; bool sat false; for (int l : c) { int val assign[std::abs(l)]; if (val 0) { unset; last l; } else if ((l 0 val 1) || (l 0 val -1)) { sat true; break; } } if (sat) continue; if (unset 0) return false; if (unset 1) { assign[std::abs(last)] last 0 ? 1 : -1; trail.push_back(last); changed true; } } } return true; } // ... };单元传播的while (changed)非常关键。一次扫描中新赋值的单子句可能让另一条子句变成新的单元子句必须继续扫描直到没有新赋值产生。很多 C 初版实现只在for循环里过一遍就返回结果该传播的变量没传播出现“明明有解却找不到”的假 UNSAT。递归搜索部分bool search() { if (!unitPropagate()) return false; bool complete true; for (int v 1; v numVars; v) { if (assign[v] 0) { complete false; break; } } if (complete) return true; int v pickBranch(); int mark trail.size(); assign[v] 1; trail.push_back(v); if (search()) return true; rollback(mark); assign[v] -1; trail.push_back(-v); if (search()) return true; rollback(mark); return false; }注意在尝试第二个分支前必须先rollback(mark)否则assign[v]-1会直接覆盖在第一分支的赋值上回溯时再把assign[v]清成 0第一个分支的传播结果就没有被彻底撤销。手动用 trail 而不是递归参数传递赋值向量好处是回滚复杂度与分支规模成正比。3.3 分支变量选择从朴素下标到计分函数pickBranch()是优化空间最大的地方。最简单的第一个未赋值变量就能跑通所有题干样例但遇到需要回溯的硬题会慢不少。将选择逻辑抽成独立函数方便后面换启发式。int pickBranch() { for (int v 1; v numVars; v) { if (assign[v] 0) return v; } return -1; }这个版本的优点是确定性强调试时容易复现。缺点是完全没有利用子句结构典型的行为是先穷举下标小的变量导致大量无意义分支。后面第四章会把它替换成基于子句权重的计分方式。4. 分支启发式与性能调参VSIDS 为什么比朴素选择快4.1 编译命令和基准测试方法本地直接编译运行时我习惯加上-O2 -stdc17 -DNDEBUG。课程设计源码里如果带了大量assert保留在 Release 里会拖慢传播循环。g -O2 -stdc17 -DNDEBUG main.cpp solver.cpp -o hexsat ./hexsat tests/hard_01.txt测试集建议从课程设计文档里抽取至少 20 道题简单题用来验证正确性硬题用来观察回溯次数。可以给程序加一个--stats参数输出传播次数和回溯次数而不是只输出求解时间因为时间在同一台机器上受负载影响波动大回溯次数是稳定指标。4.2 三种分支启发式的实测对比我拿一个 37 格、需要 4 次决策以上回溯的题目分别跑三个版本第一个未赋值变量、Jeroslow-Wang、VSIDS。JW 启发式对每条未满足子句中的未赋值变量累计权重权重取2^{-|clause|}短子句权重大。VSIDS 则是维护每个变量的浮点分数冲突时给冲突子句里的相关变量加分同时全局分数按固定比例衰减。分支策略回溯次数实现难度硬题耗时第一个未赋值变量1318低386msJeroslow-Wang452中96msVSIDS衰减 0.95217中高38ms回看数据朴素选择大部分时间浪费在把整个变量空间试一遍而 VSIDS 会在早期聚焦到高频冲突变量上。课程设计实验报告里如果能画出这条曲线比贴十行代码更有说服力。VSIDS 的更新逻辑本身很短std::vectordouble score(numVars 1, 0.0); // 每产生一次冲突对冲突子句中的字面量变量加分 for (int l : conflictClause) { score[std::abs(l)] 1.0; } // 每处理一次冲突后全局衰减让旧分数的影响逐步降低 for (int v 1; v numVars; v) { score[v] * 0.95; }衰减系数 0.95 表示大约 20 次冲突后旧分数会折半这是 MiniSat 风格比较常用的参数。如果公式里变量极多可以把衰减系数调到 0.9让历史权重降得更快如果题目贴近 SAT 竞赛的大公式0.99 更稳妥。对蜂窝数独这种 333 变量的小公式0.95 和 0.9 差别不大但千万别去掉衰减否则早期冲突的变量会一直霸占最高分分支方向被锁死在局部。4.3 子句学习要不要做坦白说37 格蜂窝数独不需要子句学习也能解完课程设计所有测试点我的实现里 20 道题最慢也不超过 1 秒。但在实验报告里可以写清楚边界如果把棋盘半径从 4 扩大到 5格子数从 37 涨到 61变量变成 549没有子句学习的 DPLL 在遇到精心构造的硬题时会指数爆炸。子句学习本质上是从冲突中提取一条蕴含式作为新子句加进子句库阻断后续重复走同一段死路。课程设计阶段不实现学习完全合理但赋值回退时要注意不能为了加学习子句破坏原有 trail 顺序。一个代价很小的折中方案是保留纯 DPLL只记录当前最长回溯深度用这个深度作为报告里的“搜索复杂度指标”。这比硬塞一个不完整的 CDCL 实现更安全。5. 解合法性校验与唯一性判断排错实录5.1 独立校验器不要复用生成器的分组函数很容易犯的一个错误是校验器直接调用buildLineGroups()再用同一份分组结果验证。这样如果分组生成逻辑本身写错了求解器和校验器同时错成一样的测试会给出极有误导性的“正确”。我的做法是在校验器里只从棋盘文本重新解析约束不经过 C 里的分组数组。bool verifySolution(const std::vectorstd::vectorint groups, const std::vectorint solution) { if ((int)solution.size() ! NC) return false; for (const auto group : groups) { bool seen[10] {}; for (int c : group) { int d solution[c]; if (d 1 || d 9) return false; if (seen[d]) return false; seen[d] true; } } return true; }每一个约束组单独开一个seen[10]重复数字直接返回 false。对 37 格棋盘来说复杂度是 O(总约束格数)一次校验在毫秒级。把这道函数接入单元测试每次修改源码后跑一遍能挡掉大量低级错误。5.2 判断唯一解否定原解再求解课程设计文档里的题目一般都会说明解是否唯一但如果你自己生成测试数据需要验证。找到第一个解后构造一条长子句原解中每个取真的变量在新子句里全部取反。这条子句的意思是“禁止整个赋值模式重现”然后重新调用search()。std::vectorint forbid; for (int c 0; c NC; c) { int d solution[c]; forbid.push_back(lit(c, d - 1, true)); } solver.addClause(forbid); if (solver.search()) { std::cout multiple solutions std::endl; } else { std::cout unique std::endl; }注意这里要复用同一个 Solver 实例因为前面的传播状态和子句库都在里面。添加否定子句之后如果返回 SAT说明存在第二个合法解如果 UNSAT则唯一。别忘了解可能不止一个需要统计数量时就循环“找到解 → 否定它 → 继续找”。5.3 三个最容易让 C 实现翻车的细节第一个坑是 Cube 坐标映射表写错。coordToId里插入了不在棋盘内的点或者少插了边缘格导致groups里出现两个指向同一物理格子的编号校验器也会跟着错。排错办法是在构建完coordToId后立刻assert(NC 37)每条约束组生成后检查格子编号不超过NC。第二个坑是单元传播只扫一遍子句。我之前有一版propagate只做单次 for 循环结果某些题目返回 UNSAT。排查时打印每个子句的赋值状态才发现新赋值的字面量没有触发后序子句的传播。改成while(changed)后问题消失。第三个坑是 VSIDS 分数没有在回溯时回滚。VSIDS 的加分发生在冲突时刻回溯不应该把分数退回去因为历史冲突信息是全局有效信息。如果你在rollback里顺手把score也恢复等于放弃了所有学习效果性能会掉回朴素策略。调试时看到回溯次数变多先检查是不是动了不该动的全局状态。最后VSCode 调试 C 时在tasks.json里加上-g -fsanitizeaddress用 GDB 跑一遍硬题样例没有崩溃再用 Release 参数编译再测性能。intelliSenseMode设置成gcc-x64可以减少大量误报特别是std::mapstd::tupleint,int,int,int这类嵌套模板配置不对会让语法高亮和补全全部失效。本文还有配套的精品资源点击获取