布爾代數運算律
布爾運算等式變換
BDD(二元決策樹)
BDD描述了一個過程，這個過程按照給定的值（0/1）進行向下搜索，直到終點。
從真值表中派生（Derive）二元決策樹：
化簡：將冗余的部分去掉
對於左邊紅框內，因為無論\(C\)取何值，最終的結果總是為0，因此\(C\)的存在對於該分支的結果並沒有影響，因此可以將其刪除。對於右邊紅框由\(B\)延伸到\(C\)處時，無論\(B\)取何值，總是延伸到相同的\(C\)，因此在這里\(B\)的取值也對該分支沒有影響，因此可以直接將\(B\)節點刪除，從而得到了右圖。
Shannon expansion formula(香農展開)
算法步驟：
- 固定一個變量，畫出此變量的節點以及01分支
- 看是否有分支可以合並，如果可以則合並，否則再選取另一個變量轉到步驟1
- 直到分支節點處變為0或1，則結束。
即：每次提取一個變量，將原來的表達式擴展為該變量取不同值的形式。
示例：
如圖a所示，將\(A\)取值為0時，原表達式\(f\)進化為為\(f_0\)，將\(A\)取值為1時，\(f\)進化為\(f_1\)。
BDD在計算機中的存儲時，每個節點對應一個三元組：(變量名稱，指針1，指針2)
其中，變量名稱指定變量，指針1，指針2分別指定，當前變量取值分別為0或1時，應該指向的節點。
如(a)表示一個節點分支，則其在計算機中的存儲可以表示為(V, g, h)。(b)表示了一組存儲的三元組。(c)表示了(b)代表的BDD。
計算BDD的輸出時，只需要沿着標識路徑一直往下走即可，所到達的終止節點的值即為輸出結果。
注：
- 一個節點的輸出路徑有且僅有一條是active path
- 從一個節點到0或1終點，有且僅有一條由active path組成的路徑
計算“和的積”與“積的和”的個數
“和的積”的個數：主合取范式中，合取式的個數，即：使輸出結果為0的路徑數目。
“積的和”的個數：主析取范式中，析取式的個數，即：使輸出結果為1的路徑數目。
用分支的權值計算：
步驟：
- 最上層結點的兩個分支權均賦值為1。
- 其余的結點的兩個分支權均賦值為它所有入度權值的和。
其中， 和的積(0): 8+7+7=22 積的和(1): (8+8+7=23)
圖的簡化(reduce) (ODBB)
簡化后的函數圖包含以下性質：
- 不包含左右子節點相同的節點
- 不包含這樣的節點：分別以左右子節點為根節點的子圖同形
注：在簡化的圖中，以每一節點為根的子圖也是簡化的。任意的布爾函數有唯一的簡化圖可以將其表示，使得圖的節點數目最少
化簡思想為：將原圖按層排列，從終止節點(底層)依次向上進行標記，最后相同標記的只取一個節點就完成了圖的簡化。
樣例：
第一步：將節點放到各層列表中，此處需要注意的是，要把終止節點全部都放在最后一層
第二步：從終止節點到根節點對每個list進行操作
對於每個節點，oldkey的初始化均為(-1,-1)，終止節點的oldkey最后應該只有一個0或1值，同時終止節點最終也應該至多只有兩個id(1,2)和oldkey(0,1)
對於非終止節點，其oldkey最后為兩個值，前一個值表示其取0時應該指向的節點id，另一個值表示其取1時應該指向的節點id。low,high分別表示其取0和1時指向的節點。
當某個節點的low值和high值相等時，說明該節點的取值對於該分支的最終結果並沒有影響，因此可以直接刪除該節點。
OBDD的Apply操作是通過深度優先搜索的方法，對一些已知的布爾函數 OBDD 表示進行二元布爾運算得到另外一些布爾函數 OBDD 表示的操作。整個過程從上至下進行，我們需要做的預備工作是給每個節點編號（1，2，3.... 每個都不相同），然后從頂層開始，用兩個 OBDD 樹的頂層的節點合成一個新的節點，合成的規則就三種：
- 兩個節點都為葉節點，可以直接根據布爾運算得出結果，合成的節點也是葉節點。
- 如果有一個節點為非葉子節點，看這兩個節點的 index 值是否一樣，如果是一樣的，比如兩個節點都表示 x1，那么新節 點的 index 就是 x1，新節點的左孩子通過兩個老節點的左孩子生成，新節點的右節點通過兩個老節點的右孩子生成。
- 如果兩個節點的 index 值不同，比如 index(u)\(<\)index(v)，新節點的 index 為較小的 index(u)，新節點的左孩子由 u 的左孩子與 v 生成，新節點的右孩子由 u 的右孩子與 v 生成，當 index(u)\(>\)index(v)反過來做即可。
舉例：\(f=(x_1+x_2)*x_3+x_4,g=x_1*x_3^{'}+x_4\)，求\(f+g\)的OBDD
關於 OBDD 的 ITE 的實現過程
ITE操作是一個三元布爾操作符，對於具有相同變量序的三個布爾函數f、g和h，ITE操作可用來實現：if f then g else h。對於相同變量序：\(x_1<x_2<...<x_n\)下的布爾函數\(f,g\)和\(h\),\(ITE(f,g,h)=f\cdot g+f^{'}\cdot h\)
在算法中，常用小寫 ite 來表示 ITE。下表給出了一些二元布爾運算的 ITE 操作實現:
程序轉化為邏輯表達式
FDS(Fair Discrete System)
一個Fair Discrete System(FDS) \(D = \lt V, O, \Theta, p, J, C \gt\)包括：
- \(V\)：一組有限的類型化狀態變量，一個V-state s表示V的一個解釋
\( \sum_V \)：表示所有的V-states集合 - \(O \subseteq V\): 可觀察變量的集合
- $\Theta $：一個初始條件。一個描述初始狀態的能夠滿足的斷言
- \(p\)：一個過渡關系。一個斷言\(p(V, V^{'})\)，引用狀態變量的當前版本和即將變換成的版本。例如，\(x^{'}=x+1\)對應於賦值\(x:=x+1\)
- \(J={J_1,...,J_k}\)：一個公平的(justice)需求集合。確保對於每個\(j_i,i=1,...,k\)的計算包含無限多個\(j_i\)-states。
- \(C=\lbrace <p_1,q_1>,...,<p_n,q_n>\rbrace\)：一個包含compassion需求的集合。無限多個\(p_i\)-states意味着無限多個\(q_i\)-states。
例子：
- 首先表示\(V\)，狀態變量
a) 首先第一行就是程序最上面的初始化，左邊兩個變量一寫，右邊寫個 natural。
b) 接下來定義$\pi \(，程序有幾個部分(用||連接)就定義幾個\)\pi \(，每個\)\pi \(對應的元素就是每一行語句\)𝑙_0$ ~ \(𝑙_𝑘\)
- 表示\(\Theta\)
\(\Theta\)表示初始條件，而初始時，每個\(\pi\)都處於第一行語句\(l_0\)，再加上變量的初始化，把它們合取即可。
- 表示𝜌：表示𝜌之前得先說明幾個定義：
- \(\pi^{'}\)可能在此表示下一個狀態
- \(pres(V)\)。對於\(V\)里面的每個元素都可以這樣表示：\(e=e^{'}\)，然后把它們用合取符號連接起來。上面例子的\(press(V)\)就應該表示為：
- \(at\_l_j\)是一個縮寫，表示\(\pi_i = l_j\)，\(at^{'}\_l_j\)表示\(\pi_i^{'}=l_j\)
- \(p_I=press(V)\)，\(p_{l_0}\)表示語句\(l_0\)轉換成邏輯公式之后的一個符號。需要掌握\(p_{l_k}\)
- $p:p_I \vee p_{l_0} \vee p_{l_1} \vee p_{m_0} $
語句的表示
a) 賦值語句樣例：\(y := e\)
進行該語句時，需要進行以下狀態檢查以確定該賦值語句是否能夠成立。\(at\_l_j \wedge at^{'}\_l_k \wedge y^{'} = e\wedge pres(V-\lbrace \pi_i,y\rbrace)\)。
進行以上例題中的\(m_0\)賦值語句時，就應該表示成：\(p_{m_0}:\pi_2=m_0 \wedge \pi_2^{'}=m_1 \wedge \pi_1^{'} = \pi_1 \wedge x^{'} = 1 \wedge y^{'} = y\)
b) if語句：if b then \(l_1: S_1\) else \(l_2:S_2\)
如果這里沒有else語句，那么\(l_2\)就是跳出if下一步要執行的語句
c) while語句：while b do [\(l_1:S_1\)]
上面例子\(l_0\)就可以表示為
- 表示\(J\)：一般把\(!at\_l_j\)這個符號加入\(J\)集合中
上面例子的\(J\)集合可表示為
- 表示\(C\)。一般該集合為\(\empty\)
子句沖突規則
SAT
SAT: 給定一個命題公式，確定是否存在變量賦值以使該公式計算為真，這稱為布爾可滿足性問題。結果是，找到一個滿足條件的解決方案或者證明不存在解決方案。
SAT問題的基本形式指給定一個命題變量集合\(X\)和一個\(X\)上的合取范式\(\varphi (X)\)，判斷是否存在一個真值賦值\(t(X)\)，使得\(\varphi (X)\)為真。如果能找到，則稱\(\varphi (x)\)是可滿足的（satisfiable），否則稱\(\varphi (x)\)是不可滿足的（unsatisfiable）。SAT問題的模型發現形式指當\(\varphi (x)\)可滿足時，給出使公式\(\varphi (x)\)可滿足的一組賦值。
實際生產中的 NP 難題可以轉化為 SAT 問題進行求解，因此，首先要進行規約和編碼，目前 SAT 問題編碼多采用 CNF 形式。DIMACS 作為標准格式廣泛用於 CNF 布爾公式，也被歷屆 SAT 國際競賽采用。 DIMACS 文件用字符 c 引導的注釋文字行開始。緊接注釋之后的一行 p cnf 表示該實例是 CNF 形式的公式，nbvar 指公式包含的變量數目，nbclauses 指公式包含的子句數目，要求1至 nbvar 之間的每個變量至少在某個子句中出現一次。然后下面各行是子句序列，每個子句由一系列互不相同的介於 -nbvar 和 nbvar 的非空數字組成，並以 0 結束。正的數字表示相應序號變量的正文字形式，負的數字表示對應序號變量的負文字形式。
最近幾年的SAT國際競賽結果證明，預處理技術對SAT求解器性能至關重要。早期的預處理技術使用原始 DPLL （DavisPutnamLogemannLoveland，簡稱DPLL）提出的單元傳播和純文字規則，后來發展了一些更復雜的技術如超二元解析、單元子句和探針等。
命題邏輯基於SAT Solver的DPLL可滿足性判定算法
合取范式樣例：\((p∨q∨r)∧(p∨┐q∨r)∧(┐p∨q∨r)\)
析取范式樣例：\((p∧q∧r)∨(p∧q∧┐r)∨(p∧┐q∧r)∨(┐p∧q∧r)∨(┐p∧┐q∧r)\)
DPLL（Davis-Putnam-Logemann-Loveland）算法，是一種完備的、以回溯為基礎的算法，用於解決在合取范式（CNF）中命題邏輯的布爾可滿足性問題；也就是解決CNF-SAT問題。
DPLL 的核心思想就是依次對 CNF 實例的每個變量進行賦值，其搜索空間可以用一個二叉樹來表示，樹中的每個節點對應一個變量，取值只能為 0 或 1，左右子樹分別表示變量取 0 或 1 的情況，從二叉樹中根節點到葉子節點的一條路徑就表示 CNF 實例中的一組變量賦值序列，DPLL 算法就是對這棵二叉樹從根節點開始進行 DFS（深度優先搜索） 遍歷所有的通路，以找到使問題可滿足的解。
預處理：將公式轉換為對應的合取范式（CNF）
DPLL 框架
- Iterative Description（迭代描述）
status = preprocess(); //預操作
if (status!=UNKNOWN) return status;
while(1) {
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;
}
}
- 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))
return CONFLICT;
var = choose_free_variable(formula, new_asgnmnt);
asgn1 = union(new_asgnmnt, assign(var, 1));
if (DPLL(formula, asgn1)==SATISFIABLE)
return SATISFIABLE;
else {
asgn2 = union (new_asgnmnt, assign(var, 0));
return DPLL(formula, asgn2);
}
}
基於迭代的實現相對於基於遞歸的實現有以下優勢：
- 遞歸速度慢且容易發生溢出，相對於迭代就有很多自身的劣勢。
- 迭代具有非時間順序回溯（智能回溯）的優勢。
- 遞歸需要更多的內存存儲空間。
以下討論基於迭代框架。
算法框圖：
算法流程：
首先執行的是 preprocess()這個預處理操作，其實就是對 CNF 實例進行各種化簡減輕后續的求解工作量。如果預處理不能直接 得出結果的話，就進行后面的 decide_next_branch()操作，這就是變量決策操作，它會分析從 哪個變量開始賦值是最合適的。對變量賦值以后，會執行一個deduce() 操作，可以管它叫推理操作，目的是識別該賦值所導致的必要賦值。 當然不正確的賦值可能會產生錯誤，這就會產生沖突，我們需要 analyze_conflict()分析這個沖 突得到沖突發生的根源位置，然后通過 backtrack()回溯到這個位置，為這個變量賦另外一個值， 繼續往下搜索，如此循環，直到找到滿足 SAT 的一組真值指派。如果回溯到了最頂層還沒有解 決問題的話，那就表示這個 CNF 實例是不可滿足的。
變量決策(decide_next_branch())
基於這樣的一個事實：先對哪個變量進行賦值，會直接影響二叉搜索樹的規模大 小，也就會影響求解時間，所以如何快速有效地決策出下一個將要賦值的變量，這很重要。以下將介紹四種變量決策方式：
- MOM(JW)方法
- Literal Count Heuristics 方法
- VSIDS 方法
- 一個改進的方法--（A Fast and Robust SAT Solver）
- MOM 法或者 JW 法
思想： 在一個子句中， 只要一個文字得到滿足，那么這個子句就得到滿足了。
所以，如果一個子句的長度越長（含有字母數越多），那么可以使得該子句滿足的文字數目也就越多，這個子句也就越容易滿足，所以它就不是所謂的“矛盾的主要方面”，我們不需要過於關注這個子句；然而，如果一個子句長度很小，那它就很不容易被滿足，所以我們要優先考慮它們，給予它們更高的權重， 這樣做的目的就是讓那些不容易被滿足的子句優先得到滿足。
具體的方法是求解出和變量 \(l\) 相對應的 \(J\) 值，哪個變量 \(J\) 值大就選哪個先賦值，變量對應的 \(J\) 值的計算公式如下：
其中 \(l\) 表示變量，\(Ci\) 表示包含變量 \(l\) 的子句，共有 \(m\) 個子句， \(n_i\) 表示這個子句的長度。它體現出了 MOM 算法的兩個關鍵點：“最短的子句”和“出現頻率最高的變量”，”最短子句”體現在長度越短（\(n\) 越小）， \(2^{-n_i}\) 的值就越大，它能給 \(J\) 值的貢獻就越多；”出現頻率最高的變量”體現在 \(l\) 出現次數越多的話，相加的項數就越多，\(J\) 值就更容易變的很大。
- Literal Count Heuristics 方法
它主要是統計已經給某些字母賦值但仍然沒有得到滿足 的子句的數量，這個數量依賴於變量賦值，所以每次換變量的時候，所有自由變量都需要重 新統計這個數量，效率較低。 - VSIDS，Variable State Independent Decaying Sum(獨立變量狀態 衰減和策略)
具體操作步驟如下：
- 為每一個變量設定一個 score，這個 score 的初始值就是該變量在所有子句集中出現的次數
- 每當一個包含該字母的沖突子句被添加進數據庫，該字母的 score 就會加 1
- 哪個變量的 socre 值最大，就從這個變量開始賦值
* 另外，為了防止一些變量長時間得不到賦值，經過一定時間的決策后，每一個變量的 score 值都會被 decay，具體方式是把 score 值除以一個常數(通常為 2-4 左右)
推理(deduce())
當一個變量被賦值后，可以通過推理來減少一些不必要的搜索，加快效率。推理過程主要依賴於 Unit clause rule（單元子句規則），所謂單元子句就是：在這個子句中，除了一個文字未賦值 外，其他所有的文字都被賦值並體現為假，這樣的子句就是 Unit clause（單元子句），剩下的 這個文字就是 unit literal（單元文字）。很容知道，在單元子句中，這最后一個文字必須體現 為真，整個子句才能被滿足，把所有的單元文字都賦值並體現為真的過程就是 BCP（布爾約束 傳播）。
BCP 的目標就是識別出單元子句並對單元文字賦值，能夠減少搜索空間或提前逼出沖突。
以下將介紹三種BCP實現方法：
- counters 方法
- head/tail list 方法
- 2-literal watching 方法
counters 方法
具體做法是是為每個變量設置兩個 lists，分別用來保存所有包含這個變量的正負字母的子句，並且每個子句都設置兩個計數器，分別統計體現為真的字母數和體現為假的字母數。如果體現為假的字母等於總字母數，那就產生了沖突；如果體現為假的字母數比總字母數少 1，那就出現了單元子句，就需要對單元文字進行自動賦值。
舉例
注：用\(!\)取代了邏輯非，因為不知道邏輯非怎么弄出來
初始的時候，1-8 號子句各有兩個計數器（分別記錄賦值為 0 和 1 的文字數量），一開始所有計數器的值都是 0。變量 \(m\) 有鏈表分別用來保存所有包含 \(m\) 和 \(!m\) 的子句，包含 \(m\) 的 鏈表中有子句 2，3，4，5，而包含 \(!m\) 的鏈表中有子句 1，7，8，其余變量也均有這樣的兩個鏈表。當給 \(m\) 賦 0 時，包含 \(m\) 的鏈表中的子句 2，3，4，5 的 0 計數器就會更新，數量加 1， 包含 \(!m\) 的鏈表中的子句 1，7，8 的 1 計數器也會更新，數量加 1；如果再給 \(p\) 賦 0 的話，包 含 \(p\) 的鏈表中的子句 1，2，3，8 的 0 計數器就也會更新，數量加 1，此時 2，3 兩個子句的 0 計數器數量變為 2，比總文字數 3 少 1，均成為了單元子句，2 可以推出 \(q\) 必須賦 1，而 3 可以 推出 \(q\) 必須賦 0，產生沖突，BCP 完成任務。
head/tail list 方法
它為每個子句設置兩個引用指針，分別是頭指針和尾指針，初始時，頭指針指向子句第一個文字，尾指針指向最后一個文字，每個子句的文字存放在一個數組中。對於一個變量 \(v\)，設置有四個鏈表，分別裝有句頭是 \(v\) 的子句，句頭是非 \(v\) 子句，句尾是 \(v\) 的子句， 句尾是非 \(v\) 的子句，分別標記為 clause_of_pos_head(v)，clause_of_pos_tail(v)， clause_of_neg_head(v)，clause_of_neg_tail(v)。假設有 \(m\) 個子句的話，所有變量的四個鏈表中就共存放着 \(2m\) 個子句，無論后面這些子句怎么調換位置，子句總數是不變的。
因為是合取式，因此一共有2m個子句
假設某變量 \(v\) 被賦值為 1，那么所有句頭和句尾為 \(v\) 的子句就都可以忽略了，因為他們已經被滿足了。而對於句頭或句尾是非 \(v\) 的子句，就需要移動頭尾指針尋找下一個未被賦值的字母，頭指針往后移，尾指針往前移，移動時可能會發生以下四種情況：
- 第一個遇到的文字 \(l\) 已經體現為真了，那么子句就已經滿足了，什么都不用做，忽略這個子句就行了。
- 第一個遇到的文字 \(l\) 是未賦值的，且不是句尾，那么就把這個子句 \(c\) 從 \(v\) 的鏈表中移除，放入到 \(l\) 的對應的鏈表中。
- 如果頭尾之間只剩一個變量未賦值，其他文字都體現為假了，就出現了單元子句，直接推斷出單元文字的取值。
- 如果頭尾之間所有文字都體現為假，那產生沖突，需要回溯。當一個變量被賦值的時候，平均有 m/n 個子句需要更新（m 為子句數，n 為變量數）。
舉例
初始時，我們可以將各個子句填入變量的鏈表中，如下表所示：
此時，頭尾指針分別指向每個子句的頭部和尾部。當我們給 \(m\) 賦值為 0 的時候，\(m\) 的 clause_of_neg_head(m)鏈表中的子句 1，7，8 就可以忽略不看了，因為已經被滿足，把它們標注為綠色，而 clause_of_pos_head(m) 中的子句 2，3，4，5 還沒有被滿足，這些子句頭指針需要后移一位，轉移后這些子句的頭指針指向的文字就不是 \(m\) 了，所以需要將表格中 2，3，4，5 的位置換一下，更換位置的子句用紅色標注，這次賦值后結果如下：
以此類推，當我們再給 \(p\) 賦 0 的時候，4，5 就可以不用考慮了，2，3 的頭指針需再后移一位，2，3 在表格中的位置也需要更換，如下表所示：
此時已經滿足條件（3）了，形成了兩個單元子句，2 可以推出 \(q\) 必須賦 1，而 3 可以推 出 \(q\) 必須賦 0，產生沖突，BCP 完成任務。
2-literal watching
這個方法與 H/T 類似，也要為每個子句關聯兩個指針，與 H/T 不同之處是，這兩個指針沒有先后次序，也就沒有所謂的頭和尾的概念，這樣設置會帶來很多好 處，比如初始時這兩個指針的位置可以是任意的（H/T 必須放在頭和尾的位置），移動時也可 以向前后兩個方向移動（H/T 中頭指針只能向后移，尾指針只能向前移），回溯時無需改動指針的位置（W/T 回溯時需要把指針變回原來的位置）。但這種設置也有弊端，即只有遍歷完所 有子句的文字后，才能識別出單元子句。相對應的，每個變量 v 也設置了兩個 list 來分別存放以 watching 指針分為 v 以及非 v 的子句。接下來的操作都與 W/T 類似，當某個變量 v 賦值為 1 的話，watching 指針為 v 的子句可以忽略，watching 指針為非 v 的子句開始移動指針。
沖突分析與學習(analyze_conflict())
目的: 是找到沖突產生的原因，這就是分析的過程；並告訴 SAT 處 理器這些搜索空間是會產生沖突的，以后不要再踩這些坑了，這就是學習的過程。
早期解決沖突的方法就是回到上一層，將變量取值翻轉，繼續往下進行搜索，這也叫時序回 溯。但是這樣做的結果很可能是沖突依舊存在，因為上一層的賦值也許並不是沖突產生的根本原 因，從而白白浪費一次計算的時間，效率非常低。目前主流的 SAT 處理器都采用基於沖突分析和學習的非時序回溯算法，它可以智能地分析 出沖突產生的根本原因，並回跳多個決策層，並把會導致沖突的子句加入到子句集中。
以下為一次沖突分析和學習的例子：
從圖中我們可以看出，導致沖突產生的根本原因是第 1 層中將 \(x_9\) 賦為 0，在第 3 層中 將 \(x_{10}\) 賦為 0，在第 3 層中將 \(x_{11}\) 賦為 0，在第 6 層中將 \(x_1\) 賦為 1（\(x_1\)=1@6 表示在第 6 層將 x1 賦值為 1）。由此我們可以直接回溯到第 3 層進行重新賦值，而不是僅僅回溯到上一層，並且我們知道$(x_9 = 0) \cap (x_{10} = 0) \cap (x_{11} = 0) \cap (x_1 = 1) \(會導致沖突，我們就可以添 加子句\)w_{10} = (x_9 \cup x_{10} \cup x_{11} \cup !x_1)$ 添加進子句庫中，在接下里的搜索過程中就能預防相同的變量賦值再次出現。
相關代碼：
analyze_conflict(){
cl = find_conflicting_clause(); // 找到沖突子句 cl
while (!stop_criterion_met(cl)) {
lit = choose_literal(cl); // 選擇一個文字
var = variable_of_literal( lit ); //這個文字所對應的變量命名為var
ante = antecedent( var ); // ante 為一個單元子句
cl = resolve(cl, ante, var);
// resolve()返回一個子句，除了 var 所對應的文字，這子句需要包含 cl 和 ante 中的
// 所有文字，其中 cl 是一個沖突子句，ante 是一個單元子句，所以返回的 cl 也是一個沖突子句
}
add_clause_to_database(cl);
back_dl = clause_asserting_level(cl);
return back_dl;
}
數據的存儲方式
數據存儲方式主要包括以下三種：
- 早期的鏈表和指針數組的存儲方式
- 數組方式
- trie 存儲方式
各個方法優缺點：
數組方式：數組采用連續空間存儲，內存利用率和存儲效率更高，局部訪問能力更強。連續存儲能提高，cache 命中率，從而增加計算速度。但不靈活。
鏈表方式：便於對子句進行增加和刪除操作，存儲效率低。因為缺少局部訪問能力，往往會造成緩存丟失。
head/tail 和 2-literal watching 都被稱為“膨脹數據結構”，它們都采用數組存儲子句，最具競爭力。
以下主要介紹Tire數據存儲方式。
Tire 是以三叉樹的方式存儲，它的每個內部節點都是都是一個變量的索引，從根節點到葉節點路徑上的所有變量組成一個子句。每個節點的三條孩子邊分別被標記為 Pos(positive)、Neg(negative)和 DC(dont care)，例如節點 v 的 Pos 邊表示文字 v,Neg 邊表示文字 !v ，DC 邊表示沒有這個變量的文字。Tire 的葉節點是 T 或者 F，T 表示 CNF 實例中有這個子句，F 表示沒有這個子句。下面是文中給出的一個例子：
從圖中我們可以清楚地看出這個 CNF 實例中有哪些子句，以 \(V_1\) 的左孩子的三條路徑舉例，第一條路徑從根節點到葉節點為\((V_1，+)，(V_2，+)，T，\)表示\((V_1+V_2)\)這個子句是存在的；第二條路徑從根節點到葉節點為\((V_1，+)，(V_2，-)，F，\)表示\((V_1+ !v_2)\) 這個子句是不存在的；第三條路徑從根節點到葉節點為\((V_1，+)，(V_2，DC)，T，\)表 示\((V1)\)這個子句是不存在的，以此類推，可以得出所有的子句，$ (V_1+V_2)(V_1^{'}+V_3) (V_1^{'} +V_3{'})(V_2{'}+V_3^{'})$。
Alloy
Alloy搜索的方法是：我給定一個定義域范圍，對這個范圍里所有的定義值都進行檢查。本質是找語句中為假的可能，證明命題為假，因為為假說明命題一定錯。
基礎語法
sig: 類似於class
pred: 用來定義謂詞
舉例：
sig Platform {}
// there are "Platform" things
sig Man{ceiling, floor: platform}
// each Man has a ceiling and a floor Platform
pred Above(m, n: Man){
m.floor = n.ceiling
}
// Man m is "above" Man n if m's floor is n's ceiling
其中m,n:Man表示m,n都是Man的實例
fact: 用來定義已知條件
舉例：
fact {
all m: Man | some n: Man | Above (n, m)
}
// one Man's ceiling is another Man's floor
該示例表示對於任意人來說，都存在某個人在他的上面
assert：表示假設
check: 用於檢驗
assert BelowToo{
all m: Man | some n: Man | Above(m, n)
}
// one Man's floor is another Man's ceiling ?
check BelowToo for 2
// check "one Man's floor is another MAn's ceiling"
// counterexample(反例) with 2 or less platform and men?
for 2：表示范圍，用於舉例的實例個數。這里表示有2個Man和兩個platform。我們的目標是找出不滿足BelowToo的反例來證明該命題是錯誤的。這里一共有2^4種可能，首先第一步，我們就要排除掉不滿足fact的，因為fact是已知條件，如果不滿足fact，則不考慮。然后再在剩下的結果中找出不滿足假設的，若找到，則證明假設有錯誤。
找出的一個反例如下：
從此可以看出對於Man1，Man0在他的下面，但是對於Man0來說，沒有人在他下面，所以這種情況就不滿足假設。
注：當我們舉例時要注意考慮所有情況，而不是自己假設存在的合理情況，比如這里，Man1就在自己的上面，但是它依舊符合fact
abstract：定義抽象，同java
all x: e | F // all: F holds for every x in e
all x: e1, y: e2 | F
all x, y: e | F
all disj x, y: e | F
some: F holds for at least one x in e
no: F holds for no x in e
one: F holds for exactly one x in e
lone: F holds for at most one x in e
set: any number
disj: short of distinct
舉例：
some n: Name, a: Address | a in n.address
// some name maps to some address — address book not empty
no n: Name | n in n.^address
// no name can be reached by lookups from itself — address book acyclic
all n: Name | lone a: Address | a in n.address
// every name maps to at most one address — address book is functional
all n: Name | no disj a, a': Address | (a + a') in n.address
// no name maps to two or more distinct addresses — same as above
RecentlyUsed: set Name
// RecentlyUsed is a subset of the set Name
^: 表示傳遞閉包
+: 表示並集
-: 表示差集
in: 表示子集
.: 表示點乘，和數據庫中的left join相同，但是結果中會去掉相同的那一項
#r: r中的元組數
&: intersection，交集
=: 表示判等
->: 交叉商，笛卡爾乘積
[]: 相當於按key取值
~: 轉置
*: 自反傳遞閉包
{(N0)} + {(N1)} = {(N0), (N1)}
{(N0)} = {(N1)} = false
{(N0)} in none = false
{N0}.{N0, N1} = {N1}
{(N1), (N2)} & {(N0), (N2)} = {(N2)}
{(N0, A0), (N1, A1)} & {(N0, A0), (N1, A2)} = {(N0, A0)}
{(N0), (N1)} -> {(A0), (A1)} = {(N0, A0), (N0, A1), (N1, A0), (N1, A1)}
e1[e2] = e2.e1
a.b.c[d] = d.(a.b.c)
{(N0, A0), (N1, A0), (N2, A2)}[{(N1)}] = {(A0)}
~{(N0, N1), (N1, N2), (N2, N3)} = {(N1, N0), (N2, N1), (N3, N2)}
^{(N0, N1), (N1, N2), (N2, N3)} = {(N0, N1), (N0, N2), (N0, N3), (N1, N2), (N1, N3), (N2, N3)}
*{(N0, N1), (N1, N2), (N2, N3)} = {(N0, N0), (N0, N1), (N0, N2), (N0, N3), (N1, N1),
(N1, N2), (N1, N3), (N2, N2), (N2, N3), (N3, N3)}
<:: 域約束，第一個集合中元組后面的值在在后面指定的集合中
:>: 范圍約束，后面集合中元組前面的一個值在后面指定的集合中
++: 相當於繼承+重載
p ++ q = p – (domain(q) <: p) + q
{(N0, N1), (N1, N2), (N2, A0)} :> {(A0)} = {(N2, A0)}
{(N0, N1), (N1, N2), (N2, A0)} :> {(N0), (N1), (N2)} = {(N0, N1), (N1, N2)}
{(N0), (N1)} <: {(N0, N1), (N1, N2), (N2, A0)} = {(N0, N1), (N1, N2)}
{(N0, N1), (N1, N2), (N2, A0)} ++ {(N0, N1), (N1, A0)} = {(N0, N1), (N1, A0), (N2, A0)}
let: 定義局部變量
if f then e1 else e2: if語句
all n: Name |
some n.workAddress => n.address = n.workAddress
else n.address = n.homeAddress
all n: Name |
let w = n.workAddress, a = n.address |
some w => a = w else a = n.homeAddress
all n: Name |
let w = n.workAddress |
n.address = if some w then w else n.homeAddress
all n: Name |
n.address = let w = n.workAddress |
if some w then w else n.homeAddress
團
團與最大團：無向圖G中任何兩個節點均有邊連接節點子集稱為團。若C是無向圖G的一個團，並且不能再加進任何一個G的結點使其成為一個更大的團，則稱此C為最大團。也就是最大團就是不能被其他團所包含的一個團。
團：
{X2,X4},{X1,X2},{X3,X5},{x1,x3},{x2,x5},
{X2,X6},{X5,X6},{X2,X5,X6}
最大團：
{X2,X4},{X1,X2},{X3,X5},{x1,x3},{X2,X5,X6}
條件隨機場
判別模型: 根據所提供的features進行學習，最后在不同的數據分類之間畫出了一個明顯或者比較明顯的邊界。
生成模型: 先從訓練樣本數據中，學習所有的數據的分布情況，最終確定一個聯合分布，來作為所有的輸入數據的分布。對於新的樣本數據（inference）對應的結果，通過學習到的模型的聯合分布 ，再結合新樣本的特征，通過條件概率就能計算出來 。
有向圖的聯合概率分布：
例如：
圖中的概率如下：
基於計數器的BCP算法是一種容易理解與實現的 BCP 算法。假設每個子句（clause）擁有兩個計數器（counter），一個用於子句中的值1字面量（literal）的計數，一個用於子句中的值0字面量的計數。每個變量（variable）都有兩個列表，其中包含所有子句，其中該變量分別顯示為正值和負值。當為變量分配一個值時，包含此字面量的所有子句將更新其計數器。設實例具有m個子句（clause）和n個變量（variable），並且平均每個子句具有l個字面值（literal）。那么每當給一個變量賦值時，有多少個計數器（counter）需要更新。簡要概述分析過程。
答：l/n表示每個變量平均在每個子句中出現的次數，然后乘以子句的數量m，所以，有一個變量被賦值的時候，會有平均 ml/n 個計數器需要更新，在回溯的時候，每取消一個變量賦值，也會平均有 ml/n 個計數器的更新。
參考鏈接
© 12/28/2019 contributed by Fan zhonghao