布林可滿足度問題

出自維基百科，自由嘅百科全書

布林可滿足度問題（英文：Boolean satisfiability problem，可以借英文字詞 satisfiability 簡稱 SAT）係一種邏輯同運算上嘅問題，指一個人或者一部電腦攞住一條布林表達式，並且決定條公式有冇可能滿足得到。簡單噉講，布林表達式可以想像成一串「狀態 A 成立、狀態 B 唔成立... 狀態 XXX 成立 / 唔成立」噉嘅句子。即係話解 SAT 嘅人或者電腦要

攞 Input：一條布林表達式
畀 Output：「有可能滿足」或者「冇可能滿足」

呢類噉嘅問題吸引咗唔少電腦科學工作者探究：一方面，SAT 問題喺理論層面有一定影響，對運算複雜度理論有相當嘅啟示；而另一方面，解決呢種問題亦有一定嘅應用價值，對密碼學同人工智能等領域嘅工作嚟講都有用。

背景概念[編輯]

内文：邏輯連接詞同布林表達式
睇埋：合取範式

首先，講講一啲基本嘅邏輯學概念。

一條布林表達式[e 1]會有若干個變數（[e 2] 數值可以係真或者假），而變數之間會有邏輯連接詞[e 3]連接住，形成一句「句子」，而句嘢嘅真假值係有可能判斷嘅，例如以下呢幾句嘢噉[1]：

公式 用日常用語講會係... 變數 連接詞
[e 4] 「A 同 B 都係真確嘅。」—如果 A 同 B 當中是但一個唔成立，呢條公式就係假嘅。（邏輯與）
[e 5] 「A 或者 B 係真確嘅。」—如果 A 同 B 當中是但一個成立，呢條公式就會係真嘅。（邏輯或）
[e 6] 「A 嘅邏輯非。」—如果 A 係真，呢條公式就會係假嘅，而如果 A 係假，呢條公式就會係真嘅。
「A 或者 B 係真」係真，同時「C 唔係真」。

邏輯連接詞嘅概念，仲可以用溫氏圖[e 7]表達：

：
如果一笪區域係屬於 A 或者屬於 B，就填紅色。
：
如果一笪區域係屬於 A 或者屬於 B，就填紅色。
 
：
如果一笪區域屬於 A 同時又屬於 B，就填紅色。
：
如果一笪區域屬於 A 同時又屬於 B，就填紅色。
 

等等。

除此之外，亦要講講 SAT 嘅相關用語。一個字面[e 8]係指一個變數或者一個變數嘅邏輯非，一句子句[e 9]由若干個字面同佢哋之間嘅邏輯或組成—即係例如 噉就係一句子句[2]，而一條合取範式（CNF [e 10]）就係由若干句子句之間嘅邏輯與組成嘅。

基本定義[編輯]

布林可滿足度問題（SAT）做嘅嘢，就係要攞住一條布林表達式，再畀出答案，答「有冇最少一個變數狀態，係可以滿足到呢條公式（令到呢條公式出真）嘅呢？」呢條問題。一個（例如）電腦程式要解一條 SAT 問題，只有兩個可能答案：

  • 真（1）：有最少一個可能嘅變數狀態，係能夠滿足嗰條布林表達式嘅；
  • 假（0）：冇任何變數狀態係可以滿足呢條布林表達式嘅，個程式要證明呢一點；

例如想像返呢條式

如果「A 係真同時 C 係假」或者「B 係真同時 C 係假」，噉呢條式就會係真—呢條式係有可能滿足嘅。舉個實用啲嘅例子，可以想像而家有四個人—阿明、阿儀、阿安同彼得—想約時間開會，希望四個人都出到席，

「阿明淨係禮拜一、禮拜三、禮拜四得閒。」「阿儀禮拜三唔得閒。」「阿安禮拜五唔得閒。」「彼得禮拜二同禮拜四唔得閒。」

就可以當成要同以下嘅式解 SAT 問題[3]:p 3：

答案係，嗰個會一定要係喺禮拜一開。喺現實應用上，SAT 可以複雜得好交關，字面嘅數量遠遠唔只三四個咁少。呢類噉嘅問題，喺理論電腦科學、複雜系統相關研究[4]、密碼學[5]以及人工智能[1]上都頗受關注。

解決方法[編輯]

睇埋：組合爆發

事實表明，SAT 呢種問題可以幾複雜。事實表明，2-SAT（有兩個字面嘅 SAT）同 3-SAT（有三個字面嘅 SAT）並唔難解，當中 3-SAT 係一個 NP 完全[e 11]嘅問題[6]，一個答案啱唔啱可以喺相對快（講緊多項式時間[e 12]）嘅時間之內核實得到。

局部搜尋[編輯]

内文：局部搜尋
睇埋：爬山演算法

要解 SAT，一種可能嘅做法係用局部搜尋[e 13]。局部搜尋係一種最佳化[e 14]技術，起始嗰陣隨機噉試一個可能答案，唔啱用嘅話就對個答案做細幅度嘅修改然後再試，一路重複直到搵到個啱用（但未必完全最好）嘅答案或者過咗時限為止。用呢種方法解 SAT 問題，涉及以下嘅步驟[3]:p 26，想像家吓要評估以下嘅布林表達式：

步驟[3]:p 26：

  1. 隨機噉設定啲變數嘅數值，例如設做
  2. 試下第 1 步產生嗰個答案係咪啱用；
    （唔啱用）
  3. 如果啱用，將手上嗰個答案畀出嚟做最終答案；
  4. 如果唔啱用，就將其中一個變數「反轉」，例如變做
    （「反轉」咗）
  5. 返去步驟 2，直至搵到個啱用嘅答案或者時限過咗為止。

局部搜尋呢種做法，本質上就帶有不確定性：例如可能手上嗰條問題查實有一個正確答案，但係部電腦咁啱唔好彩撞唔中（撞中之前時間到）；又或者條問題實際上有多過一個答案，但係部電腦淨係搵到其中一個。

解 SAT 器[編輯]

睇埋：歸約

解 SAT 器[e 15]顧名思義係指解 SAT 問題嘅演算法。自從 2000 年代起，電腦科學界就有喺度開發解 SAT 器，有搞比賽用獎金鼓勵啲人開發新嘅解 SAT 器[7]。呢啲比賽引起嘅創新，甚至仲有啟發其他電腦科學子領域嘅研究者。

解 SAT 器有好多種唔同嘅做法，一種幾常見嘅做法係將手上嗰條問題歸約做 3-SAT 問題：一條噉嘅演算法會攞一條 SAT 問題 ，將 轉化做一條 3-SAT 問題 ，即係例如將一條有成六個變數咁多嘅 SAT 問題轉化做

噉嘅 CNF，同時兩條問題係「同等」嘅，即係話「若且唯若 係可滿足嘅， 會係可滿足嘅」[8]。3-SAT 問題係 NP-完全嘅，如果一條 SAT 問題可以轉做 3-SAT 當係 3-SAT 噉嚟解，就有可能令到條問題易解好多。

睇埋[編輯]

參考[編輯]

用咗嘅重要概念嘅英文名：

  1. ↑ Boolean expression
  2. ↑ variable
  3. ↑ logical connectives
  4. ↑ A and B
  5. ↑ A or B
  6. ↑ negation of A
  7. ↑ Venn diagram
  8. ↑ literal
  9. ↑ clause
  10. ↑ 全名 conjunctive normal form
  11. ↑ NP-complete
  12. ↑ polynomial time
  13. ↑ local search
  14. ↑ optimization
  15. ↑ SAT solver

引用咗嘅學術文獻或者網頁：

  1. ↑ 1.0 1.1 Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021-2035.
  2. ↑ (2011). Clause. In: Sammut, C., Webb, G.I. (eds) Encyclopedia of Machine Learning. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-30164-8_116
  3. ↑ 3.0 3.1 3.2 Satisfiability: Algorithms, Applications and Extensions (PDF), SAC 2010 Lecture slides.
  4. ↑ Aho, Alfred V.; Hopcroft, John E.; Ullman, Jeffrey D. (1974). The Design and Analysis of Computer Algorithms. Addison-Wesley. p. 403.
  5. ↑ Massacci, Fabio; Marraro, Laura (2000-02-01). "Logical Cryptanalysis as a SAT Problem". Journal of Automated Reasoning. 24 (1): 165-203.
  6. ↑ Cook, Stephen A. (1971). "The complexity of theorem-proving procedures" (PDF). Proceedings of the third annual ACM symposium on Theory of computing - STOC '71. pp. 151–158.
  7. ↑ The International SAT Competition Web Page.
  8. ↑ Reduction from SAT to 3SAT (PDF), Swagato Sanyal.

外拎[編輯]

由「https://zh-yue.wikipedia.org/w/index.php?title=布林可滿足度問題&oldid=2124701」收