conjunctive normal form, MiniSat

SAT solver 是解決 SAT 問題的程式的統稱，這裡介紹一些先備知識，以及 miniSAT 這套開源的 SAT solver。

一些名詞定義

• variable
  boolean function 裡面用到的那些值就叫 variable，例如: (¬a ∨ b ⊕ x)，a, b, x 就是它的 variable，當然 variable 要取什麼名子都可以。

• literal
  在 boolean function 中實際出現的 variable 就叫 literal，其中帶有 NOT(negation, ¬) 的叫 negative literal，沒有的叫 positive literal，例如: (¬a ∨ a)，就有 a 的 negative literal、positive literal 各一個。

• clause
  clause 就是一個括號中全部都只有 OR(disjunction, ∨)，例如 (x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1，裡面就有三個 clause(最後 ¬x1 這樣單獨一個也是)。

conjunctive normal form

conjunctive normal form 簡稱 CNF，在數位電路中又叫作 product of sums(先作一堆 OR 在 AND 起來的意思)，簡單來說就是把一堆 clause 給 AND 起來。

1
2
3
4
5
6

# 直接給例子比較好明白
# 以下都是 CNF
(a ∨ b ∨ ¬c) ∧ (a ∨ b) ∧ (a ∨ c)
(x ∨ y) ∧ (¬x ∨ y)
(x1 ∨ x2) ∧ (x2 ∨ ¬x3) ∧ x3

可以發現上一篇文中舉的 Circuit satisfiability problem、四色問題都是 CNF 的形式，而我們之後討論 SAT，以及 SAT solver 吃的資料都是用 CNF 格式，因為:

• 任何 boolean function 都可以轉成 CNF
  可以運用 double negative law, De Morgan’s laws, distributive law 將所有的 boolean function 轉成 CNF 形式(假設真的有人會點進來看這篇文，應該都會學過邏輯設計之類的東西吧)。

1
2
3
4

# 舉幾個例子
a ⊕ b -> (¬a ∨ ¬b) ∧ (a ∨ b)
(a ∨ (b ∧ c)) -> (a ∨ b) ∧ (a ∨ c)

• CNF 有很好的結構
  一個 clause 裡面只要有一個 true，那該 clause 就為 true(因為 clause 裡都作 OR)。所有的 clause 都必須為 true，boolean function 才會為 true(因為把每個 clause AND 起來)。

  首先這樣的形式很好被理解(可以注意到大部份我們在寫程式時，if 條件多半都會寫成 AND of ORs)。

  在來想像一下你有幾千個 variable 要作處理，這時候整個 boolean function 要再增加幾百個有關的 variable 進去，CNF 只需要簡單的在 AND 新的邏輯就行了。

  最後當我們在解決 SAT 問題，對一個 variable assign true 或 false 來測試 boolean function 時，簡單的檢查有沒有 clause 全部的 literal 都是 false 就能知道這樣的賦值方式會不會 unsatisfiable。

  試想一下你有一個邏輯非常複雜，一大堆的巢狀邏輯包在一起的時候，你如何處理以上的情況? 比起殺死一堆腦細胞，簡化問題是更好的作法。

DIMACS CNF format

餵給 SAT solver 吃的 CNF 有個通用的格式叫 DIMACS CNF format，就是副檔名叫 XXX.cnf 的純文字檔。

1
2
3
4
5
6
7
8
9

# DIMACS檔案格式如下
# #開頭是我的說明 不是 DIMACS 的註解
c 
c c開頭的這些是 DIMACS 註解
c
p cnf 3 2    # 第一個數字是 variable 數、第二個是 clause 數
1 -3 0       # 之後的每行是一個 clause， variable 名稱都是數字(從1開始，0是行結尾的意思)
2 3 -1 0     # 這行代表 (2 ∨ 3 ∨ ¬1)

這裡可以找到一系列問題的 DIMACS 檔案
http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html

MiniSat

MiniSat 是一個很棒的 SAT solver，在 2005 年拿下了一系列 SAT 比賽的冠軍，更重要的是它是 open source 的，只有幾千行簡潔精練的 code，可以在之後通過對 MiniSat 的研究，來為自製 SAT solver 有一個比較高的起點。

reference

wiki SAT
https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

wiki CNF
https://en.wikipedia.org/wiki/Conjunctive_normal_form

CNF 格式
http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html

Boolean Satisfiability Problem

什麼是 SAT?

Boolean satisfiability problem 簡稱 SAT，簡單說就是用來判斷一組給定的布林函數，是否可以找到一組變數賦值能使其為真。

1
2
3
4
5
6
7

# a, b, c 任一為 true 該式都為 true，也就是找的到解
# satisfiable
(a ∨ b ∨ c)
  
# a 不論為 true 或 false 該式都為 false，即找不到能使該式為 true 的 assign 方式
# unsatisfiable
(a ∧ ¬a)

SAT 的重要性

• SAT 是第一個 NP-Complete problem
  在應用的角度只要知道 NP-Complete problem 很難，沒辦法有效率找到最佳解(但可能可以有效率的找到近似最佳解)，以及 NP-Complete problem 可以在多項式時間內互相轉換(就是說你可以拿一個 NP-Complete problem 來解另外一個)，這樣就夠了。

• 解 SAT 的方法發展的很好
  SAT 做為最古老且知名的 NP-Complete problem，已經有許多演算法跟技巧被發明出來解它，目前最好的那些 SAT solver 可以解到上萬個變數，我們知道 NP-Complete problem 可以在多項式時間內互轉，而 SAT solver 的效率又不錯，那麼 SAT 自然是很有實用性的。

SAT 的應用

SAT 被應用在如 EDA 領域的測試、驗證，AI 領域如自動定理證明 ，網路上還查的到很多，但一時間看不懂所以然的我就不列了，以下舉幾個例子。

• Circuit satisfiability problem
  給出一個電路，是否有 input 能讓 output 為 true

1
2
3
4
5

# 考慮下列 AND gate
C = A . B
# 有對應如下的 boolean function
(¬a ∨ ¬b ∨ c)∧(a ∨ ¬c)∧(b ∨ ¬c)
# 思考拼湊一下可以發現能讓它 satisfiable 的值就是 AND gate output true 的值

如果運用這種方法，就可以堆積出複雜電路的 boolean function，可以測試一個電路能不能 output true，也就是說能知道它會不會是無用的電路(可以化簡)。

這種方法叫做 Tseitin transformation，有興趣可參考 wiki:https://en.wikipedia.org/wiki/Tseytin_transformation

• 四色問題
  如果地圖上相鄰的兩個區域不能畫相同的顏色，那不管這張地圖多複雜，最少都可以用四種顏色畫出它。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

# 考慮區域1跟2相鄰
# 下列四個變數代表區域1能被畫的顏色
R1 B1 G1 Y1
# R1 B1 G1 Y1 只能有一個為 true
(¬R1 ∨ ¬B1)∧
(¬R1 ∨ ¬G1)∧
(¬R1 ∨ ¬Y1)∧
(¬B1 ∨ ¬G1)∧
(¬B1 ∨ ¬Y1)∧
(¬G1 ∨ ¬Y1)
# 區域2相同
R2 B2 G2 Y2
(¬R2 ∨ ¬B2)∧
(¬R2 ∨ ¬G2)∧
(¬R2 ∨ ¬Y2)∧
(¬B2 ∨ ¬G2)∧
(¬B2 ∨ ¬Y2)∧
(¬G2 ∨ ¬Y2)
# 區域1跟區域2不能同顏色
(¬R1 ∨ ¬R2)∧(¬B1 ∨ ¬B2)∧(¬G1 ∨ ¬G2)∧(¬Y1 ∨ ¬Y2)
# 將全部 AND 起來，就能得到一個 boolean function，
# 一定找的到 true 的賦值方式，而且區域1,2不同色，就
# 算區域更多也不會用超過四種顏色。

不過我們知道一張地圖的區域最少能用幾種顏色畫，讓相鄰的區域不同顏色，這樣的事情要幹嘛? 當然是有用處的。

例如很多地方都蓋了基地台，但只要是相鄰的基地台使用相同的頻率，就會相互干擾導致收訊不良。因此對應到四色問題，我們知道最少用四種頻率的基地台就能解決干擾了。

reference

一個介紹 SAT 的英文文章
http://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html