---
tags: 108-2, Formal Languages
---
# state-of-the-art in SAT solving
::: info
### 以下內容和期末考無關
:::

## 1. Introduction
* 理論上，現在 NP-Complete 問題的複雜度至少是指數時間。那要是遇到 NP-Complete 問題該怎麼辦？

第七章談到：「任一 NP-Complete (以下簡稱 NPC) 問題可在多項式時間內歸約成 3SAT 問題」

有些人就在研究如何加速解 3SAT 問題，如果解 3SAT 足夠快，那就相當於加速所有 NPC 問題，但在這裡我們能做的事情是**實務面**的，比如說 pruning 這種限縮 search space 的方法，時間複雜度依然是指數級的。

### 1-1. how to prune search space?
> 給個例子看 pruning 的想法
::: warning
### Q1.
Determine whether the given boolean formula $F = (a + b)(a’ + b’ + c)$ is satisfiable; that is, find a set of variable assignment such that the formula evaluates to 1.
:::
> 每一個 SAT 問題實例可以簡單的轉為等價的 3SAT 問題實例，這邊省略。
* 對於 n 個變數的 SAT 問題，worst case 需要窮舉 2^n^ 種可能。
* 用窮舉法 (brute force) 解 SAT 問題需要時間複雜度 $O(2^n)$
* 這個 SAT 問題實例完整個 search space 如下圖
> 

如果這裡的變數 a 是有意義的，比方說 a=1 表示系統通電，a=0 表示系統斷電，當系統斷電時就不用考慮 F 的 satisfiability。那就只需考慮 a=1，我們可把 F 改為以下的 F'：
::: warning
Modify that boolean formula to $F' = (a + b)(a’ + b’ + c)(a)$
:::
* 把該實例的 search space 從 2^5^ prune 成 2^4^
* 當 $O(2^n)$ 的 n 非常大的時候，能夠砍成 $O(2^{n-1})$ 甚至 $O(2^{n-k})$ 在實務上都可能是很大的幫助，當然理論上他們都還是 $O(2^n)$。

### 1-2. Recap of Asymptotic Notation
*[演算法課本]: Thomas H. Cormen. Charles E. Leiserson. Ronald L. Rivest. Clifford Stein. Introduction to Algorithms. Third Edition.

借用 演算法課本 的 Asymptotic Notation：
f(n) 需要在 n 足夠大 (大過某個整數 $n_0$ ) 之後才會呈 g(n) 的成長速度。
要是能夠把要處理的 n 壓得盡量小，最好能小於 $n_0$，可能所需計算時間 f(n) 就不會太誇張。
* 對於 NPC 類的問題，這裡的 g(n) 至少是指數級函數


## 2. Example

舉個例子，我們要解一個 CLIQUE 問題的 instance

1. 如果只是要解 **an instance** of that problem，可以考慮直接暴力解 (brute force)。
2. 如果常常遇到該類問題，每處理一個 instance 都用暴力解所需時間可能是無法接受的，可能就需要設計專門的演算法來加速。
3. 設計一組 mapping reduction，能夠把該類問題和 3SAT **互轉**。
* 3-1. 舉個例子，我們要解一個 CLIQUE 問題的 instance $c_1$
* 3-2. 設計一個 mapping reduction $T$，使得 $T(c_1)$ 成為一個 3SAT 問題的 instance，記為 $3SAT_1 = T(c_1)$
* 3-3. 設計一個 mapping reduction $T^{-1}$，使得 $T^{-1}(3SAT_1)$ 成為一個 CLIQUE 問題的 instance，記為 $T^{-1}(3SAT_1) = c_1$
> 當然，我們希望這裡兩次的 reduction 加上解 3SAT 所需時間，比直接解原本的問題還少，不然乾脆解原本的問題就好了。

## 3. sota SAT solver
* [minisat-in-your-browser](http://www.msoos.org/2013/09/minisat-in-your-browser/)
* [minisat](http://minisat.se/)
...

對於一般沒要拚演算法的人，只要會抓 SAT solver 下來用就好了，需要做的事情是把你遇到的 NPC 問題 map 到 SAT 問題，再把解完的 SAT assignment map 回來。

### 3-1. algorithms in SAT solvers
> 同學不需要知道現今 SAT solver 是怎麼設計的，這裡只是提供一些 general trick 的名字，維基百科其實都有寫運作原理，詳細設計的方式應該維基百科有附原始 paper 出處。
* DPLL (conflict-driven learning)
* 用 <a href="#1-1-how-to-prune-search-space" smoothhashscroll> 這個例子的 unit-rule 概念</a>，加上一些 resolution 的方法，動態產生新子句。
* chronological backtracking
* 承 DPLL 產生的新子句，如果發生 conflict，例如 (a)(a')，便可以直接 break 掉接下來的搜尋，backtrack 回發生 conflict 之前的狀態。
* 2-literal watching
* 建立 watching window，一次只看兩個 variable 造成的 conflict，比一次看整條 formula 效率高。

## 4. SAT competetion
http://www.satcompetition.org/
https://satcompetition.github.io/2020/
* 每年都有 SAT competition 在拚更好更快的 SAT solver

## 5. Other application - Hardware Security
* 每一個 boolean formula 可視為一個電路單元，其中每一個 literal(variable) 對應一個 input 要給 0 還是 1。

* 對於台積電或瑞昱這種以賣 IC 或是矽智財維生的公司，很怕被其他公司抄走他們的技術，因此大多以申請專利保護他們公司設計出的電路。

* 但他們產品賣出去還是可能被人拿來研究，看要怎麼照抄他們設計出來的電路。但是每個電路單元可以寫成一個 SAT 問題實例，直接丟一個 SAT solver 下去解就知道這個電路單元該輸出 1 還是 0 了：稱作 SAT-attack。

* 這樣即使不知道電路內部的 layout 是怎麼設計的，還是可以做出功能一模一樣的偽造電路，可能偽造電路的體積、能耗比不上原本的，但是至少功能一樣，就能用更低價去搶市場。

## 6. Conclusion
* 因為任一 NPC 問題皆可在多項式時間內歸約到 3SAT，只要 3SAT (等價於 SAT) 解的足夠有效率，就相當於在實務上所有 NPC 問題都能有效率的解掉 (即便是用指數級複雜度的演算法)。
* 也有可能遇到要解的 NPC 問題真的太難，設計 mapping reduction 的 overhead 其實大到不行，可能還是暴力解原本的 NPC 問題比較快。

* 有興趣的同學可找系上吳凱強老師聊聊。

## 7. Further reading:

* SMT problem
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
> 程式安全應該會遇到

* SAT attack
* [logic-locking (防禦 SAT attack)](https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7495588)
> 硬體安全應該會遇到