主題研究►SAT Problem

(一) SAT problem 介紹

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