主題研究►SAT Problem

(二) conjunctive normal form, MiniSat

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