可滿足性問題的精確算法和計算復雜性

陳建二，楊 偉

（廣州大學計算機科學與網絡工程學院，廣東 廣州 510006）

可滿足性問題是計算機科學中最重要且十分著名的問題之一。在理論計算機科學的研究中，可滿足性問題是第一個NP（Non-deterministic Polynomial，NP）完全問題［1］，在計算困難問題的研究中起著重要作用［2］。實踐中可滿足性問題是解決很多應用領域問題的基礎，包括人工智能［3］、模型檢查［4］、自動推理［5］、計算機輔助設計［6］、數據庫［7］、機器人學［8］、調度［9］、電路設計［10］、計算機體系結構設計［11］和計算機網絡［12］等。

布爾變量是只能采用布爾值1（TRUE）或0（FALSE）的變量。布爾函數是布爾變量上輸出布爾值的函數，僅使用邏輯運算∧（AND）、∨（OR）和?（NOT）。對布爾函數F賦值是給F中的每個變量賦一個確定的0或1的布爾值，如果F在賦值集合π下輸出1，則π滿足F，稱布爾函數F是可滿足的；否則F是不可滿足的。

文字是布爾變量x或x的否定ˉx，子句C是文字的析取，C＝x1∨x2∨…∨xk，其中，xk表示文字。當增加新的文字x到子句C上時，可以得到一個新的子句C′＝x∨x1∨…∨xk，也可以直接寫成C′＝x∨C。CNF公式F是一個合取范式的布爾函數，F＝C1∧C2∧…∧Cm，其中，Cm表示子句，同樣也可以在CNF公式中添加或刪除一個子句來得到新的CNF公式。每個布爾函數都可以寫成合取范式［2］?？蓾M足性問題定義如下：

可滿足性（SAT）：給定CNF公式F，確定F是否可滿足。

SAT是NP完全問題，除非有P＝NP，否則SAT問題在多項式時間內不能有效求解，P＝NP在計算機科學和數學領域共識中是不成立的。

本文從標準計算復雜性理論的角度論述了SAT問題的精確算法和計算復雜性。精確算法指的是對每個輸入實例輸出正確解的算法，并且根據輸入實例的參數對其（最壞情況）運行時間有一個已證明的上界。這與啟發式算法是一致的，啟發式算法的正確性可能不會被正式驗證而且其運行時間上限也可能不會被指定。文章重點論述了SAT問題的算法發展，算法（最壞情況）復雜性分析和復雜度上界；對一些著名的有意義的算法結果進行解釋和分析，并討論它們的意義；介紹了最近幾年相關領域的研究進展；最后簡要分析了已經在許多領域取得成功應用的啟發式算法在SAT問題中的應用情況。

1 基礎概念和相關技術

設CNF公式F＝C1∧C2∧…∧Cm為SAT問題的一個實例，Cm表示子句。以下情況可以進行預處理：

（1）如果一個子句Ci包含空文字，那么Ci不可能被滿足。對于這樣的實例F，直接輸出NO；

（2）如果一個子句Ci只包含一個文字x（單位子句），為了滿足F，必須令x＝1來滿足Ci；

（3）如果公式F包含文字x且不包含ˉx，那么可以令x＝1來滿足F中包含x的子句，而且不影響F中其他子句的滿足性；

（4）如果一個子句Ci同時包含一個變量x和它的否定，那么Ci總是可滿足的?？梢院雎宰泳銫i（不需要確定x的值）。

編寫一個簡單的算法可以處理上述情況。預處理完成之后，CNF公式就是明確的。下面的研究放在明確的SAT問題實例上。

SAT算法的發展有兩種基本技術：消解和分支搜索。這兩種技術已經被證明在SAT算法分析、計算復雜性以及在SAT問題的算法開發中有著重要作用。

1.1 消解

消解技術是由Davis等［13］提出的，設C1＝x∨C′1、C2＝ˉ∨C′2為兩個子句，分別包含一個變量x和它的否定ˉx，其中，C′1和C′2是子句。變量x上C1和C2的消解子句為C′1∨C′2。其中，子句C′1和C′2可能有共同的文字，那么就需要刪除C′1∨C′2中的重復文字。F為CNF公式，F在變量x上的消解也是CNF公式，該公式通過刪除F中包含x和的所有子句，并將F中所有子句的消解子句添加到變量x上獲得。具體如下：

其中，F0是子句既不包含x也不包含的CNF公式。那么F在變量x上的消解式為

下面給出定理，并對完整性進行證明。

定理1（消解原理） 設x是一個確定的CNF公式F中的任意變量，F是可滿足的當且僅當DPx（F）是可滿足的。

證明設F是變量集X＝｛x，x2，…，xn｝上的CNF公式，如（1）所示，在變量x上的消解DPx（F）如（2）所示。

假設F是可滿足的。π是F的一個可滿足賦值集合，π（x）＝x*，π（xk）＝（2≤k≤n），其中，x*和是布爾常數。設π′為CNF公式DPx（F）中變量｛x2，…，xn｝的賦值集合，π′（xk）＝（2≤k≤n）。如果π（x）＝x*＝0，那么由于π（F）＝1，必須有π（x∨Ci）＝1，因此π′（Ci）＝1（1≤i≤s）（F是明確的，Ci既不包含x也不包含ˉx）；如果π（x）＝x*＝1，那么π（ˉx）＝0，必須有π′（C′j）＝1（1≤j≤t）。在這兩種情況下，總有π′（Ci∨C′j）＝1（1≤i≤s和1≤j≤t）。此外，由于F0既不包含x也不包含，有π′（F0）＝π（F0）＝1。因此，π′（DPx（F））＝1。DPx（F）是可滿足的。

另一方面，假設DPx（F）是可滿足的，π′是可滿足DPx（F）的變量｛x2，…，xn｝上的賦值集合。如果π′（Ci）＝1（1≤i≤s），那么除了π′之外，指定x＝0，則ˉx＝1，賦值滿足F中的所有子句；如果對于某些i0，有π′（Ci0）＝0，由于π′（DPx（F））＝1，可得π′（Ci0∨C′j）＝1（1≤j≤t），即π′（C′j）＝1（1≤j≤t）。這種情況下，在π′之外指定x＝1，滿足公式F。因此，只要DPx（F）是可滿足的，公式F就是可滿足的。證明完成。

根據消解原理，要判定SAT的一個實例F是否可滿足，只需判定F中任意變量x上F的消解DPx（F）是否可滿足。消解原理消去了SAT實例F中變量本身和它的否定都出現的變量。不好之處在于DPx（F）是通過從F中刪除s＋t個子句，然后向F中添加s×t（最大）個子句來獲得。當s和t較大時，這會明顯增加實例的大小，因此，消解原理不能保證總是有效地解決SAT問題，但是在子句數量較少的情況下，消解原理是非常有用的，它減少了CNF公式中的變量數量，不會顯著增加實例大小。目前，消解原理仍然是大多數啟發式算法的基礎，這些算法可以有效地解決一組非常大的SAT實例。

1.2 分支搜索

算法1是基于分支和搜索技術的SAT算法，F［x＝0］（或F［x＝1］）為變量x賦值0（或1）。F［x＝1］是通過刪除包含x的所有子句（由于x＝1而滿足），并刪除文字（因為通過賦值x＝1＝0），獲得的CNF公式。

?

SAT-Alg（F）顯然能夠求解SAT問題：如果F是可滿足的，那么對F的一個滿意賦值必須給變量x賦值，這個值可以是0或1。因此，F0＝F［x＝0］和F1＝F［x＝1］中的至少一個是可滿足的，SAT-Alg（F）步驟4輸出YES。反之，如果F不可滿足，那么F［x＝0］和F［x＝1］都不可滿足，則SAT-Alg（F）第4步輸出NO。

將n個變量上輸入實例F的SAT-Alg（F）時間復雜度記為T（n）。F0和F1最多都有n－1個變量，有以下遞推關系，其中，L（F）是輸入實例F的長度：

容易得到T（n）＝O（2nL（F）），有如下定理：

定理2SAT-Alg在O（2nL）時間內解決有n個變量、長度為L的SAT實例F。

許多參數可以用來衡量CNF公式的“大小”，也可以衡量SAT算法的時間復雜度。子句Ci的大?。麮i｜是Ci中的文字數。CNF公式F＝C1∧C2∧…∧Cm，用n（F）表示F中變量的個數，m（F）表示F中子句個數，表示F的長度。一般情況下用n、m和L來表示這些參數。在一個明確的CNF實例中，有如下關系：n，m≤L，L≤nm，m≤2n。SAT是NP完全的，不期望SAT算法在這些參數多項式時間內運行。無論使用哪種參數來分析時間復雜性，SAT算法在最壞情況下的運行時間都是該參數的時間上界。

一種典型的基于分支搜索技術的SAT算法A的工作原理如下：在CNF公式F上，如果F足夠簡單，則算法A直接求解F。否則算法A生成CNF公式的集合｛F1，…，Fc｝，其中，c＞1，使得F是可滿足的當且僅當｛F1，…，Fc｝中至少一個公式是可滿足的。然后算法A遞歸地處理公式F1，…，Fc。F上的分支和搜索算法A可以描述為一個搜索樹TA，其中，根用實例F標記，搜索樹TA中用CNF公式F′標記的節點vF′，如果用算法A直接求解F′，則節點vF′是TA的葉子，對于公式F′，算法A生成一組CNF公式集合｛F′1，…，F′c｝，并遞歸地處理這些公式，節點vF′在搜索樹TA中有c個孩子，分別標記為F′1，…，F′c。算法A的執行對應從根開始的搜索樹TA的深度搜索遍歷。

使用一個參數q（n、m或L）來度量算法A的時間復雜度。將參數值q的實例F分支到c個實例F1，…，Fc，實例F1，…，Fc的參數值q－d1，…，q－dc分別減小di，di＞0。將＃（q）記為參數值q實例上算法A的搜索樹TA中的葉子數，那么可以得出如下遞推關系（算法A在q≤1時不分支）：

為了求解遞推關系（4），用pA（x）＝xq －定義了（4）的分支多項式。設x0為多項式pA（x）的最大根，可以證明x0≥1（文獻［14］）。從關系式（4）中通過對q的歸納，容易驗證＃（q）≤x0q。因此，基于參數值q的CNF公式的算法A的搜索樹TA中節點數邊界為。當q≤1時，如果能在多項式時間內求解SAT實例，而且在多項式時間內由實例F生成實例F1，…，Fc，則算法A在參數q實例上的運行時間為

討論SAT算法時間復雜度的多項式上界因子，對所選參數q使用符號O*（f（q））來表示O（LO（1）f（q）），即O*（f（q））具有隱藏在O*－符號中L的多項式因子。如前所述，測量分支的時間復雜度并通過參數q進行搜索，得到算法分支多項式的最大根等于x0，則算法運行時間為O*）。

根據給定的實例結構，上述討論可以很容易地推廣到使用多個分支規則的SAT算法，定理如下：

定理3讓A是基于參數q分支和搜索技術的SAT算法。如果算法A有多個分支規則，每個分支規則都有一個相應的分支多項式，那么算法A的運行時間是O*（），其中，xmax是所有這些分支多項式的最大根。

2 基于參數n的算法

如定理2所示，SAT-Alg算法在時間O*（2n）內解決SAT問題。通過檢查給定CNF公式的所有2n賦值，SAT問題可以在時間O*（2n）內得到解決。那么是否能比這個基本的算法做得更好？這是理論計算機科學中長期存在的開放性問題。文獻［15］中提出了強指數時間猜想（Strong Exponential Time Hypothesis，SETH）。

SAT問題不能在O*（cn）（c＜2，c為任意常數）時間內求解。

在最近的研究中，SETH被廣泛用于著名的計算優化問題開發計算下限（如文獻［16］的14.5節）。在SAT算法和復雜性研究中，任何一種算法如優于基本SAT算法都是一個重大的進步，也將是許多其他優化問題算法研究的一個重要進展。

如果使用參數n來度量算法的復雜度，那么SETH為更優的算法開發留下了很少的空間。SAT算法的研究熱點已經發展到具有各種限制條件的算法研究上。

k-可滿足性（k-SAT）：給定CNF公式F，其中，子句大小以k為界，確定F是否可滿足。

當k＝2，3時，k-SAT問題特別有趣。2-SAT問題在多項式時間內是可解的，屬于P類［17］。3-SAT問題是一個非常著名的NP完全問題，它在NP完全性理論、SAT算法和計算復雜性的研究中起著關鍵的作用。接下來重點討論3-SAT問題的算法，討論如何將這些算法推廣到一般k-SAT問題。

為了研究運行速度快于O*（2n）的3-SAT算法，筆者根據Monien等［18］的文章從簡單分支和搜索算法（算法2）開始，在不喪失一般性的情況下，輸入實例F是明確的—可以通過多項式時間的預處理使F明確。

?

首先，如果F沒有大小為3的子句，如步驟1，那么F是一個2-SAT實例，其可滿足性可以在多項式時間內確定［17］。

3SATms算法中為了滿足公式F，必須滿足子句（l1∨l2∨l3），滿足F的賦值必須將值1賦值給3個文字l1、l2和l3中的至少一個?？偣灿?組對文字l1、l2和l3的賦值可以滿足子句（l1∨l2∨l3）（僅排除賦值l1＝l2＝l3＝0），F1中的賦值l1＝1涵蓋了這7組賦值中的4個（l1＝1，l2和l3是0或1），函數F01中的賦值l1＝0，l2＝1涵蓋了7組賦值中的兩個（l3是0或1），該算法步驟3中的3個賦值覆蓋了對文字l1、l2、l3的所有可能賦值，它們可以對輸入實例F進行可滿足賦值。這證明了該算法的正確性，即當且僅當F1、F01、F001中至少有一個可滿足，輸入實例F才是可滿足的。

為了分析算法3SATms的復雜度，設輸入實例F是明確的，3個文字l1、l2和l3來自3個不同的變量。如果F有n個變量，那么函數F1、F01和F001分別最多有n－1、n－2和n－3個變量。因此，如果將＃（n）設為3SATms在輸入n個變量情況下搜索樹中的葉數，那么就有如下遞推關系（F是明確的，如果n≤2，那么F就不能有大小為3的子句）：

遞推關系（5）的分支多項式為p（x）＝xn－xn－1－xn－2－xn－3，其最大根為1.83…，通過上述討論，得到如下定理：

定理4算法3SATms在時間O*（1.84n）內求解3-SAT問題。

算法3SATms可以進一步改進，并且推廣到求解一般k的k-SAT問題。對于整數k（k≥3），基于此方法的算法在時間O*（）內求解k-SAT問題，其中，ck是方程ck＝2－1的最大根（ck＜2），當k增加時，ck接近2。例如，c3＝1.619，c4＝1.839，c5＝1.928，c6＝1.966［18］。

?

對SAT-Alg和3SATms算法的討論表明，基于分支和搜索的SAT算法的效率取決于如何為給定SAT實例F生成集合C＝｛F1，…，Fc｝，使得F是可滿足的當且僅當C中至少有一個實例是可滿足的。一般來說，集合C中的實例越少，其參數值n的減少越多，算法的效率就越高。這一結論導致了一系列改進運行時間的3-SAT算法，O*（1.579n）、O*（1.505n）、O*（1.497n）和O*（1.476n）（文獻［19］）。這種方法產生的算法需要檢查SAT實例詳細的結構，并且需要繁瑣復雜的逐步分析。

相比之下，Sch?ning［19］提出了一種隨機3-SAT算法，該算法從隨機選擇的初始賦值開始，對所選賦值應用局部搜索。Sch?ning的算法如算法3所示，其中，b是一個數字可以用來控制算法正確的概率，“翻轉文字li的值”是將文字li的變量值從0改為1，反之亦然。

Sch?ning算法只有在第1.2.1步得到可滿足賦值時才輸出YES。如果輸入實例F是不可滿足的，它將永遠不會輸出YES。設F是有n個變量的可滿足CNF公式，π*是滿足F的賦值集合。由于步驟1.1隨機選取了一個賦值集合π給F，可以期望π與π*在n／2個變量上一致。因此，對大約n／2個變量的賦值π進行“修正”，以獲得滿意的賦值集合π*。為了找出π中“不正確”的變量，步驟1.2.2選取π不滿足的子句C＝（l1∨l2∨l3）。如果F是可滿足的而π不滿足C，那么C中至少有一個文字在賦值π下得到一個錯誤的值，因此應該“翻轉”。為了決定要翻轉C中的哪個文字，步驟1.2.3隨機選取C中的一個文字。該算法的步驟1.2.2～1.2.3對賦值進行（隨機）局部搜索，可視為從隨機選擇的賦值π開始的隨機進行以達到滿意的賦值集合π*。與以前的算法相比，Sch?ning算法的一個不同之處是算法最多運行3n步（參見步驟1.2）。在3n步中，隨機進行沒有達到目標π*，那么通過步驟1.1用一個新的隨機選擇的分配重新開始局部搜索。

Sch?ning證明了在輸入F是可滿足的情況下，步驟1.1～1.2將在步驟1.2.1得到一個滿意的賦值，并輸出YES，概率至少為（3／4）n。步驟1.1～1.2在算法中重復b·（4／3）n次，實例F在步驟2中輸出NO（即在步驟1.2.1中不輸出YES）的概率有界于

式中，e＝2.718…是自然對數的常數，不等式（1－1／p）p≤1／e。由于Sch?ning算法在不可滿足的輸入上從不輸出YES，因此得出結論，Sch?ning算法在每個輸入上輸出正確答案的概率至少為1－1／eb，當b足夠大時，其值可以無限接近1。就時間復雜性而言，步驟1.1～1.2顯然需要時間O（L）。只要b以n的多項式為界，Sch?ning算法的運行時間為O*（b·（4／3）n）＝O*（1.334n）。

定理53-SAT問題在時間O*（1.334n）內可用隨機算法求解。

Sch?ning算法可推廣到一般的k-SAT問題，k-SAT（k≥3）問題給出了運行時間為O*（（2－2／k）n）的隨機算法。

Dantsin等［20］為k-SAT問題開發了確定性算法，可以看作是Sch?ning算法的去隨機化。本文使用覆蓋碼代替隨機初始賦值。3-SAT確定性算法運行時間在O*（1.481n）之內，當k≥4時，確定性算法運行時間在O*（（2－2／（k＋1））n）之內。

3-SAT和k-SAT隨機算法是近年來非常熱門和活躍的研究課題?？梢詤⒖嘉墨I［21－24］及相關文獻了解最新的研究狀況以及內容更新。3-SAT算法的運行時間上界O*（cn）已經取得了新的研究進展，從Sch?ning算法的c＝1.334，逐步改進為c＝1.324，1.323，1.322，1.321，…，1.308，1.307。目前，最佳上界c＝1.307是由Hansen等［24］取得的。k＞3的k-SAT也有進展，研究了這些隨機算法的去隨機化。

3-SAT算法運行時間的指數上界O*（cn）在不斷減小。不能期望c＝1，因為這意味著NP完全問題3-SAT在多項式時間內可解。那么3-SAT指數時間算法的c是否可以無限接近1？這與P≠NP并不矛盾。事實上有一些NP完全問題可以在時間O*（cn）內求解，其中，常數c＞1無限接近1［16］。從實際計算的角度來看這個問題也有意義。例如如果3-SAT問題能在時間O*（1.000 1n）內得到解決，該算法可用于多達100 000個變量的3-SAT實例，這可能滿足許多工程應用的需要。在精確算法的研究以及整個理論計算機科學中，指數時間猜想（Exponential Time Hypothesis，ETH）排除了這種可能性［25］。

3-SAT不能在時間O*（cn0）內求解，其中，常數c0＞1。

不確定猜想ETH中常數c0的值接近目前最好的上限1.307，還是可以更??？如1.000 1？這方面的研究具有意義。

如果問題在時間O*（2n／ɑ（n））內求解，則可以在次指數時間內求解，其中，ɑ（n）是n的一個遞增無界函數。能夠證明一個問題在次指數時間內求解［26］，當且僅當它可以在時間O*（cn）（c＞1）內求解。在指數時間算法的文獻中，ETH通常被描述為“3-SAT不能在次指數時間內求解”。

根據SETH猜想，對于任意常數c＜2，SAT問題不能在時間O*（cn）內求解?？梢钥闯?，SETH 包含ETH［16］。SETH的猜想比ETH的猜想強（ETH被認為更可信）。ETH是近年來證明計算復雜性下限的一個非常流行的猜想，同時，SETH在某種程度上被許多研究者視為一個可疑的猜想。

3 基于參數m的算法

在本節中用輸入CNF公式F中子句數量m來衡量SAT算法時間復雜度。m可以大到2n，也可以比n小得多，那么對有n個變量的3-SAT實例的CNF公式F，F中子句數量m的邊界為由于3-SAT是NP完全的，除非有P＝NP，否則不期望3-SAT算法（一般SAT問題的算法）的運行時間是m的多項式。

對于常數c＜2的一般SAT問題，用實例中的變量個數n來度量SAT算法的復雜度，與SETH猜想相比得到一個O*（cm）時間算法并不困難。

設F是一個CNF公式，l是F中的一個文字。如果文字l在F中正好出現ɑ次且其否定ˉl在F中正好出現b次，則稱l為（ɑ，b）－文字；如果文字l在F中至少出現ɑ＋次且其否定ˉl在F中正好出現b次，則稱l為（ɑ＋，b）－文字。同樣可以定義（ɑ，b＋）－文字和（ɑ＋，b＋）－文字。由于通過多項式時間的預處理，總可以使公式F明確，在下面的討論中，公式F中的每個文字都是（1＋，1＋）－文字。對于（ɑ，b）－文字l，CNF公式F可以寫為

其中，F0是CNF公式，Ci和C′j是既不包含l也不包含的子句。F在文字l上的消解為

如果公式F有m個子句，那么消解式DPl（F）最多可以有m＋ɑb－（ɑ＋b）個子句，（DPl（F）中的一個子句Ci∨C′j可能包含變量x和ˉx，那么可以刪除這種子句）。當ɑb≤ɑ＋b時，對（ɑ，b）－文字l的消解操作不會增加子句的數目。因此，可以直接對公式F應用消解，為了確保運算是安全的，還需要CNF公式的長度是可控的。由n個變量和m個子句組成的CNF公式，由于F中每個子句的長度不能大于n，公式的長度L以nm為界。由于消解運算減少了變量的數量，如果它不增加子句的數量，那么所得公式長度邊界為（n－1）m≤nm。如果對有n個變量、m個子句、長度為L的CNF公式F中ɑb≤ɑ＋b的（ɑ，b）－文字應用消解運算，那么在這個過程中得到所有公式的長度邊界為nm≤L2。這確保了消解運算可以在公式F長度內多項式時間完成。

上述分析表明，當公式中存在ɑb≤ɑ＋b的（ɑ，b）－文字時，對文字l進行消解運算減少了變量的個數，最多可以進行n次。經過多項式時間的預處理，得到了一個CNF公式F，其中，每個文字都是ɑb＞ɑ＋b的（ɑ，b）－文字，這意味著ɑ，b≥2且ɑ＋b≥5。對于任何這樣的（ɑ，b）－文字l，用F［l＝1］和F［l＝0］進行分支。ɑ，b≥2，ɑ＋b≥5，F［l＝1］和F［l＝0］都必須將子句的數目m至少減少2，并且其中至少有一個將子句的數目m至少減少3。如果將＃（m）設為該算法在m個子句的CNF公式上的搜索樹中的葉數，有如下遞推關系（由于ɑ＋b≥5，有m≥5）：

求解這個遞推關系＃（m）≤1.325m，得到下面的定理：

定理6SAT問題在時間O*（1.325m）內能求解，其中，m是輸入公式中的子句個數。

定理6給出的SAT算法時間復雜度的上界O*（1.325m）是通過（2，3）－文字的分支和搜索過程。如果想降低上界，需要更有效地處理（2，3）－文字。對一個SAT算法，它的時間復雜度不比遞推關系＃（m）≤2＃（m－3）給出的算法差，＃（m）≤1.260m。因此，在（3＋，3＋）－文字上進行分支。對ɑb≤ɑ＋b的（ɑ，b）－文字，可以在多項式時間內使用無分支的消解進行處理。為了達到定理6中的上界并實現一個O*（1.260m）時間的SAT算法，只需要更有效地處理（2，3）－文字和（2，4）－文字，不是簡單地在這些文字上進行分支。有一種通用技術可以更有效地處理所有b≥3的（2，b）－文字。將此技術介紹如下：

按照給定的順序，考慮重復應用以下步驟的過程：

過程－M

M1.使F明確；

M2.如果F有兩個子句C′和C″，滿足C′?C″，則從F中刪除C″；

M3.如果F有一個ɑb≤ɑ＋b的（ɑ，b）－文字l，則對l應用消解原理；

M4.如果F有一個（3＋，3＋）－文字，那么在該文字上進行分支。

過程－M的步驟M2顯然是準確的：如果賦值滿足子句C′，那么它肯定滿足C″。如上所述過程－M的步驟至少與（3，3）－文字上的分支同樣有用。通常如果過程－M的任何一個步驟都不能應用于F，那么CNF公式F是可簡化的。

因此，只需要查看簡化實例，它包含（2，3＋）－文字和（3＋，2）－文字?？紤]下面兩種情形：

情形1F中包含（2，3＋）－文字的每個子句也包含（3＋，2）－文字。

這種情況很容易通過以下推導證明：（A1）簡化實例F中的每個文字都是（2，3＋）－文字或（3＋，2）－文字；（A2）對于文字l，l和ˉl不可能同時都是（2，3＋）－文字。因此，可以直接將1賦給所有（3＋，2）－文字，然后（S1）如果一個子句只包含（3＋，2）－文字，則該子句可滿足；（S2）如果一個子句包含一個（2，3＋）－文字，根據情形的條件該子句還包含（3＋，2）－文字，因此該子句也滿足。在第一種情形下，公式F是可滿足的。

情形2F中有一個子句只包含（2，3＋）－文字。

可簡化公式F必須包含（2，3＋）－文字。如果情形1的條件不成立，那么F中必須有一個只包含（2，3＋）－文字的子句C。由于F是明確的（過程－M 的步驟M1），｜C｜≥2。不是C中所有文字都可以包含在F中的另一個子句中（因為過程－M的步驟M2）。因此，C中必須有兩個（2，3＋）－文字l1和l2，F中必須有另外兩個子句C1和C2使得l1∈C1，l2∈C2，C，C1和C2兩兩不同。在分支F［l1＝0］中，至少F中的3個子句是可滿足的（因為l1是（2，3＋）－文字）。另外，在分支F［l1＝1］中，子句C和C1是可滿足的，從公式中刪除?，F在l2只出現在C2子句中，變成F［l1＝1］中的一個（1，0＋）－文字，可以在l2上進行消解運算，將F［l1＝1］中的子句數至少減少1。通過分支F［l1＝1］，然后在l2上進行消解，子句的數量至少減少了3個。這表明，在F［l1＝1］中文字l1上的分支與l2上的消解相結合，至少與（3，3）－文字上的分支一樣好。算法4對上述討論進行了總結。

?

上述討論證明了SATm算法的正確性。特別通過對情形1的討論，在步驟3的條件下公式F必須是可滿足的。對情形2的討論確保了如果步驟3中的條件不成立，那么算法的步驟4總能找到所需的文字和子句。情形2所討論的步驟5中的實例F［l1＝0］和F1中的每一個都將子句的數目m至少減少3。因此，步驟5中的分支至少與（3，3）－文字上的分支一樣好。如果在m個子句的公式上，讓＃（m）為算法SATm的搜索樹中的葉子數，則所有分支規則至少與＃（m）≤2＃（m－3）一樣好，得出算法SATm的運行時間為O*（1.260m）。

定理7SAT問題能在時間O*（1.260m）內求解，其中，m是輸入公式中的子句數。

對SATm算法的討論提出了一個合理的方法來分析SAT問題的分支和搜索算法：復雜的分支步驟是算法效率的“瓶頸”（SATm算法是（2，3）－文字分支），總會導致一些特殊結構，能夠在這些結構上應用更有效的運算（SATm上是公式F［l1＝1］的消解）。通過將復雜的分支步驟與更高效的操作相結合，從而得到了更簡易的分支，這將突破“瓶頸”，得出更高效的算法。

SATm算法的瓶頸是（3，3）－文字的分支。在對瓶頸分支操作后公式結構更細致分析的基礎上，得到了一些改進的算法。Hirsch［27］開發了一種運行時間為O*（1.239m）的SAT算法，后來Yamamoto［28］用一種在時間O*（1.234m）中運行的算法對其進行了改進。Chu等［29］也報告了運行時間為O*（1.223m）的SAT算法。

從目前的研究現狀來看，用m來衡量SAT算法可以比用（3，3）－文字分支算法做得更好。下一個目標是（3，4）－文字。在（3，4）－文字上實現分支的效率將得到時間為O*（1.221m）的SAT算法。目前還未有符合這個上限的SAT算法。

4 基于參數L的算法

下面考慮用輸入實例長度L來衡量SAT算法時間復雜度。由于SAT問題是NP完全問題，不期望SAT算法的運行時間是L的多項式，要得到由參數L度量的SAT算法，可以觀察得到L≥m。任何運行時間為O*（cm）的SAT算法也是運行時間為O*（cL）的SAT算法。根據第3節討論的結果，易知SAT問題可以在時間O*（1.223L）內求解。

分支和搜索SAT算法通常使用參數L比使用參數m做得更好。對于子句C中的文字l，賦值l＝1使子句C滿足，從而將參數m減少1，將參數L減少｜C｜。當處理參數L時，用于參數m的一些方法變得無效。設公式F是明確的，沒有子句是F中另一個子句的子集（參見第3節過程－M的步驟M1和M2），過程－M的步驟M3不再滿足：即使在ɑb＜ɑ＋b的條件下，在（ɑ，b）－文字上的消解也可能增加公式的長度，（1，1）－文字上的消解不會增加公式長度?？紤]（1，2）－文字l，公式F可以寫成

如果｜C1｜≤3，則不難驗證消解不會增加公式長度。

當使用L作參數時，有以下過程：

過程－L

L1.F是明確的；

L2.如果F有兩個子句C′和C″，滿足C′?C″，則從F中刪除C″；

L3.如果F有一個（1，1）－文字l，或者有一個（1，2）－文字l，其中，l在一個大小不大于4的子句中，那么對l進行消解；

L4.選擇文字l和l上的分支。

步驟L1－L3是多項式時間的，沒有增加公式長度。只需要考慮步驟L4，假設步驟L1－L3都不適用于公式F，讓l是L4中F的文字。

如果l是（1，2）－文字，那么由于步驟L3中｜C1｜≥4，并且由L1易知｜C′1｜，｜C′2｜≥1。賦值l＝1將公式長度至少減少5＋1＋1＝7（也可以通過此賦值從公式中刪除ˉl），賦值l＝0會將公式長度至少減少1＋2＋2＝5。這樣分支至少和（5，7）－分支一樣好。

如果l是（1，3＋）－文字，那么F＝F0∧（l∨C1）∧（CNF公式F0可能仍然包含文字）。步驟L3不適用于l，｜C1｜可以小到1。賦值l＝1將公式長度至少減少2＋1＋1＋1＝5，賦值l＝0將公式長度至少減少1＋2＋2＋2＝7。同樣，至少和（5，7）－分支一樣好。

如果l是（2＋，2＋）－文字，那么使用與上述類似的分析可以得出分支至少與（6，6）－分支一樣好。

（5，7）－分支的分支多項式為xL－xL－5－xL－7，其最大根為x＝1.123…，（6，6）－分支的分支多項式為xL－2xL－6，其最大根為x＝1.122…。通過定理3，得出定理8。

定理8SAT問題能在時間O*（1.124L）內求解，其中，L是輸入公式的長度。

同樣地，通過更仔細地檢查復雜分支操作的公式結構，識別更多不需要分支就可以處理的情況，定理8中給出的上界可以得到改進。進展包括Gelder［30］提出的運行時間為O*（1.093L）的SAT算法，Hirsch［27］提出的進一步改進的時間上界O*（1.074L），以及Wahlstr?m［31］提出的運行時間為O*（1.067L）的新的SAT算法。

Chen等［32］提出了一種基于度量與控制方法的新算法，這是一種用于分析一般NP難問題的分支與搜索算法新技術［33］。將CNF公式F中變量x的度數deg（x）定義為文字x和xˉ在F中出現的次數。在更大程度的變量上進行分支，會使公式長度減少得更明顯，處理效率更高。對一個變量進行分支會改變其他變量的度數，這可能會影響實例的后續處理。

可以根據變量度數來分配不同權重的變量。分支搜索算法不僅考慮了公式長度的減少，而且還考慮了公式中變量度數的變化。

形式上wi是分配給度數為i的變量的權重（i≥0）。將CNF公式F的加權長度L′（F）定義為L′（F）＝其中，ni是F中度數為i的變量的個數。Chen等［32］選擇了以下可變權重：

w1＝0.32，w2＝0.45，w3＝0.997，w4＝1.897，當i≥5時，wi＝i／2，0.32·L（F）≤L′（F）≤L（F）。分支和搜索過程嘗試對導致權值長度L′最大減少的變量進行分支。

從正則公式長度L到加權公式長度L′的轉換并非沒有意義。多項式時間預處理中使用的許多技巧不再有效，它們可能會增加加權公式長度。在運算之后檢查結果公式的加權長度也更加復雜，因為還需要考慮運算中涉及的變量度數。Chen等［32］提出了一種基于加權公式長度的分支搜索SAT算法，并且能夠證明該算法運行時間為O*（1.134 5L′）。由于L′≤L／2，因此，給出了一個運行時間為O*（1.065L）的算法，該算法是目前基于參數L最快的SAT算法。

5 結 論

本文介紹SAT問題最前沿的精確算法，SAT問題是計算機科學研究的核心，在自然科學、社會科學、醫學、工程和商業等許多領域都有應用。本文的方法遵循了算法發展和計算復雜性理論中的主流，基于最壞情況對算法的性能進行了定量分析。在這一研究領域，仍有許多有趣而重要的未解問題。

第一個基本的方向是用參數n、m和L開發更快的SAT算法。文獻中大多數已知算法都在很大程度上基于兩種基本技術：消解和分支搜索。消解是一種有效的操作，可以減少變量的數量，缺點是它可能會增加公式的長度。這可能是困難的，而且需要繁瑣的個案分析以了解公式通過特定變量消解而實際影響的長度。事實上大多數算法在很多情況下都不應用消解，這僅僅是因為檢查所有可能的情況來驗證解析操作的效率變得過于繁瑣。另一方面分支和搜索是一個復雜的操作，這是使算法指數時間運行的來源，基于最壞情況分析考慮了應用分支和搜索最壞可能的公式結構，并且在很大程度上忽略了復雜的分支和搜索操作次數以及應用這些操作后的結果。開發SAT算法的經驗表明分支和搜索操作可能會產生一些非常受歡迎的公式結構，在這些結構上可以應用更有效的操作，然而同樣不好的是這些公式結構研究困難，而且這種方法很難避免繁瑣的逐個檢查。許多逐步改進的SAT算法在很大程度上是基于識別更多公式結構的技術，在這些公式結構上可以應用有效的運算。研究復雜的分支和搜索產生的可以更有效處理的公式結構能夠“平衡”分支和搜索操作所導致的高計算復雜性。進一步的研究僅能取得小的改進，想要獲得突破還需要新的技術、算法和分析。

在第2節中所討論的Sch?ning的3-SAT問題隨機算法是為SAT問題開發的新算法技術，不使用消解也不使用分支和搜索。它從一個精心選擇的初始賦值開始（在隨機版本中，它是一個隨機選擇的賦值，而在其去隨機化版本［20］中，賦值是由精心設計的“覆蓋碼”構成的，覆蓋了一些Hamming半徑的球的所有可能賦值）。在初始分配之后，該算法使用局部搜索來“糾正”初始分配中的錯誤位。這種方法還是很自然的，不便之處在于分析該算法的有效性。

第4節中描述的度量和控制方法是SAT算法的新分析技術。該方法對變量賦予不同的權值，使得不同變量的分支和搜索操作的計算開銷得到評估。通過計算分支和搜索操作的權重，用高效的操作“平衡”分支和搜索的高計算復雜性，從而使算法總的復雜度變得更好。

這些新的算法和分析技術仍處于非常初級的階段，前景很好，對發現更快的SAT算法具有重要作用。

對SAT問題的計算上限也需要更新、更深入的研究。人們希望有更有力的證據來支持ETH和SETH假說，假說失敗的可能性并沒有被完全排除。許多與ETH和SETH有關或類似問題的答案都是未知的。例如如果使用參數L來測量SAT算法，SAT算法是否可能在時間O*（2o（L））內運行，這是以L表示的次指數時間，這并非完全不可能，用L度量的當前最佳SAT算法運行時間為O*（1.065L），1.065已經非常接近1（SAT問題可以在時間O*（2o（L））內解決當且僅當它可以在時間O*（cL）（c＞1）內解決）。此外，SAT問題的O*（2o（L））時間算法與SAT問題的NP完備性并不矛盾。有許多已知的NP完全問題（如平面圖上的NP完全圖問題）可以在其輸入長度上以次時間指數求解。

除了基于最壞情況計算復雜性分析的SAT問題精確算法的研究外，SAT問題啟發式算法的發展歷史悠久，是計算機科學與工程領域一個非?；钴S和熱門的研究領域。啟發式算法以實例結構中的直覺和實踐經驗為基礎，試圖有效地解決SAT問題。在某些情況下啟發式算法可能無法正確地解決問題（如在YES實例中可能輸出NO），而且可能無法保證某些輸入實例的計算效率。一些SAT算法被稱為“啟發式”算法，即使它們能夠在所有輸入實例上正確有效地解決SAT問題，但是不能為這些性能提供正式的證明。許多文獻中發表的啟發式算法在大多數SAT實例上運行良好，并在實際中得到了成功的應用。關于SAT問題啟發式算法的更多細節可參閱文獻［34］。

這些求解SAT問題的啟發式算法在文獻中被稱為SAT求解器。在本文中詳細討論的兩種基本技術消解和分支與搜索一直是SAT求解器開發中的主要工具。盡管在最壞的情況下，所有已知的SAT算法的運行時間復雜度都具有很強的指數因子，但現代SAT求解器能夠求解涉及數萬個變量和數百萬個子句的SAT實例［35］。某種程度上快速SAT求解器的存在與基于最壞情況分析的SAT算法時間復雜度的最佳理論上界相矛盾，這表明該研究領域的理論研究與實際實現之間存在著巨大的差距。顯然為了更好地求解SAT問題和更準確地分析SAT算法，還需要新的技術和更深入的研究。