--- # System prepended metadata title: state-of-the-art in SAT solving tags: [108-2, ' Formal Languages'] --- --- 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 如下圖 > ![](https://i.imgur.com/AKeVhzT.png) 如果這裡的變數 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)$。 ![](https://i.imgur.com/hfWKUjQ.png) ### 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) 至少是指數級函數 ![](https://i.imgur.com/euUonoY.png) ![](https://i.imgur.com/0cyBTG6.png) ## 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) * 用 這個例子的 unit-rule 概念，加上一些 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) > 硬體安全應該會遇到