代課老師：劉西洋
課件下載：https://github.com/mathematical-logic/mathematical-logic
參考："好心人"的往年總結(jié)
從萊布尼茲之夢(mèng)到馮-諾依曼計(jì)算機(jī)
命題邏輯的有序二叉決策圖（OBDD）
題型 1:根據(jù)真值表畫(huà)出 BDD，或根據(jù)公式畫(huà)出 BDD钾虐。
三步走(不斷利用香農(nóng)展開(kāi)的過(guò)程):
a) 固定一個(gè)變量腥椒，畫(huà)出此變量的節(jié)點(diǎn)及 0 1 分支烛卧。
b) 看是否有分支可以合并妄迁，如果可以則合并祥绞，否則再選取另一個(gè)變量轉(zhuǎn)到步驟 a)姓惑。
c) 直到分支節(jié)點(diǎn)處變?yōu)?0 或 1操灿，則結(jié)束。
題型 2:化簡(jiǎn)圖
這里就使用 PPT 里面給的那個(gè) Reduction 操作拐纱。這里把流程 走一遍铜异。
題型 3:給出兩個(gè) f，對(duì)其進(jìn)行<op>操作戳玫。
這題需要兩步熙掺， 第一步是 Apply 操作未斑，將兩個(gè)圖合并成一個(gè)圖咕宿，第二步是 Reduction 操作，就 是上面的化簡(jiǎn)蜡秽。
a) f1 的根結(jié)點(diǎn) v1府阀，f2 的跟結(jié)點(diǎn) v2，操作為<op>芽突，
整個(gè)過(guò)程就是在 f1 中取一個(gè)結(jié)點(diǎn)试浙，在 f2 中取一個(gè)結(jié)點(diǎn)，然后比較
b) 如果 v1 和 v2 均為終止結(jié)點(diǎn)寞蚌，那么目標(biāo)圖上畫(huà)一個(gè)終止結(jié)點(diǎn)田巴，值為 v1<op>v2
c) 如果 v1 和 v2 都不是終止結(jié)點(diǎn)，那就比較他們的索引值挟秤。
1. 如果 index(v1) = index(v2) = i壹哺，目標(biāo)圖畫(huà)一個(gè)非終止結(jié)點(diǎn)，對(duì)應(yīng) index = i;
然后在 low(v1)和 low(v2)遞歸地應(yīng)用該算法艘刚，深度優(yōu)先管宵，完成之后，在 high(v1)和 high(v2)遞歸地應(yīng)用該算法。
2. 如果 index(v1) = i箩朴，index(v2) > i岗喉，目標(biāo)圖畫(huà)一個(gè)非終止結(jié)點(diǎn)，對(duì)應(yīng) index = i;然后炸庞，在子樹(shù)中遞歸調(diào)用該算法钱床。
d) 如果 v1 和 v2 一個(gè)是非終止結(jié)點(diǎn)，另一個(gè)是終止結(jié)點(diǎn)埠居，終止結(jié)點(diǎn)的值是x
1. 如果 x<op>v2 的值由 x 決定诞丽，目標(biāo)圖上畫(huà)一個(gè)終止結(jié)點(diǎn)，值為 x拐格。
2. 如果 x<op>v2 的值不由 x 決定僧免，目標(biāo)圖上畫(huà)一個(gè)非終止結(jié)點(diǎn)，index = index(v2)
命題邏輯基于SAT Solver的DPLL可滿足性判定算法
DPLL Framework
DPLL（Davis-Putnam-Logemann-Loveland）算法捏浊，是一種完備的懂衩、以回溯為基礎(chǔ)的算法，用于解決在合取范式（CNF）中命題邏輯的布爾可滿足性問(wèn)題金踪；也就是解決CNF-SAT問(wèn)題浊洞。DPLL是一種高效的程序，并且經(jīng)過(guò)40多年還是最有效的SAT解法胡岔，以及很多一階邏輯的自動(dòng)定理證明的基礎(chǔ)法希。
Some conception:
1. 文字:一個(gè)變量或者它的補(bǔ)。
2. 子句:合取范式中兩個(gè)合取符號(hào)間的部分叫子句靶瘸。
3. 單元子句苫亦、單元文字:子句中其他變量的邏輯值都為 0，只剩一個(gè)文字未被賦值怨咪，
則該文字是單元文字屋剑，對(duì)應(yīng)的子句是單元子句。
4. 矛盾子句:子句中所有文字的邏輯值都為 0诗眨。
5. 可滿足問(wèn)題:一個(gè)合取范式唉匾，存在一組賦值使所有子句的邏輯值都為 1。
6. SAT 求解算法:1. 局部搜索算法(不完備算法);2. DPLL 算法(完備算法)
1匠楚、如果文字a（正文字或者負(fù)文字）在子句c（clause）中出現(xiàn)并且在其它子句中未出現(xiàn)!a巍膘，那么刪除該子句。
`刪除后所得公式與原公式具有相同的可滿足性芋簿！`
2峡懈、`任意選擇`一個(gè)文字b，并且對(duì)b賦值“真” (V = 益咬) 逮诲，刪除包含b的子句帜平，并且把所有其余子句中的!b刪除。
3梅鹦、對(duì)`只剩余一個(gè)文字的子句賦值`裆甩，使該文字為真（擴(kuò)大the partial valuation V＝ {b，!C} ）齐唆。
4嗤栓、如果the partial valuation有矛盾賦值（contradictory valuation），例如 V = {b, !C, C} 箍邮，
`退回原來(lái)的選擇`（backtrack to the privous choice）茉帅，重新對(duì)文字b賦值 V= {!b} .
5、如果已經(jīng)沒(méi)有辦法回退锭弊，則該公式不可滿足（unsatisfiable）
- Recursive description
DPLL(formula, assignment){
necessary = deduction(formula, assignment); # 找出必要的變量賦值
new_asgnmnt = union(necessary, assignment); # 得到新的一組賦值
if (is_satisfied(formula, new_asgnmnt)) # 判斷是否可滿足
return SATISFIABLE;
else if (is_conflicting(formula, new_asgnmnt)) # 判斷是否出現(xiàn)沖突
return CONFLICT;
var = choose_free_variable(formula, new_asgnmnt); # 挑選一個(gè)未賦值變量
asgn1 = union(new_asgnmnt, assign(var, 1)); # 給未賦值變量賦 1堪澎，得到新的賦值
if (DPLL(formula, asgn1)==SATISFIABLE) # 遞歸判斷
return SATISFIABLE;
else {
asgn2 = union (new_asgnmnt, assign(var, 0)); # 給未賦值變量賦 0
return DPLL(formula, asgn2); # 遞歸判斷
}
}
- Iterative Description
status = preprocess(); # 預(yù)處理
if (status!=UNKNOWN) return status;
while(true) {
decide_next_branch(); # 變量決策
while (true) {
status = deduce(); # 推理(BCP)
if (status == CONFLICT) {
blevel = analyze_conflict(); # 沖突分析
if (blevel == 0) # 如果沖突層次為頂層，則邏輯式直接不可滿足
return UNSATISFIABLE;
else backtrack(blevel); # 智能回溯
}
else if (status == SATISFIABLE)
return SATISFIABLE;
else break;
}
}
迭代比遞歸的優(yōu)勢(shì):
- 遞歸速度慢且容易發(fā)生溢出味滞，相對(duì)于迭代就有很多自身的劣勢(shì)樱蛤。
- 迭代具有非時(shí)間順序回溯(智能回溯)的優(yōu)勢(shì)。
預(yù)處理:所謂預(yù)處理就是根據(jù)邏輯蘊(yùn)含推理以及冗余子句刪除和添加等值子句等相關(guān)技術(shù)剑鞍。
變量決策:如何快速有效地決策出下一個(gè)將要賦值的變量昨凡。
MOM 方法:
思想:如果一個(gè)子句長(zhǎng)度很小，那它就很不容易被滿足蚁署，所以我們要優(yōu)先考慮它們便脊，給予它們更高的權(quán)重。
方法要點(diǎn):子句長(zhǎng)度短光戈，出現(xiàn)頻率高哪痰。-
VSIDS 方法:
- 為每一個(gè)變量設(shè)定一個(gè) score，這個(gè) score 的初始值就是該變量在所有子句集中出現(xiàn)的次數(shù)田度。
- 每當(dāng)一個(gè)包含該文字的沖突子句被添加進(jìn)子句庫(kù)妒御，該文字的 score 就會(huì)加 1解愤。
- 哪個(gè)變量的 socre 值最大镇饺，就從這個(gè)變量開(kāi)始賦值。
- 為了防止一些變量長(zhǎng)時(shí)間得不到賦值送讲，經(jīng)過(guò)一定時(shí)間的決策后奸笤，每一個(gè)變量的 score 值都會(huì)被 decay，具體方式是把 score 值除以一個(gè)常
數(shù)(通常為 2-4 左右)哼鬓〖嘤遥——“周期衰減”
優(yōu)點(diǎn):統(tǒng)計(jì)數(shù)據(jù)與變量賦值狀態(tài)無(wú)關(guān)，因此系統(tǒng)資源開(kāi)銷非常低异希〗『校可以 顯著提高求解器性能。
BCP：通過(guò)推理來(lái)減少一些不必要的搜索，加快效率扣癣。主要依賴單元子句規(guī)則
Counters 方法:每個(gè)子句有兩個(gè)計(jì)數(shù)器惰帽，一個(gè)記錄邏輯值為 true 的文 字?jǐn)?shù)，另一個(gè)記錄邏輯值為 false 的文字?jǐn)?shù)父虑。如果一個(gè) CNF 實(shí)例有 m 個(gè)子句该酗，n 個(gè)變量，每個(gè)子句平均有 L 個(gè)文字士嚎，則有一個(gè)變量被賦值 的時(shí)候呜魄，會(huì)有平均 mL/n 個(gè)計(jì)數(shù)器需要更新，在回溯的時(shí)候莱衩，每取消 一個(gè)變量賦值爵嗅，也會(huì)平均有 mL/n 個(gè)計(jì)數(shù)器的更新。如果一個(gè)子句的false 計(jì)數(shù)器的值等于該子句的文字?jǐn)?shù)笨蚁，則說(shuō)明出現(xiàn)了沖突;如果一 個(gè)子句的 false 計(jì)數(shù)器的值等于該子句的文字?jǐn)?shù)減 1操骡，則該子句是單元子句。
head/tail 方法:每個(gè)子句存在一個(gè)數(shù)組中赚窃，并且有兩個(gè)指針册招，一個(gè)頭指針，一個(gè)尾指針勒极，每個(gè)變量 v 有四個(gè)附加鏈表是掰，分別裝有句頭是 v 的子句，句頭是非 v 的子句辱匿，句尾是 v 的子句键痛，句尾是非 v 的子句。 所以匾七，如果有 m 個(gè)子句絮短，四個(gè)鏈表中就存放著 2m 個(gè)子句。移動(dòng)指針有四種情況:
1. 第一個(gè)遇到的文字為真昨忆，說(shuō)明子句已經(jīng)滿足丁频，直接忽略該子句。
2. 第一個(gè)遇到的文字未賦值且不是句尾邑贴，那就將該子句刪除席里，放到對(duì)應(yīng)文字的鏈表中。
3. 頭尾指針之間只有一個(gè)變量未賦值且其他文字都為假拢驾，則出現(xiàn)單元子句奖磁。
4. 頭尾指針之間所有文字都為假，產(chǎn)生沖突繁疤，回溯咖为。
當(dāng)一個(gè)變量被賦值的時(shí)候秕狰，平均有 m/n 個(gè)子句需要更新(m 為子句 數(shù)，n 為變量數(shù))躁染。
- 2-literal watching 方法(應(yīng)用于 zChaff 求解器):與 head/tail 方法相 似封恰，為每個(gè)子句關(guān)聯(lián)兩個(gè)指針，但這兩個(gè)指針沒(méi)有頭和尾之分褐啡，位置 任意诺舔。它與 head/tail 方法的關(guān)鍵區(qū)別是回溯時(shí)指針的位置無(wú)需移動(dòng)， 取消一個(gè)變量的賦值時(shí)間的開(kāi)銷是常量备畦，但壞處是只有遍歷完所有 文字才能找到單元文字低飒。兩個(gè)指針隨時(shí)監(jiān)視子句中任意兩個(gè)未被賦 值為 0 的文字。每個(gè)變量 v 有兩個(gè)附加鏈表懂盐，對(duì)應(yīng)變量的正負(fù)形態(tài)褥赊， 存放的是對(duì)應(yīng)的子句。設(shè)初始時(shí)變量 v 賦值為 1莉恼，則搜索將在一個(gè)含 有文字-v 的子句中進(jìn)行(因?yàn)?v 已滿足)拌喉，并且此時(shí)一個(gè)監(jiān)視指針指 向文字-v，繼續(xù)搜索俐银，該過(guò)程中有四種情況:
1. 如果存在文字 L 不是該子句的另外一個(gè)被監(jiān)視文字尿背，則刪除指向文字-v 的指針，
并添加指向文字 L 的指針捶惜，相當(dāng)于指針移動(dòng)田藐。
2. 如果唯一符合條件的文字 L 是另外一個(gè)被監(jiān)視文字，且它沒(méi)有被賦值吱七，
則該被監(jiān)視文字是單元文字汽久，該子句是單元子句。
3. 如果唯一符合條件的文字 L 是另外一個(gè)被監(jiān)視文字踊餐，且它已經(jīng)被賦值為 1景醇，
說(shuō)明該子句已經(jīng)滿足，不需要進(jìn)行任何處理吝岭。
4. 如果所有文字都已經(jīng)被賦值為 0三痰，那么出現(xiàn)沖突，回溯苍碟。
沖突分析
- Conflict Analysis and Learning 尋找沖突的原因并學(xué)習(xí)
analyze_conflict(){
cl = find_conflicting_clause();
while (!stop_criterion_met(cl)) {
lit = choose_literal(cl);
var = variable_of_literal( lit );
ante = antecedent( var );
cl = resolve(cl, ante, var);
}
add_clause_to_database(cl);
back_dl = clause_asserting_level(cl);
return back_dl;
}
智能回溯
- 時(shí)序回溯:直接返回上一層酒觅，將變量取值翻轉(zhuǎn)。
- 非時(shí)序回溯:結(jié)合沖突學(xué)習(xí)微峰，智能分析，跳回多個(gè)決策層抒钱，并且會(huì)將導(dǎo)
致沖突的子句加入到子句集中蜓肆。
子句數(shù)據(jù)結(jié)構(gòu)
- 數(shù)組方式:數(shù)組采用連續(xù)空間存儲(chǔ)颜凯，內(nèi)存利用率和存儲(chǔ)效率更高，局部訪問(wèn)能力更強(qiáng)仗扬。連續(xù)存儲(chǔ)能提高 cache 命中率症概，從而增加計(jì)算速度。但不靈活早芭。
- 鏈表方式:便于對(duì)子句進(jìn)行增加和刪除操作彼城，存儲(chǔ)效率低。因?yàn)槿鄙倬植吭L問(wèn)能力退个，往往會(huì)造成緩存丟失募壕。
注:head/tail 和 2-literal watching 都被稱為“膨脹數(shù)據(jù)結(jié)構(gòu)”，它們都采用數(shù)組存儲(chǔ)子句语盈，最具競(jìng)爭(zhēng)力舱馅。
例題:設(shè)計(jì)一個(gè)基于數(shù)組的數(shù)據(jù)結(jié)構(gòu)存儲(chǔ)子句
方案 1:head/tail
用數(shù)組存儲(chǔ)子句的文字，對(duì)于每個(gè)數(shù)組設(shè)置兩個(gè)指針刀荒，分別為頭指針 與尾指針代嗤，然后對(duì)于每個(gè)變量 v 設(shè)置 4 個(gè)鏈表，分別裝有句頭是 v 的子句缠借， 句頭是非 v 的子句干毅，句尾是 v 的子句，句尾是非 v 的子句泼返，這樣存儲(chǔ)的子 句溶锭，無(wú)論子句順序及其中變量順序的改變都不會(huì)影響所有變量的四個(gè)鏈表中 的子句數(shù)量。取所有變量 v 是句頭的子句與非 v 是句頭的子句或者 v 是句尾 的子句與非 v 是句尾的子句合取可以得到公式符隙。
方案 2:2-literal watching
為每個(gè)子句關(guān)聯(lián)兩個(gè)指針趴捅，這兩個(gè)指針位置任意，隨時(shí)監(jiān)視子句中任
意兩個(gè)未被賦值為 0 的文字霹疫。每個(gè)變量 v 有兩個(gè)附加鏈表拱绑，對(duì)應(yīng)變量的正負(fù) 形態(tài)，存放的是含有對(duì)應(yīng)文字的子句丽蝎。該種結(jié)構(gòu)的好處是回溯時(shí)指針的位置 無(wú)需移動(dòng)猎拨，取消一個(gè)變量的賦值時(shí)間的開(kāi)銷是常量。此外屠阻，重新分配最近分 配和未分配的變量將比第一次分配的變量更快红省，并且可以減少內(nèi)存訪問(wèn)總數(shù)， 提高緩存命中率国觉。
FDS
一個(gè)程序 D 由五部分組成?? = < ??,??,??,??,??,?? >
??:有限狀態(tài)集合吧恃。包括程序中的變量和語(yǔ)句.
??:可觀測(cè)狀態(tài)集合。定義??屬于??麻诀。一般沒(méi)有說(shuō)明的話痕寓，默認(rèn)所有狀態(tài)都可觀測(cè)傲醉，因此??等于??。這個(gè)不重要呻率，應(yīng)該不考.
??:初始條件.
??:轉(zhuǎn)換關(guān)系硬毕。考察的重點(diǎn).
??:justice 集合礼仗，弱公平的.
??:compassion 集合吐咳，強(qiáng)公平的.
Alloy
