1. 從“邏輯謎題”到“計(jì)算基石”SAT問題究竟是什么如果你玩過數(shù)獨(dú)或者嘗試過那種“誰說了真話誰說了假話”的邏輯推理題那你其實(shí)已經(jīng)和布爾可滿足性問題打過交道了。SAT全稱布爾可滿足性問題聽起來學(xué)術(shù)味十足但它本質(zhì)上問的是一個(gè)非常樸素的問題給定一個(gè)由布爾變量只能取真或假和邏輯運(yùn)算符與、或、非構(gòu)成的邏輯公式是否存在一組對(duì)這些變量的賦值使得整個(gè)公式的最終結(jié)果為“真”舉個(gè)例子一個(gè)簡(jiǎn)單的公式可能是(A 或 B) 與 (非A 或 C)。SAT問題就是問我們能不能給A、B、C這三個(gè)變量分配真值True或False讓整個(gè)括號(hào)里的式子最終算出來是True你可以自己試一下比如讓AFalse BTrue CTrue代入計(jì)算(False 或 True) True(非False 或 True) (True 或 True) True最后True 與 True True。看我們找到了一組解所以這個(gè)公式是“可滿足的”。這個(gè)看似簡(jiǎn)單的“邏輯謎題”卻是計(jì)算機(jī)科學(xué)理論中一個(gè)里程碑式的存在。它是第一個(gè)被證明的NP完全問題。這意味著什么簡(jiǎn)單來說目前沒有已知的、能在所有情況下都快速多項(xiàng)式時(shí)間內(nèi)解決SAT問題的通用算法但同時(shí)成千上萬的實(shí)際問題從集成電路設(shè)計(jì)、軟件驗(yàn)證、人工智能規(guī)劃到排班調(diào)度都可以被轉(zhuǎn)化為SAT問題來求解。因此SAT求解器成為了一個(gè)強(qiáng)大的“通用計(jì)算引擎”你不需要為每個(gè)新問題從頭發(fā)明算法只需要把它“編譯”成SAT公式然后丟給求解器就行。理解SAT不僅是理解一個(gè)理論概念更是掌握了一把解決眾多復(fù)雜實(shí)際問題的鑰匙。2. 問題的標(biāo)準(zhǔn)“接口”合取范式在深入求解算法之前我們必須先統(tǒng)一問題的“表達(dá)格式”。任意復(fù)雜的邏輯公式其形態(tài)千變?nèi)f化直接處理起來非常困難。為此學(xué)術(shù)界和工業(yè)界約定俗成地使用一種標(biāo)準(zhǔn)形式合取范式。CNF是“Conjunctive Normal Form”的縮寫中文叫合取范式。它的結(jié)構(gòu)非常規(guī)整由三層組成文字一個(gè)布爾變量或其否定。例如A和非A都是文字。子句由多個(gè)文字通過“或”連接而成的邏輯表達(dá)式。例如(A 或 非B 或 C)就是一個(gè)子句。子句的本質(zhì)是一個(gè)約束條件它要求其中至少有一個(gè)文字為真。公式整個(gè)CNF公式由多個(gè)子句通過“與”連接而成。例如(A 或 B) 與 (非A 或 C) 與 (非B 或 非C)。公式的整體為真要求每一個(gè)子句都必須為真。為什么CNF如此重要首先它提供了統(tǒng)一的、機(jī)器友好的輸入格式所有現(xiàn)代SAT求解器都接受CNF作為輸入。其次CNF的結(jié)構(gòu)清晰地揭示了SAT問題的本質(zhì)尋找一組賦值同時(shí)滿足所有約束子句。這非常像我們面對(duì)的現(xiàn)實(shí)問題必須同時(shí)滿足預(yù)算、時(shí)間、資源等多重限制條件。將任意公式轉(zhuǎn)化為CNF需要一些技巧核心是利用邏輯等價(jià)變換例如利用德·摩根定律和分配律。一個(gè)實(shí)用的方法是引入輔助變量。例如公式A 等價(jià)于 (B 且 C)直接轉(zhuǎn)化較復(fù)雜。我們可以引入一個(gè)新變量X來表示(B 且 C)然后將原公式等價(jià)地轉(zhuǎn)化為三個(gè)子句(非A 或 B)、(非A 或 C)、(A 或 非B 或 非C)再加上定義X的子句(非X 或 B)、(非X 或 C)、(X 或 非B 或 非C)和(A 或 非X)、(非A 或 X)。雖然變量增多了但結(jié)構(gòu)變成了規(guī)整的CNF便于求解器處理。注意在實(shí)際使用中我們通常不需要手動(dòng)進(jìn)行復(fù)雜的轉(zhuǎn)化。絕大多數(shù)編程語言或建模工具都提供了將高級(jí)約束自動(dòng)編譯成CNF的功能。理解CNF的意義在于當(dāng)求解器報(bào)錯(cuò)或性能不佳時(shí)你能知道它底層真正在處理的是什么。3. 經(jīng)典算法的智慧DPLL框架解析在SAT求解器的發(fā)展史上DPLL算法是一個(gè)奠基性的里程碑。它以三位發(fā)明者Davis, Putnam, Logemann, Loveland的名字命名。盡管后來的算法在它基礎(chǔ)上做了極大增強(qiáng)但DPLL的核心思想——深度優(yōu)先搜索結(jié)合確定性推理——仍然是現(xiàn)代求解器的骨架。DPLL算法可以看作一個(gè)遞歸的回溯搜索過程其核心是兩種簡(jiǎn)化策略和一種選擇策略3.1 單元傳播利用確定性的推理這是DPLL中最高效的步驟。如果一個(gè)子句中只有一個(gè)文字未被賦值其他文字都已賦值為假那么這個(gè)唯一的文字必須被賦值為真才能使該子句為真。這個(gè)被強(qiáng)制賦值的變量稱為“單元變量”這個(gè)過程就是單元傳播。例如假設(shè)我們有子句(A 或 非B)且我們已經(jīng)賦值B True。那么非B就是 False。此時(shí)為了使該子句為真A必須為 True。于是我們不必猜測(cè)可以直接推導(dǎo)出A True。這個(gè)推導(dǎo)可能會(huì)觸發(fā)新的單元傳播形成連鎖反應(yīng)極大地縮小搜索空間。3.2 純文字消除識(shí)別“無害”變量如果一個(gè)變量在整個(gè)公式的所有子句中都以同一種形式全是正出現(xiàn)或全是負(fù)出現(xiàn)出現(xiàn)那么這個(gè)變量就是一個(gè)“純文字”。例如變量A在所有出現(xiàn)的地方都是A從未出現(xiàn)過非A。那么我們可以直接將其賦值為真如果全是正出現(xiàn)或假如果全是負(fù)出現(xiàn)這不會(huì)使任何子句為假因?yàn)榘淖泳鋾?huì)立即被滿足。純文字消除是一個(gè)優(yōu)化它減少了需要決策的變量數(shù)量。3.3 決策與回溯搜索的核心當(dāng)單元傳播和純文字消除都無法再進(jìn)行時(shí)算法就面臨一個(gè)選擇需要為一個(gè)尚未賦值的變量猜測(cè)一個(gè)值比如選擇變量X先嘗試X True。這個(gè)選擇是“決策點(diǎn)”。算法會(huì)基于這個(gè)決策繼續(xù)向下進(jìn)行單元傳播。如果沿著這條路徑走下去最終導(dǎo)致了矛盾某個(gè)子句的所有文字都被賦值為假稱為“沖突”則說明當(dāng)前的決策是錯(cuò)的。算法需要“回溯”撤銷從這個(gè)決策點(diǎn)之后所做的所有賦值然后嘗試該變量的另一個(gè)賦值X False。如果兩個(gè)賦值都導(dǎo)致沖突則算法需要回溯到更早的決策點(diǎn)。3.4 DPLL的流程與局限標(biāo)準(zhǔn)的DPLL偽代碼流程如下持續(xù)進(jìn)行單元傳播和純文字消除直到無法進(jìn)行為止。如果所有子句都被滿足返回“可滿足”及當(dāng)前賦值。如果發(fā)現(xiàn)沖突有空子句則返回“沖突”。選擇一個(gè)未賦值的變量為其賦值決策然后遞歸調(diào)用步驟1。如果遞歸調(diào)用返回沖突則回溯嘗試該變量的另一個(gè)賦值。如果兩個(gè)賦值都導(dǎo)致沖突則回溯到上一個(gè)決策點(diǎn)。DPLL的強(qiáng)大在于它通過推理單元傳播減少了大量盲目的猜測(cè)。然而它的回溯是“時(shí)序回溯”即簡(jiǎn)單地回到上一個(gè)決策點(diǎn)。當(dāng)沖突的原因涉及多個(gè)早期決策時(shí)這種回溯方式非常低效會(huì)導(dǎo)致重復(fù)探索大量無效的搜索空間。正是為了克服這個(gè)缺陷更強(qiáng)大的CDCL算法應(yīng)運(yùn)而生。4. 現(xiàn)代求解器的引擎CDCL算法精講沖突驅(qū)動(dòng)子句學(xué)習(xí)算法是當(dāng)今所有高性能SAT求解器的核心。它在DPLL的框架上引入了三個(gè)革命性的機(jī)制子句學(xué)習(xí)、非時(shí)序回溯和變量活動(dòng)度啟發(fā)從而實(shí)現(xiàn)了性能的質(zhì)的飛躍。4.1 沖突分析與子句學(xué)習(xí)當(dāng)求解器在搜索中遇到?jīng)_突一個(gè)子句的所有文字都為假時(shí)CDCL不會(huì)像DPLL那樣簡(jiǎn)單地回溯了事。它會(huì)啟動(dòng)一個(gè)“沖突分析”過程。這個(gè)過程的目標(biāo)是找出導(dǎo)致當(dāng)前沖突的根本原因。具體做法是構(gòu)建一個(gè)“蘊(yùn)含圖”。圖中記錄了所有通過單元傳播產(chǎn)生的賦值及其原因是哪個(gè)子句的單元傳播導(dǎo)致了這次賦值。當(dāng)沖突發(fā)生時(shí)從沖突子句出發(fā)沿著蘊(yùn)含圖反向追溯找到那些為當(dāng)前沖突“負(fù)責(zé)”的早期決策變量。通過解析這些原因可以推導(dǎo)出一個(gè)新的子句這個(gè)子句是原有公式的邏輯推論但它直接刻畫了導(dǎo)致沖突的變量賦值組合。例如通過分析發(fā)現(xiàn)沖突是因?yàn)闆Q策ATrue,BFalse,CTrue共同導(dǎo)致的。那么學(xué)習(xí)到的新子句可能就是(非A 或 B 或 非C)。這個(gè)子句的意思是“A為真、B為假、C為真”這個(gè)組合不能再出現(xiàn)。這個(gè)新子句會(huì)被永久添加到問題中。4.2 基于學(xué)習(xí)子句的回溯學(xué)習(xí)到新子句后CDCL會(huì)根據(jù)這個(gè)子句進(jìn)行回溯。它計(jì)算這個(gè)新子句里在當(dāng)前的決策層級(jí)下除了最后一個(gè)被賦值的文字外其他文字是否都已賦值為假?；厮莸哪繕?biāo)決策層級(jí)就是倒數(shù)第二個(gè)文字被賦值時(shí)的層級(jí)。這種回溯不是按時(shí)間順序回到上一個(gè)決策點(diǎn)而是直接跳回到?jīng)_突根源所在的層級(jí)這被稱為“非時(shí)序回溯”或“智能回溯”。這樣做的好處是巨大的它不僅僅避免了一次沖突而是修剪了搜索空間中所有共享同一錯(cuò)誤根源的子樹學(xué)習(xí)到的子句在后續(xù)搜索中會(huì)持續(xù)發(fā)揮作用防止求解器再次踏入同一條河流。4.3 變量活動(dòng)度與決策啟發(fā)在CDCL中選擇哪個(gè)變量進(jìn)行下一次決策也有一套高效的啟發(fā)式策略——變量活動(dòng)度。其基本思想是在近期引發(fā)過沖突的變量更可能重要。每個(gè)變量都有一個(gè)“活動(dòng)度”分?jǐn)?shù)。每當(dāng)一個(gè)學(xué)習(xí)到的子句中包含了某個(gè)變量該變量的活動(dòng)度就會(huì)增加。在需要做決策時(shí)求解器傾向于選擇活動(dòng)度最高的未賦值變量。這類似于一種“經(jīng)驗(yàn)學(xué)習(xí)”經(jīng)常出現(xiàn)在矛盾核心的變量對(duì)問題是否可滿足可能起著關(guān)鍵作用優(yōu)先給它們賦值能更快地逼近核心矛盾或找到解。4.4 CDCL的工作流程結(jié)合以上機(jī)制CDCL的簡(jiǎn)化工作循環(huán)如下單元傳播持續(xù)進(jìn)行直到無法推導(dǎo)出新的賦值。沖突檢測(cè)如果發(fā)現(xiàn)沖突進(jìn)入沖突分析階段如果所有變量都已賦值且無沖突問題可滿足。沖突分析與學(xué)習(xí)分析沖突根源推導(dǎo)出一個(gè)新的學(xué)習(xí)子句并將其加入子句數(shù)據(jù)庫?；厮莞鶕?jù)學(xué)習(xí)子句執(zhí)行非時(shí)序回溯到適當(dāng)?shù)臎Q策層級(jí)。決策如果未解決根據(jù)變量活動(dòng)度啟發(fā)式選擇一個(gè)未賦值變量并為其賦值然后回到步驟1。這個(gè)“傳播-沖突-學(xué)習(xí)-回溯”的循環(huán)使得CDCL求解器能夠從錯(cuò)誤中高效學(xué)習(xí)動(dòng)態(tài)調(diào)整搜索方向從而能夠處理規(guī)模極其龐大數(shù)百萬變量、數(shù)千萬子句的工業(yè)級(jí)問題。5. 不止于理論SAT技術(shù)的實(shí)際應(yīng)用場(chǎng)景SAT求解器早已不是實(shí)驗(yàn)室里的玩具它已經(jīng)滲透到許多需要嚴(yán)格邏輯推理的工業(yè)領(lǐng)域。理解這些應(yīng)用場(chǎng)景能讓你更直觀地感受到它的威力。5.1 硬件設(shè)計(jì)與驗(yàn)證這是SAT最早也是最重要的應(yīng)用領(lǐng)域之一。等價(jià)性檢查比較兩個(gè)電路設(shè)計(jì)例如優(yōu)化前后的電路在功能上是否完全等價(jià)?？梢詫蓚€(gè)電路的輸入輸出關(guān)系用邏輯公式描述然后詢問“是否存在一種輸入使得兩個(gè)電路的輸出不同”這個(gè)問題可以轉(zhuǎn)化為SAT問題。如果SAT求解器返回“不可滿足”則證明兩個(gè)電路等價(jià)。模型檢測(cè)驗(yàn)證一個(gè)數(shù)字系統(tǒng)如一個(gè)芯片的控制器是否滿足某些時(shí)序邏輯規(guī)范。系統(tǒng)所有可能的狀態(tài)和轉(zhuǎn)換被編碼成一個(gè)巨大的邏輯公式規(guī)范被編碼為需要滿足的性質(zhì)。SAT求解器被用來搜索是否存在違反該性質(zhì)的狀態(tài)路徑。自動(dòng)測(cè)試模式生成為了測(cè)試制造出的芯片是否有缺陷需要生成特定的輸入向量測(cè)試模式。ATPG工具的核心引擎之一就是SAT求解器它被用來計(jì)算能夠激活特定故障并使其傳播到可觀測(cè)輸出端的輸入。5.2 軟件分析與安全符號(hào)執(zhí)行這是一種程序分析技術(shù)它不像普通執(zhí)行那樣使用具體值而是使用符號(hào)值作為輸入并將程序執(zhí)行路徑表示為符號(hào)表達(dá)式。在路徑分支點(diǎn)會(huì)產(chǎn)生路徑條件。使用SAT求解器可以判斷某條路徑是否可行路徑條件是否可滿足這對(duì)于發(fā)現(xiàn)程序深層漏洞如安全漏洞至關(guān)重要。反病毒與惡意代碼分析某些高級(jí)惡意代碼會(huì)使用混淆技術(shù)。分析人員可以將代碼的語義編碼為邏輯約束然后使用SAT求解器來推理可能的輸入輸出行為或嘗試進(jìn)行反混淆。5.3 人工智能與規(guī)劃自動(dòng)規(guī)劃給定初始狀態(tài)、目標(biāo)狀態(tài)和一系列可執(zhí)行的動(dòng)作規(guī)劃問題是尋找一個(gè)動(dòng)作序列使得能從初始狀態(tài)到達(dá)目標(biāo)狀態(tài)。經(jīng)典的規(guī)劃問題可以編碼為SAT問題其中變量表示“在時(shí)間步t命題p是否為真”或“在時(shí)間步t是否執(zhí)行動(dòng)作a”。通過逐步增加時(shí)間步的長度并調(diào)用SAT求解器可以找到滿足條件的最短計(jì)劃。知識(shí)推理在專家系統(tǒng)或描述邏輯中可以進(jìn)行一致性檢查知識(shí)庫是否自相矛盾和蘊(yùn)含查詢知識(shí)庫是否隱含某個(gè)事實(shí)這些都可以規(guī)約到SAT問題。5.4 其他趣味與實(shí)用領(lǐng)域密碼學(xué)分析哈希函數(shù)的抗碰撞性、尋找對(duì)稱密碼算法的密鑰等有時(shí)可以建模為SAT問題。數(shù)學(xué)謎題諸如數(shù)獨(dú)、N皇后、邏輯網(wǎng)格謎題等其規(guī)則可以很自然地編碼為CNF公式然后用SAT求解器秒解。排班與調(diào)度為員工排班、安排課程表、優(yōu)化物流路線等在加入各種約束后往往可以轉(zhuǎn)化為SAT或其擴(kuò)展問題。提示對(duì)于初學(xué)者從解決數(shù)獨(dú)、邏輯謎題入手來練習(xí)SAT建模是一個(gè)極佳的起點(diǎn)。你可以親身體驗(yàn)到如何將游戲規(guī)則用邏輯子句清晰地表達(dá)出來然后看著求解器瞬間給出答案或證明無解這種“定義問題機(jī)器解決”的思維方式非常強(qiáng)大。6. 上手實(shí)踐使用現(xiàn)代SAT求解器解決一個(gè)具體問題理論說得再多不如親手運(yùn)行一次。我們以解決一個(gè)經(jīng)典的“邏輯謎題”為例演示如何使用一款流行的SAT求解器——CaDiCaL它小巧、快速且易于使用來解決問題。6.1 問題描述誰養(yǎng)斑馬這是一個(gè)簡(jiǎn)化版的“愛因斯坦謎題”。有五個(gè)房子每個(gè)房子顏色、主人國籍、喝的飲料、抽的煙、養(yǎng)的寵物都不同。我們簡(jiǎn)化一下只關(guān)注寵物并給出部分線索房子按順序排成一排1, 2, 3, 4, 5。寵物有狗、貓、鳥、魚、斑馬。英國人住在紅房子里。瑞典人養(yǎng)狗。綠房子在白房子左邊。綠房子的主人喝咖啡。抽“萬寶路”的人養(yǎng)鳥。黃房子的主人抽“登喜路”。中間房子3號(hào)的主人喝牛奶。挪威人住第一個(gè)房子。抽“混合煙”的人住在養(yǎng)貓人的隔壁。養(yǎng)馬的人住在抽“登喜路”的人的隔壁。抽“藍(lán)領(lǐng)”牌香煙的人喝啤酒。德國人抽“王子”牌香煙。挪威人住在藍(lán)房子隔壁。抽“混合煙”的人有個(gè)鄰居只喝水。問題誰養(yǎng)斑馬6.2 將問題編碼為CNF我們需要為每個(gè)屬性定義布爾變量。例如Red1表示“1號(hào)房子是紅色”British1表示“1號(hào)房子的主人是英國人”以此類推。變量總數(shù)會(huì)很多5房子 * 5種屬性 * 5個(gè)取值但編碼是系統(tǒng)性的。編碼規(guī)則是關(guān)鍵需要將自然語言線索轉(zhuǎn)化為精確的邏輯子句。以“英國人住在紅房子里”為例它等價(jià)于對(duì)于每個(gè)房子i如果主人是英國人那么房子是紅色并且如果房子是紅色那么主人是英國人。這可以編碼為兩個(gè)子句(非British1 或 Red1)且(非Red1 或 British1)(非British2 或 Red2)且(非Red2 或 British2)... 對(duì)5個(gè)房子都如此。但更高效的編碼方式是使用“恰好為1”約束。例如“每個(gè)房子有且只有一種顏色”。對(duì)于房子1這意味著在Red1, Green1, Blue1, Yellow1, White1這五個(gè)變量中恰好有一個(gè)為真。這可以編碼為至少一個(gè)為真(Red1 或 Green1 或 Blue1 或 Yellow1 或 White1)至多一個(gè)為真對(duì)于每一對(duì)不同的顏色變量它們不能同時(shí)為真。例如(非Red1 或 非Green1),(非Red1 或 非Blue1), ... 總共需要 C(5,2)10 個(gè)子句?！熬G房子在白房子左邊”這樣的相對(duì)位置線索需要編碼為對(duì)于每個(gè)位置i如果房子i是綠色那么房子i1必須是白色。即(非Green1 或 White2),(非Green2 或 White3),(非Green3 或 White4)。注意綠房子不能在最后一個(gè)5號(hào)因?yàn)樗疫厸]有房子可以放白房子了這需要額外約束非Green5?！案舯凇标P(guān)系如線索11、12、15、16的編碼稍微復(fù)雜需要表示“如果房子i的人抽混合煙那么房子i-1或房子i1的人養(yǎng)貓”并且要處理邊界情況。由于手動(dòng)編碼如此多變量和子句非常繁瑣且易錯(cuò)在實(shí)際中我們通常使用更高級(jí)的建模語言如Python的python-sat庫、Z3的SMT接口等它們可以自動(dòng)將高級(jí)約束編譯成CNF。但為了理解本質(zhì)我們需要知道底層就是這些布爾變量和子句。6.3 使用CaDiCaL求解器假設(shè)我們已經(jīng)通過腳本或手動(dòng)方式生成了CNF文件zebra.cnf。CNF文件有標(biāo)準(zhǔn)的DIMACS格式。第一行以p cnf開頭聲明變量數(shù)和子句數(shù)。之后每一行是一個(gè)子句以0結(jié)尾。例如子句(非Red1 或 British1)如果Red1是變量1British1是變量6且“非”用負(fù)號(hào)表示那么這一行就是-1 6 0。在命令行中我們可以這樣調(diào)用CaDiCaL./cadical zebra.cnf solution.txt求解器會(huì)讀取CNF文件進(jìn)行計(jì)算并將結(jié)果輸出到solution.txt。6.4 解讀結(jié)果如果問題有解求解器會(huì)在文件中輸出“s SATISFIABLE”然后是一行以“v”開頭的賦值列表例如v 1 -2 3 -4 5 ... 0。正數(shù)表示變量為真負(fù)數(shù)表示變量為假。我們需要根據(jù)之前定義的變量映射表將這些賦值翻譯回現(xiàn)實(shí)意義比如變量1為真表示1號(hào)房子是紅色變量-2為假表示2號(hào)房子不是綠色……最終我們可以找出哪個(gè)國籍的人對(duì)應(yīng)的“養(yǎng)斑馬”變量為真從而回答“德國人養(yǎng)斑馬”這是經(jīng)典謎題的答案。如果問題無解比如線索給錯(cuò)了導(dǎo)致矛盾求解器會(huì)輸出“s UNSATISFIABLE”。通過這個(gè)完整的流程——從理解問題、定義變量、編碼約束、調(diào)用求解器到解讀結(jié)果——你就能真正掌握將現(xiàn)實(shí)世界難題轉(zhuǎn)化為SAT問題并求解的完整鏈路。這不僅僅是解決一個(gè)謎題更是學(xué)會(huì)了一種強(qiáng)大的問題求解范式。