布爾可滿足性問題

布爾可滿足性問題（有時稱為命題可滿足性問題，縮寫為SATISFIABILITY或SAT）是指在計算機科學中，是確定是否存在滿足給定布爾公式的解釋的問題。換句話說，它詢問給定布爾公式的變量是否可以一致地用值TRUE或FALSE替換，公式計算結果為TRUE。

如果是這種情況，公式稱為可滿足。另一方面，如果不存在這樣的賦值，則對於所有可能的變量賦值，公式表示的函數為FALSE，並且公式不可滿足。例如，公式「a AND NOT b」是可以滿足的，因為可以找到值a = TRUE且b = FALSE，這使得（a AND NOT b）= TRUE。相反，「a AND NOT a」是不可滿足的。^[1]

基本定義和術語

命題邏輯公式，也稱為布爾表達式，由變量，運算符AND（連接，也用∧表示），OR（分離，∨）， NOT （否定，¬）和括號構成。如果通過為其變量分配適當的邏輯值（即TRUE，FALSE）可以使公式為TRUE，則稱該公式是可滿足的。給定公式，布爾可滿足性問題（SAT）是檢查它是否可滿足。這個決策問題在計算機科學的各個領域都至關重要，包括理論計算機科學，複雜性理論，算法，密碼學和人工智能。

布爾可滿足性問題有幾種特殊情況，其中公式需要具有特定結構。文字是一個變量，稱為正文字，或變量的否定，稱為負文字。子句是文字（或單個文字）的分離。如果一個子句最多包含一個正文字，則該子句稱為Horn子句。如果公式是條款（或單個子句）的連接，則公式為合取範式（CNF）。例如，x1是正文字，¬x2是負文字，x1∨¬x2是子句，（x1∨¬x2）∧（¬x1∨x2∨x3）∧x1是聯合範式的公式;它的第一和第三個條款是Horn條款，但它的第二個條款不是。公式是可以滿足的，通過選擇x1 = FALSE，x2 = FALSE和x3任意，因為（FALSE∨¬FALSE）∧（¬FALSE∨FALSE∨x3）∧FALSE求值為（FALSE∨TRUE）∧（TRUE∨FALSE ∨x3）∧TRUE，依次為TRUE∧TRUE∧TRUE（即為TRUE）。相反，CNF公式a∧¬a由一個文字的兩個子句組成，是不可滿足的，因為對於a = TRUE或a = FALSE，它評估為TRUE∧¬TRUE或FALSE∧¬FALSE（即，分別為FALSE）。

對於SAT問題的某些版本，定義廣義聯合範式公式的概念是有用的，即。作為任意多個廣義子句的連接，後者對於某些布爾運算符R和（普通）文字li具有R（l1，...，ln）形式。不同的允許布爾運算符集導致不同的問題版本。例如，R（¬x，a，b）是一個廣義子句，R（¬x，a，b）∧R（b，y，c）∧ R（c，d，¬z）是廣義的聯合正規形式。下面使用此公式，其中R是三元運算符，只有當其中一個參數為時才為TRUE。

使用布爾代數的定律，每個命題邏輯公式都可以轉換為等效的連接法線形式，然而，它可以指數地更長。例如，將公式（x1∧y1）∨（x2∧y2）∨...∨（xn∧yn）轉換為連接法線形式。

(x1∨x2∨…∨xn) ∧

(y1∨x2∨…∨xn) ∧

(x1∨y2∨…∨xn) ∧

(y1∨y2∨…∨xn) ∧ ... ∧

(x1∨x2∨…∨yn) ∧

(y1∨x2∨…∨yn) ∧

(x1∨y2∨…∨yn) ∧

(y1∨y2∨…∨yn);

而前者是2個變量的n個連接的分離，後者由n個變量的2n個子句組成。

SAT是第一個已知的NP完全問題，1971年多倫多大學的Stephen Cook 和1973年國家科學院的Leonid Levin獨立證明了這一問題。在此之前，NP完全問題的概念甚至不存在。證明顯示複雜性類NP中的每個決策問題如何可以簡化為CNF公式的SAT問題，有時稱為CNFSAT。 Cook減少的一個有用特性是它保留了接受答案的數量。例如，確定給定圖形是否具有3色是NP中的另一個問題;如果一個圖表有17個有效的3色，那麼Cook-Levin減少產生的SAT公式將有17個令人滿意的分配。

NP完全性僅指最壞情況實例的運行時間。實際應用中出現的許多實例可以更快地解決。請參閱下面的解算SAT的算法。

如果公式僅限於析取正規形式，即它們是文字連詞的脫節，那麼SAT是微不足道的。當且僅當其連接中的至少一個是可滿足的時，這樣的公式確實是可滿足的，並且當且僅當它對於某個變量x不包含x和NOT x時，連接是可滿足的。這可以在線性時間內檢查。此外，如果它們被限制為完全分離正常形式，其中每個變量在每個連接中恰好出現一次，則可以在恆定時間內檢查它們（每個連接代表一個令人滿意的分配）。但是，將一般SAT問題轉換為析取範式可能需要指數時間和空間;例如，對於聯合正規形式，在上述指數爆炸示例中交換「∧」和「∨」。

SAT的擴展

自2003年以來獲得顯着普及的擴展是可滿足模數理論（SMT），其可以通過線性約束，數組，所有不同的約束，未解釋的函數，等來豐富CNF公式。這樣的擴展通常保持NP完全，但是可以使用有效的求解器來處理許多這樣的約束。

如果允許「for all」（∀）和「there there」（∃）量詞允許綁定布爾變量，則可滿足性問題變得更加困難。這種表達的一個例子是∀x∀y∃z（x∨y∨z）∧（¬x∨¬y∨¬z）;它是有效的，因為對於x和y的所有值，可以找到適當的z值，即。如果x和y都為FALSE，則z = TRUE，否則z = FALSE。 SAT本身（默認）僅使用∃量詞。如果只允許∀量詞，則獲得所謂的重言式問題，即共同NP完全。如果允許兩個量詞，則該問題稱為量化布爾公式問題（QBF），可以顯示為PSPACE完全。人們普遍認為PSPACE完全問題比NP中的任何問題都嚴格，儘管尚未得到證實。使用高度並行的P系統，可以在線性時間內解決QBF-SAT問題。

普通的SAT詢問是否存在至少一個使公式成立的變量賦值。各種變體處理此類任務的數量：

MAJ-SAT詢問所有作業的大部分是否使公式為TRUE。眾所周知，PP是一種概率類。

SAT，計算有多少變量賦值滿足公式的問題，是計數問題，而不是決策問題，並且是#P-complete。

UNIQUE-SAT是確定公式是否只有一個賦值的問題。對於美國來說，它是完整的，描述了由非確定性多項式時間圖靈機解決的問題的複雜性類，當只有一個非確定性接受路徑時它接受並拒絕否則。

當輸入限於具有至多一個令人滿意的賦值的公式時，UNAMBIGUOUS-SAT是給予可滿足性問題的名稱。允許UNAMBIGUOUS-SAT的求解算法在具有若干令人滿意的分配的公式上表現出任何行為，包括無限循環。雖然這個問題似乎更容易，但Valiant和Vazirani已經證明如果有一個實用的（即隨機多項式時間）算法來解決它，那麼NP中的所有問題都可以很容易地解決。

MAX-SAT是最大可滿足性問題，是SAT的FNP推廣。它要求最大數量的條款，任何轉讓都可以滿足。它具有有效的近似算法，但是NP難以精確解決。更糟糕的是，它是APX完全的，意味着除非，否則不存在針對該問題的多項式時間近似方案（PTAS）。

其他概括包括對一階和二階邏輯的可滿足性，約束滿足問題，0-1整數規劃。

視頻