布林可滿足度問題

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

攞 Input：一條布林表達式

畀 Output：「有可能滿足」或者「冇可能滿足」

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

背景概念

内文：邏輯連接詞同布林表達式

睇埋：合取範式

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

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

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

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

： 如果一笪區域係屬於 A 或者屬於 B，就填紅色。 ${\displaystyle A\lor B}$： 如果一笪區域係屬於 A 或者屬於 B，就填紅色。  ： 如果一笪區域屬於 A 同時又屬於 B，就填紅色。 ${\displaystyle A\land B}$： 如果一笪區域屬於 A 同時又屬於 B，就填紅色。

等等。

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

基本定義

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

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

例如想像返呢條式

${\displaystyle (A\lor B)\land (\neg C)}$

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

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

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

${\displaystyle ({\text{ 禮 拜 一 }}{\text{ }}\lor {\text{ }}{\text{ 禮 拜 三 }}{\text{ }}\lor {\text{ }}{\text{ 禮 拜 四 }}{\text{ }})\land (\neg {\text{ }}{\text{ 禮 拜 三 }}{\text{ }})\land (\neg {\text{ 禮 拜 五 }}{\text{ }})\land (\neg {\text{ 禮 拜 二 }}{\text{ }}\land \neg {\text{ 禮 拜 四 }}{\text{ }})}$

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

解決方法

睇埋：組合爆發

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

局部搜尋

内文：局部搜尋

睇埋：爬山演算法

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

${\displaystyle (x_{1}\lor \neg x_{2}\lor \neg x_{3})\land (\neg x_{1}\lor \neg x_{3}\lor x_{4})\land (\neg x_{1}\lor \neg x_{2}\lor x_{4})}$

步驟^{[4]:p 26}：

1. 隨機噉設定啲變數嘅數值，例如設做

   ${\displaystyle x_{4}=0,x_{1}=x_{2}=x_{3}=1}$

2. 試下第 1 步產生嗰個答案係咪啱用；

   ${\displaystyle (1\lor 0\lor 0)\land (0\lor 0\lor 0)\land (0\lor 0\lor 0)=0}$（唔啱用）

3. 如果啱用，將手上嗰個答案畀出嚟做最終答案；
4. 如果唔啱用，就將其中一個變數「反轉」，例如變做

   ${\displaystyle x_{1}=x_{2}=x_{3}=x_{4}=1}$（${\displaystyle x_{4}}$「反轉」咗）

5. 返去步驟 2，直至搵到個啱用嘅答案或者時限過咗為止。

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

解 SAT 器

睇埋：歸約

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

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

${\displaystyle (x_{1}\lor \neg x_{2}\lor \neg x_{4})\land (x_{2}\lor x_{3}\lor x_{5})\land (x_{1}\lor x_{4}\lor \neg x_{6})}$

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

睇埋

• 運算複雜度理論