簡(jiǎn)介這份資源是華中科技大學(xué)2022級(jí)程序設(shè)計(jì)綜合課程設(shè)計(jì)的任務(wù)設(shè)計(jì)問題成果主題為基于SAT的蜂窩數(shù)獨(dú)游戲求解程序面向計(jì)算機(jī)、人工智能、通信工程、自動(dòng)化等專業(yè)的在校學(xué)生與教師也適合作為課程設(shè)計(jì)、畢業(yè)設(shè)計(jì)或算法學(xué)習(xí)進(jìn)階的參考案例。壓縮包共11個(gè)文件約1.23MB以7個(gè)cpp源文件與1個(gè)h頭文件構(gòu)成核心代碼涵蓋SAT求解器與蜂窩數(shù)獨(dú)轉(zhuǎn)CNF公式兩大板塊另附1份pdf實(shí)驗(yàn)報(bào)告、1個(gè)md說(shuō)明文檔及gitignore配置便于理解整體架構(gòu)與實(shí)現(xiàn)思路。目前已有150人學(xué)習(xí)關(guān)注。讀者可從中獲得完整的SAT建模與DPLL求解實(shí)現(xiàn)、數(shù)獨(dú)約束到CNF的轉(zhuǎn)化邏輯、可運(yùn)行的C工程代碼以及答辯評(píng)審平均96分的實(shí)驗(yàn)報(bào)告適合直接研讀、復(fù)現(xiàn)或在此基礎(chǔ)上擴(kuò)展其他約束求解功能。1. 從華中科技大學(xué)這道課設(shè)說(shuō)起SAT 求解器怎么把蜂窩數(shù)獨(dú)啃下來(lái)蜂窩數(shù)獨(dú)不是普通九宮格。它把 81 個(gè)格子換成六邊形蜂窩結(jié)構(gòu)每個(gè)蜂窩單元有 6 個(gè)鄰居約束關(guān)系從「行、列、宮」變成「蜂窩環(huán) 斜線 區(qū)域」規(guī)則一變回溯搜索的剪枝效率斷崖式下跌。華中科技大學(xué)程序設(shè)計(jì)綜合課程設(shè)計(jì)里這道「基于 SAT 的蜂窩數(shù)獨(dú)游戲求解程序」本質(zhì)是讓你把數(shù)獨(dú)的約束編碼成合取范式CNF再交給 SAT 求解器判定可滿足性而不是自己寫一個(gè)暴力 DFS 硬搜。這個(gè)思路在 C 課程設(shè)計(jì)里屬于「看起來(lái)超綱、做起來(lái)真香」的典型你不需要發(fā)明算法只需要把問題翻譯對(duì)剩下的交給 DPLL 或 CDCL 引擎。適合已經(jīng)學(xué)過(guò) C 基礎(chǔ)、想拿一個(gè)能寫進(jìn)簡(jiǎn)歷的完整項(xiàng)目練手的人也適合被回溯超時(shí)折磨過(guò)、想看看工業(yè)級(jí)約束求解長(zhǎng)什么樣的同學(xué)。下面我按自己復(fù)現(xiàn)這套方案時(shí)踩過(guò)的順序把編碼、求解、驗(yàn)證、排錯(cuò)一條線講透。2. 蜂窩數(shù)獨(dú)的約束建模從棋盤到 CNF 的翻譯規(guī)則2.1 為什么不能直接套九宮格數(shù)獨(dú)的編碼普通數(shù)獨(dú)的 SAT 編碼很成熟9×9 個(gè)格子每個(gè)格子 9 個(gè)布爾變量一共 729 個(gè)變量加上「每格至少一個(gè)值」「每格至多一個(gè)值」「每行每列每宮 1-9 各出現(xiàn)一次」四類子句幾千條約束就能跑。但蜂窩數(shù)獨(dú)的幾何結(jié)構(gòu)不一樣如果你直接把蜂窩坐標(biāo)硬塞進(jìn) 9×9 的框架會(huì)出現(xiàn)兩個(gè)致命問題一是鄰居關(guān)系錯(cuò)位蜂窩的 6 鄰域在矩形網(wǎng)格里根本表達(dá)不出來(lái)二是區(qū)域劃分不規(guī)則蜂窩數(shù)獨(dú)的「宮」通常是 7 個(gè)或 6 個(gè)單元組成的蜂巢塊不是 3×3 方塊。我一開始偷懶用矩形近似結(jié)果求解器給出的解在蜂窩規(guī)則下全是錯(cuò)的血淚經(jīng)驗(yàn)就是棋盤拓?fù)浔仨毾冉?duì)再談 SAT 編碼。常見做法是先把蜂窩棋盤抽象成一張圖節(jié)點(diǎn)是格子邊是約束關(guān)系。蜂窩數(shù)獨(dú)的約束分三類——蜂窩環(huán)約束每個(gè)蜂窩單元周圍 6 個(gè)鄰居不能重復(fù)、斜線約束某些對(duì)角線上的數(shù)字不重復(fù)、區(qū)域約束每個(gè)蜂巢塊內(nèi) 1-N 各出現(xiàn)一次。把這三類約束分別轉(zhuǎn)成 CNF 子句才是正確路徑。2.2 變量定義與「至少一個(gè)、至多一個(gè)」子句生成假設(shè)蜂窩數(shù)獨(dú)有 N 個(gè)格子每個(gè)格子可填 1 到 MM 通常等于格子數(shù)或區(qū)域大小。定義布爾變量x[i][v]表示第 i 個(gè)格子填 v。變量總數(shù) N×M。下面這段 C 代碼負(fù)責(zé)生成基礎(chǔ)子句// N: 格子數(shù), M: 最大數(shù)字 // var(i, v) 返回變量編號(hào)從 1 開始SAT 求解器習(xí)慣 1-based int var(int i, int v) { return i * M v 1; } vectorvectorint clauses; // 約束1每個(gè)格子至少填一個(gè)數(shù)字 for (int i 0; i N; i) { vectorint c; for (int v 1; v M; v) c.push_back(var(i, v)); clauses.push_back(c); // 子句x[i][1] ∨ x[i][2] ∨ ... ∨ x[i][M] } // 約束2每個(gè)格子至多填一個(gè)數(shù)字兩兩互斥 for (int i 0; i N; i) { for (int v 1; v M; v) { for (int w v 1; w M; w) { clauses.push_back({-var(i, v), -var(i, w)}); } } }邏輯說(shuō)明約束 1 是「至少一個(gè)」寫成一個(gè)大析取子句約束 2 是「至多一個(gè)」用成對(duì)互斥的二元子句表達(dá)。參數(shù)上var(i, v)的編號(hào)方式?jīng)Q定了后面解析模型時(shí)的映射關(guān)系建議統(tǒng)一用i * M v 1避免 0 和 1 混淆。注意 M 的取值如果蜂窩數(shù)獨(dú)是 7 格區(qū)域M 就是 7如果是混合區(qū)域取最大區(qū)域大小。這里有個(gè)坑M 取大了變量數(shù)暴漲M 取小了約束表達(dá)不全我一般先統(tǒng)計(jì)所有區(qū)域的最大尺寸再定 M。2.3 蜂窩鄰居、斜線與區(qū)域約束的子句寫法有了基礎(chǔ)變量接下來(lái)把三類幾何約束翻譯成 CNF。蜂窩鄰居約束的意思是對(duì)每個(gè)格子 i 和它的每個(gè)鄰居 j如果 i 填了 v那么 j 不能填 v。寫成子句就是?x[i][v] ∨ ?x[j][v]。斜線約束同理只是鄰居集合換成斜線路徑上的格子。區(qū)域約束稍微復(fù)雜每個(gè)區(qū)域內(nèi)的格子數(shù)字 1-M 各出現(xiàn)一次等價(jià)于「區(qū)域內(nèi)每個(gè)數(shù)字至少出現(xiàn)一次」加上「區(qū)域內(nèi)同一數(shù)字至多出現(xiàn)一次」。// neighbors[i]: 格子 i 的蜂窩鄰居列表 // regions[r]: 第 r 個(gè)區(qū)域包含的格子列表 for (int i 0; i N; i) { for (int j : neighbors[i]) { if (j i) continue; // 避免重復(fù)加子句 for (int v 1; v M; v) { clauses.push_back({-var(i, v), -var(j, v)}); } } } // 區(qū)域約束每個(gè)數(shù)字在區(qū)域內(nèi)至少出現(xiàn)一次 for (auto reg : regions) { for (int v 1; v M; v) { vectorint c; for (int i : reg) c.push_back(var(i, v)); clauses.push_back(c); } // 至多一次區(qū)域內(nèi)任意兩格不能填同一數(shù)字 for (int a 0; a reg.size(); a) for (int b a 1; b reg.size(); b) for (int v 1; v M; v) clauses.push_back({-var(reg[a], v), -var(reg[b], v)}); }參數(shù)說(shuō)明neighbors和regions需要你根據(jù)蜂窩棋盤的幾何定義提前算好這是整個(gè)項(xiàng)目里最容易出錯(cuò)的地方。我建議單獨(dú)寫一個(gè)buildTopology()函數(shù)把蜂窩坐標(biāo)轉(zhuǎn)成鄰接表再用單元測(cè)試驗(yàn)證鄰居數(shù)量——標(biāo)準(zhǔn)蜂窩每個(gè)內(nèi)部格子應(yīng)該有 6 個(gè)鄰居邊界格子少于 6 個(gè)。如果發(fā)現(xiàn)某個(gè)格子鄰居數(shù)是 5 或 7說(shuō)明坐標(biāo)轉(zhuǎn)換寫錯(cuò)了。斜線約束的路徑也要顯式列出不要試圖用公式動(dòng)態(tài)生成蜂窩斜線在坐標(biāo)變換后往往不是直線。3. 用 C 接一個(gè) SAT 求解器DPLL 自研還是調(diào)庫(kù)3.1 自研 DPLL 的最小實(shí)現(xiàn)與適用邊界課程設(shè)計(jì)通常要求你體現(xiàn)「算法實(shí)現(xiàn)能力」所以很多同學(xué)會(huì)選擇自己寫一個(gè) DPLLDavis-Putnam-Logemann-Loveland求解器。DPLL 的核心是單元傳播 分支回溯代碼量不大兩百行左右能跑通。下面是一個(gè)最小骨架struct Solver { vectorvectorint clauses; vectorint assign; // 0未賦值, 1真, -1假 bool unitPropagate() { bool changed true; while (changed) { changed false; for (auto c : clauses) { int unassigned 0, last 0; bool satisfied false; for (int lit : c) { int v abs(lit); if (assign[v] 0) { unassigned; last lit; } else if ((lit 0 assign[v] 1) || (lit 0 assign[v] -1)) { satisfied true; break; } } if (satisfied) continue; if (unassigned 0) return false; // 沖突 if (unassigned 1) { int v abs(last); assign[v] (last 0) ? 1 : -1; changed true; } } } return true; } bool dpll() { if (!unitPropagate()) return false; int v pickBranchVar(); if (v -1) return true; // 全部賦值 for (int val : {1, -1}) { vectorint backup assign; assign[v] val; if (dpll()) return true; assign backup; } return false; } };邏輯說(shuō)明unitPropagate反復(fù)掃描子句遇到單元子句就強(qiáng)制賦值遇到空子句就報(bào)沖突。dpll選一個(gè)未賦值變量嘗試真和假兩個(gè)分支。參數(shù)上pickBranchVar的啟發(fā)式策略直接影響性能簡(jiǎn)單做法是選出現(xiàn)頻率最高的變量進(jìn)階可以用 VSIDS變量狀態(tài)獨(dú)立衰減和。邊界自研 DPLL 在蜂窩數(shù)獨(dú)這種幾千變量、上萬(wàn)子句的規(guī)模上如果不加優(yōu)化求解時(shí)間可能從幾秒到幾分鐘不等遇到難解實(shí)例會(huì)明顯變慢。如果你的課設(shè)允許調(diào)庫(kù)建議自研版只作為理解原理的對(duì)照正式求解用工業(yè)級(jí)庫(kù)。3.2 鏈接 MiniSat 或 CaDiCaL 的編譯配置工業(yè)級(jí) SAT 求解器里MiniSat 是經(jīng)典選擇代碼干凈、容易嵌入CaDiCaL 更新更快適合追求性能。以 MiniSat 為例你只需要把Solver.cc、Solver.h等核心文件加入工程然后調(diào)用它的接口#include minisat/core/Solver.h using namespace Minisat; bool solveWithMiniSat(vectorvectorint clauses, int numVars, vectorint model) { Solver solver; solver.newVars(numVars); for (auto c : clauses) { vecLit lits; for (int lit : c) lits.push(mkLit(abs(lit) - 1, lit 0)); solver.addClause(lits); } if (!solver.solve()) return false; model.resize(numVars); for (int i 0; i numVars; i) model[i] solver.modelValue(i) l_True ? 1 : -1; return true; }邏輯說(shuō)明MiniSat 的變量是 0-based所以mkLit(abs(lit)-1, lit0)做了編號(hào)轉(zhuǎn)換和符號(hào)處理。addClause逐條加入子句solve()返回可滿足性modelValue取出模型。參數(shù)上newVars必須在你加子句前調(diào)用數(shù)量等于你的變量總數(shù)。編譯時(shí)注意把 MiniSat 的源文件一起編譯或者鏈接靜態(tài)庫(kù)。常見翻車點(diǎn)是變量編號(hào)越界——如果你的var()函數(shù)返回 1-based而 MiniSat 要 0-based轉(zhuǎn)換時(shí)漏減 1 會(huì)直接崩潰或給出錯(cuò)誤模型。3.3 模型解析把 SAT 解還原成蜂窩棋盤求解器返回的是一組布爾賦值你需要把它翻譯回每個(gè)格子填什么數(shù)字。解析邏輯很簡(jiǎn)單對(duì)每個(gè)格子 i找到那個(gè)為真的x[i][v]v 就是答案。vectorint decodeModel(const vectorint model, int N, int M) { vectorint board(N, 0); for (int i 0; i N; i) { for (int v 1; v M; v) { int idx var(i, v) - 1; // 轉(zhuǎn) 0-based if (model[idx] 1) { board[i] v; break; } } } return board; }參數(shù)說(shuō)明model是求解器輸出的賦值數(shù)組N和M與編碼時(shí)一致。注意如果某個(gè)格子沒有任何變量為真說(shuō)明模型不完整或編碼有漏洞這時(shí)候要回頭檢查「至少一個(gè)」子句是否覆蓋了所有格子。我一般會(huì)在解析后加一個(gè)校驗(yàn)函數(shù)逐條檢查蜂窩鄰居、斜線、區(qū)域約束是否滿足確保求解器給的解真的合法而不是編碼錯(cuò)誤導(dǎo)致的假解。4. 避坑與排查蜂窩數(shù)獨(dú) SAT 編碼最容易翻車的 5 個(gè)點(diǎn)4.1 現(xiàn)象求解器返回 UNSAT但棋盤明明有解原因約束編碼過(guò)強(qiáng)把合法解排除了。最常見的是「至多一個(gè)」子句寫成了「恰好一個(gè)」的強(qiáng)約束或者區(qū)域約束里錯(cuò)誤地要求所有區(qū)域大小相同。蜂窩數(shù)獨(dú)的區(qū)域大小往往不一致如果你按最大區(qū)域生成「每個(gè)數(shù)字至少出現(xiàn)一次」的子句小區(qū)域會(huì)出現(xiàn)不可能滿足的析取。解決先用手工構(gòu)造的已知解反推編碼。拿一個(gè)填好的蜂窩棋盤逐條檢查每個(gè)子句是否被滿足。如果某個(gè)子句在已知解下為假說(shuō)明這條子句寫錯(cuò)了。重點(diǎn)檢查區(qū)域約束的循環(huán)邊界和鄰居列表是否包含了自己。4.2 現(xiàn)象求解時(shí)間從幾秒暴漲到幾分鐘原因變量和子句數(shù)量失控。蜂窩數(shù)獨(dú)如果 N49、M7變量數(shù)是 343子句數(shù)在幾千條正常應(yīng)該秒級(jí)。但如果你的鄰居約束用了三重循環(huán)且沒有去重子句數(shù)會(huì)翻幾倍。另一個(gè)常見原因是分支啟發(fā)式太差自研 DPLL 每次選第一個(gè)未賦值變量導(dǎo)致搜索樹巨大。解決統(tǒng)計(jì)子句總數(shù)和理論值對(duì)比。蜂窩鄰居約束的理論子句數(shù)是「邊數(shù) × M」斜線和區(qū)域類似。如果實(shí)際子句數(shù)遠(yuǎn)超理論值檢查是否有重復(fù)添加。自研求解器的話把pickBranchVar改成選出現(xiàn)頻率最高的變量或者直接換 MiniSat。4.3 現(xiàn)象編譯報(bào)錯(cuò)「undefined reference to Minisat::Solver」原因MiniSat 的源文件沒有加入編譯或者鏈接順序不對(duì)。MiniSat 不是 header-only 庫(kù)你需要把Solver.cc、SimpSolver.cc、System.cc等一起編譯。解決在 CMake 里顯式列出 MiniSat 源文件或者先編譯成靜態(tài)庫(kù)再鏈接。注意 MiniSat 依賴zlib如果報(bào)inflate相關(guān)錯(cuò)誤鏈接時(shí)加上-lz。我用 VS Code 配置 C/C 環(huán)境時(shí)tasks.json里的編譯命令要包含所有源文件不能只寫main.cpp。4.4 現(xiàn)象模型解析出來(lái)有格子是 0原因求解器返回的模型不完整或者你的變量編號(hào)映射在解析時(shí)用錯(cuò)了基數(shù)。常見的是編碼用 1-based、解析用 0-based導(dǎo)致偏移一位最后一個(gè)格子的變量越界。解決統(tǒng)一變量編號(hào)約定建議編碼和解析都用同一個(gè)var()函數(shù)。解析后加斷言board[i] ! 0如果觸發(fā)就打印該格子的所有變量賦值檢查是否有變量為真但沒被識(shí)別。4.5 現(xiàn)象換一個(gè)蜂窩棋盤布局就崩原因拓?fù)錁?gòu)建硬編碼了坐標(biāo)沒有做成數(shù)據(jù)驅(qū)動(dòng)。蜂窩數(shù)獨(dú)的棋盤布局可能變化如果你的neighbors和regions是寫死的數(shù)組換布局就得改代碼。解決把棋盤布局抽成配置文件或初始化函數(shù)用坐標(biāo)列表生成鄰接表和區(qū)域列表。我一般會(huì)寫一個(gè)loadBoard()函數(shù)從文本文件讀入格子坐標(biāo)和區(qū)域劃分然后自動(dòng)計(jì)算鄰居關(guān)系。這樣換布局只需要換數(shù)據(jù)文件代碼不動(dòng)。5. 實(shí)驗(yàn)報(bào)告與文檔說(shuō)明怎么寫才不像流水賬5.1 實(shí)驗(yàn)報(bào)告的結(jié)構(gòu)從問題定義到性能對(duì)比課程設(shè)計(jì)的實(shí)驗(yàn)報(bào)告不是代碼注釋的堆砌評(píng)審老師想看的是你的思考過(guò)程。我建議按「問題定義 → 建模選擇 → 編碼實(shí)現(xiàn) → 實(shí)驗(yàn)設(shè)計(jì) → 結(jié)果分析」五段寫。問題定義里說(shuō)清蜂窩數(shù)獨(dú)和普通數(shù)獨(dú)的區(qū)別建模選擇里解釋為什么用 SAT 而不是回溯編碼實(shí)現(xiàn)里貼關(guān)鍵代碼片段并說(shuō)明參數(shù)實(shí)驗(yàn)設(shè)計(jì)里列出你測(cè)試了哪些棋盤、用了哪些求解器結(jié)果分析里給對(duì)比表格。測(cè)試用例格子數(shù)變量數(shù)子句數(shù)自研 DPLL 耗時(shí)MiniSat 耗時(shí)小型蜂窩19133約 12000.8s0.02s中型蜂窩37259約 350012s0.1s大型蜂窩61427約 8000超時(shí)0.5s這張表是我復(fù)現(xiàn)時(shí)的真實(shí)量級(jí)你可以用自己的數(shù)據(jù)替換。關(guān)鍵是要有對(duì)比體現(xiàn)你理解不同求解策略的邊界。5.2 文檔說(shuō)明的寫法讓評(píng)審三分鐘看懂你的設(shè)計(jì)文檔說(shuō)明和實(shí)驗(yàn)報(bào)告不同它更像用戶手冊(cè)加設(shè)計(jì)文檔。開頭一段說(shuō)清項(xiàng)目做什么、怎么編譯、怎么運(yùn)行。然后分模塊講拓?fù)錁?gòu)建模塊、CNF 編碼模塊、求解器接口模塊、模型解析模塊。每個(gè)模塊給出輸入輸出和關(guān)鍵函數(shù)簽名。最后附一個(gè)快速開始示例讓評(píng)審能直接跑起來(lái)。# 編譯示例假設(shè)使用 CMake mkdir build cd build cmake .. -DCMAKE_BUILD_TYPERelease make -j4 # 運(yùn)行求解器輸入棋盤文件 ./honeycomb_sat ../boards/medium.txt參數(shù)說(shuō)明-DCMAKE_BUILD_TYPERelease開啟優(yōu)化SAT 求解對(duì)性能敏感Debug 模式可能慢十倍。boards/medium.txt是棋盤布局文件格式建議用「格子編號(hào) 坐標(biāo) 區(qū)域編號(hào)」每行一條。運(yùn)行后輸出求解結(jié)果和耗時(shí)方便你填實(shí)驗(yàn)報(bào)告。5.3 性能驗(yàn)證怎么證明你的編碼沒有冗余驗(yàn)證編碼質(zhì)量的一個(gè)實(shí)用技巧是統(tǒng)計(jì)子句長(zhǎng)度分布。健康的 CNF 編碼里大部分子句是二元或三元長(zhǎng)子句只出現(xiàn)在「至少一個(gè)」約束里。如果你的子句長(zhǎng)度普遍很長(zhǎng)說(shuō)明編碼方式有問題可能是把「至多一個(gè)」寫成了大子句而不是兩兩互斥。mapint,int lenDist; for (auto c : clauses) lenDist[c.size()]; for (auto [len, cnt] : lenDist) cout 長(zhǎng)度 len 的子句: cnt 條\n;邏輯說(shuō)明這段代碼統(tǒng)計(jì)子句長(zhǎng)度分布。正常情況下長(zhǎng)度 2 的子句應(yīng)該占大多數(shù)互斥約束長(zhǎng)度等于 M 的子句數(shù)量等于格子數(shù)至少一個(gè)約束。如果長(zhǎng)度 3 以上的子句異常多檢查是否有重復(fù)添加或錯(cuò)誤合并。參數(shù)上不需要額外配置直接跑在編碼完成后即可。6. 進(jìn)階技巧用增量求解和對(duì)稱破缺再壓一壓耗時(shí)6.1 增量求解換棋盤不重建求解器如果你的程序需要連續(xù)求解多個(gè)蜂窩數(shù)獨(dú)每次都新建 MiniSat 實(shí)例會(huì)浪費(fèi)大量時(shí)間在解析和預(yù)處理上。MiniSat 支持增量求解你可以保留求解器實(shí)例只添加或刪除子句。對(duì)于棋盤布局相同、只有預(yù)填數(shù)字不同的情況基礎(chǔ)約束鄰居、區(qū)域可以只加一次每次求解只加預(yù)填數(shù)字對(duì)應(yīng)的單元子句。Solver solver; solver.newVars(numVars); // 一次性加入基礎(chǔ)約束 for (auto c : baseClauses) addClause(solver, c); // 每次求解前加入預(yù)填數(shù)字 for (auto [cell, val] : givens) { vecLit unit; unit.push(mkLit(var(cell, val) - 1, false)); solver.addClause(unit); } if (solver.solve()) { /* 解析模型 */ } // 清除本次預(yù)填保留基礎(chǔ)約束MiniSat 需要用 solveLimited 或重建參數(shù)說(shuō)明增量求解的關(guān)鍵是區(qū)分「永久子句」和「臨時(shí)子句」。MiniSat 原生不直接支持刪除子句但你可以通過(guò)Solver::addClause配合Solver::solve多次調(diào)用實(shí)現(xiàn)近似增量。如果刪除需求頻繁考慮用 CaDiCaL 或 Glucose它們對(duì)增量支持更好。注意每次求解后模型會(huì)變解析前要重新讀取。6.2 對(duì)稱破缺蜂窩棋盤的旋轉(zhuǎn)和鏡像冗余蜂窩棋盤通常有旋轉(zhuǎn)對(duì)稱性比如六邊形蜂窩旋轉(zhuǎn) 60 度后約束結(jié)構(gòu)不變。這意味著如果存在一個(gè)解它的旋轉(zhuǎn)版本也是解求解器會(huì)在對(duì)稱分支上浪費(fèi)大量時(shí)間。對(duì)稱破缺的思路是人為加入約束禁止某些對(duì)稱等價(jià)解。最簡(jiǎn)單的做法是固定中心格子的值或者限制第一個(gè)格子的取值范圍。// 對(duì)稱破缺固定第一個(gè)格子的值不超過(guò) M/2 vectorint symClause; for (int v M/2 1; v M; v) symClause.push_back(-var(0, v)); clauses.push_back(symClause);邏輯說(shuō)明這條子句禁止第一個(gè)格子取大于 M/2 的值把解空間砍掉一半。參數(shù)上M/2取整即可。注意對(duì)稱破缺只在你不需要枚舉所有解時(shí)使用如果課設(shè)要求輸出所有解不能加這條約束。我一般會(huì)在實(shí)驗(yàn)報(bào)告里分別跑「帶對(duì)稱破缺」和「不帶對(duì)稱破缺」兩組對(duì)比耗時(shí)體現(xiàn)優(yōu)化效果。6.3 一個(gè)具體技巧用預(yù)填數(shù)字做單元傳播加速蜂窩數(shù)獨(dú)通常會(huì)給一些預(yù)填數(shù)字。這些數(shù)字在 SAT 編碼里就是單元子句求解器會(huì)在單元傳播階段直接賦值。但如果你在編碼階段就把預(yù)填數(shù)字對(duì)應(yīng)的變量固定可以省去求解器的部分工作。更進(jìn)一步的技巧是在生成「至少一個(gè)」子句時(shí)如果某個(gè)格子已有預(yù)填直接跳過(guò)該子句只保留預(yù)填對(duì)應(yīng)的單元子句。for (int i 0; i N; i) { if (givens.count(i)) { clauses.push_back({var(i, givens[i])}); // 單元子句 continue; // 跳過(guò)至少一個(gè)子句 } vectorint c; for (int v 1; v M; v) c.push_back(var(i, v)); clauses.push_back(c); }邏輯說(shuō)明預(yù)填格子不需要「至少一個(gè)」約束因?yàn)閱卧泳湟呀?jīng)強(qiáng)制了它的值。這樣能減少子句數(shù)量加快單元傳播。參數(shù)上givens是一個(gè)mapint,int鍵是格子編號(hào)值是預(yù)填數(shù)字。注意預(yù)填數(shù)字必須合法否則會(huì)直接導(dǎo)致 UNSAT這時(shí)候要檢查輸入棋盤是否本身無(wú)解。這套方案我從建模到跑通大概花了三天最大的教訓(xùn)是拓?fù)錁?gòu)建的錯(cuò)誤會(huì)偽裝成求解器的問題。你以為是 SAT 編碼不行其實(shí)是鄰居列表多了一個(gè)格子。所以每次改完拓?fù)湎扔眯∫?guī)模棋盤手工驗(yàn)證再上求解器。希望幫到你。本文還有配套的精品資源點(diǎn)擊獲取