維基百科

布林可滿足度問題

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

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

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

背景概念

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

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

一條 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]）就係由若干句子句之間嘅邏輯與組成嘅[3]。

基本定義

編輯

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

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

例如想像返呢條式

 

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

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

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

 

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

解決方法

編輯
睇埋：組合爆發

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

局部搜尋

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

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

 

步驟[4]:p 26：

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

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

解 SAT 器

編輯
睇埋：歸約

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

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

 

噉嘅 CNF，同時兩條問題係「同等」嘅，即係話「若且唯若   係可滿足嘅，  會係可滿足嘅」[9]。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. ↑ polynomial time
  12. ↑ local search
  13. ↑ optimization
  14. ↑ 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. ↑ Barry DwyerBarry Dwyer, in Systems Analysis and Synthesis, 2016.
  4. ↑ 4.0 4.1 4.2 Satisfiability: Algorithms, Applications and Extensions (PDF), SAC 2010 Lecture slides.
  5. ↑ Aho, Alfred V.; Hopcroft, John E.; Ullman, Jeffrey D. (1974). The Design and Analysis of Computer Algorithms. Addison-Wesley. p. 403.
  6. ↑ Massacci, Fabio; Marraro, Laura (2000-02-01). "Logical Cryptanalysis as a SAT Problem". Journal of Automated Reasoning. 24 (1): 165-203.
  7. ↑ 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.
  8. ↑ The International SAT Competition Web Page.
  9. ↑ Reduction from SAT to 3SAT (PDF), Swagato Sanyal.

外拎

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