可滿足性問題的精確算法和計(jì)算復(fù)雜性

陳建二，楊 偉

（廣州大學(xué)計(jì)算機(jī)科學(xué)與網(wǎng)絡(luò)工程學(xué)院，廣東 廣州 510006）

可滿足性問題是計(jì)算機(jī)科學(xué)中最重要且十分著名的問題之一。在理論計(jì)算機(jī)科學(xué)的研究中，可滿足性問題是第一個(gè)NP（Non-deterministic Polynomial，NP）完全問題［1］，在計(jì)算困難問題的研究中起著重要作用［2］。實(shí)踐中可滿足性問題是解決很多應(yīng)用領(lǐng)域問題的基礎(chǔ)，包括人工智能［3］、模型檢查［4］、自動(dòng)推理［5］、計(jì)算機(jī)輔助設(shè)計(jì)［6］、數(shù)據(jù)庫(kù)［7］、機(jī)器人學(xué)［8］、調(diào)度［9］、電路設(shè)計(jì)［10］、計(jì)算機(jī)體系結(jié)構(gòu)設(shè)計(jì)［11］和計(jì)算機(jī)網(wǎng)絡(luò)［12］等。

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

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

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

SAT是NP完全問題，除非有P＝NP，否則SAT問題在多項(xiàng)式時(shí)間內(nèi)不能有效求解，P＝NP在計(jì)算機(jī)科學(xué)和數(shù)學(xué)領(lǐng)域共識(shí)中是不成立的。

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

1 基礎(chǔ)概念和相關(guān)技術(shù)

設(shè)CNF公式F＝C1∧C2∧…∧Cm為SAT問題的一個(gè)實(shí)例，Cm表示子句。以下情況可以進(jìn)行預(yù)處理：

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

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

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

（4）如果一個(gè)子句Ci同時(shí)包含一個(gè)變量x和它的否定，那么Ci總是可滿足的。可以忽略子句Ci（不需要確定x的值）。

編寫一個(gè)簡(jiǎn)單的算法可以處理上述情況。預(yù)處理完成之后，CNF公式就是明確的。下面的研究放在明確的SAT問題實(shí)例上。

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

1.1 消解

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

其中，F(xiàn)0是子句既不包含x也不包含的CNF公式。那么F在變量x上的消解式為

下面給出定理，并對(duì)完整性進(jìn)行證明。

定理1（消解原理） 設(shè)x是一個(gè)確定的CNF公式F中的任意變量，F(xiàn)是可滿足的當(dāng)且僅當(dāng)DPx（F）是可滿足的。

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

假設(shè)F是可滿足的。π是F的一個(gè)可滿足賦值集合，π（x）＝x*，π（xk）＝（2≤k≤n），其中，x*和是布爾常數(shù)。設(shè)π′為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）是可滿足的。

另一方面，假設(shè)DPx（F）是可滿足的，π′是可滿足DPx（F）的變量｛x2，…，xn｝上的賦值集合。如果π′（Ci）＝1（1≤i≤s），那么除了π′之外，指定x＝0，則ˉx＝1，賦值滿足F中的所有子句；如果對(duì)于某些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就是可滿足的。證明完成。

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

1.2 分支搜索

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

?

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

將n個(gè)變量上輸入實(shí)例F的SAT-Alg（F）時(shí)間復(fù)雜度記為T（n）。F0和F1最多都有n－1個(gè)變量，有以下遞推關(guān)系，其中，L（F）是輸入實(shí)例F的長(zhǎng)度：

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

定理2SAT-Alg在O（2nL）時(shí)間內(nèi)解決有n個(gè)變量、長(zhǎng)度為L(zhǎng)的SAT實(shí)例F。

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

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

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

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

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

根據(jù)給定的實(shí)例結(jié)構(gòu)，上述討論可以很容易地推廣到使用多個(gè)分支規(guī)則的SAT算法，定理如下：

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

2 基于參數(shù)n的算法

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

SAT問題不能在O*（cn）（c＜2，c為任意常數(shù)）時(shí)間內(nèi)求解。

在最近的研究中，SETH被廣泛用于著名的計(jì)算優(yōu)化問題開發(fā)計(jì)算下限（如文獻(xiàn)［16］的14.5節(jié)）。在SAT算法和復(fù)雜性研究中，任何一種算法如優(yōu)于基本SAT算法都是一個(gè)重大的進(jìn)步，也將是許多其他優(yōu)化問題算法研究的一個(gè)重要進(jìn)展。

如果使用參數(shù)n來度量算法的復(fù)雜度，那么SETH為更優(yōu)的算法開發(fā)留下了很少的空間。SAT算法的研究熱點(diǎn)已經(jīng)發(fā)展到具有各種限制條件的算法研究上。

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

當(dāng)k＝2，3時(shí)，k-SAT問題特別有趣。2-SAT問題在多項(xiàng)式時(shí)間內(nèi)是可解的，屬于P類［17］。3-SAT問題是一個(gè)非常著名的NP完全問題，它在NP完全性理論、SAT算法和計(jì)算復(fù)雜性的研究中起著關(guān)鍵的作用。接下來重點(diǎn)討論3-SAT問題的算法，討論如何將這些算法推廣到一般k-SAT問題。

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

?

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

3SATms算法中為了滿足公式F，必須滿足子句（l1∨l2∨l3），滿足F的賦值必須將值1賦值給3個(gè)文字l1、l2和l3中的至少一個(gè)。總共有7組對(duì)文字l1、l2和l3的賦值可以滿足子句（l1∨l2∨l3）（僅排除賦值l1＝l2＝l3＝0），F(xiàn)1中的賦值l1＝1涵蓋了這7組賦值中的4個(gè)（l1＝1，l2和l3是0或1），函數(shù)F01中的賦值l1＝0，l2＝1涵蓋了7組賦值中的兩個(gè)（l3是0或1），該算法步驟3中的3個(gè)賦值覆蓋了對(duì)文字l1、l2、l3的所有可能賦值，它們可以對(duì)輸入實(shí)例F進(jìn)行可滿足賦值。這證明了該算法的正確性，即當(dāng)且僅當(dāng)F1、F01、F001中至少有一個(gè)可滿足，輸入實(shí)例F才是可滿足的。

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

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

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

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

?

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

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

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

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

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

定理53-SAT問題在時(shí)間O*（1.334n）內(nèi)可用隨機(jī)算法求解。

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

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

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

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

3-SAT不能在時(shí)間O*（cn0）內(nèi)求解，其中，常數(shù)c0＞1。

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

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

根據(jù)SETH猜想，對(duì)于任意常數(shù)c＜2，SAT問題不能在時(shí)間O*（cn）內(nèi)求解。可以看出，SETH 包含ETH［16］。SETH的猜想比ETH的猜想強(qiáng)（ETH被認(rèn)為更可信）。ETH是近年來證明計(jì)算復(fù)雜性下限的一個(gè)非常流行的猜想，同時(shí)，SETH在某種程度上被許多研究者視為一個(gè)可疑的猜想。

3 基于參數(shù)m的算法

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

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

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

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

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

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

求解這個(gè)遞推關(guān)系＃（m）≤1.325m，得到下面的定理：

定理6SAT問題在時(shí)間O*（1.325m）內(nèi)能求解，其中，m是輸入公式中的子句個(gè)數(shù)。

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

按照給定的順序，考慮重復(fù)應(yīng)用以下步驟的過程：

過程－M

M1.使F明確；

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

M3.如果F有一個(gè)ɑb≤ɑ＋b的（ɑ，b）－文字l，則對(duì)l應(yīng)用消解原理；

M4.如果F有一個(gè)（3＋，3＋）－文字，那么在該文字上進(jìn)行分支。

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

因此，只需要查看簡(jiǎn)化實(shí)例，它包含（2，3＋）－文字和（3＋，2）－文字。考慮下面兩種情形：

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

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

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

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

?

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

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

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

SATm算法的瓶頸是（3，3）－文字的分支。在對(duì)瓶頸分支操作后公式結(jié)構(gòu)更細(xì)致分析的基礎(chǔ)上，得到了一些改進(jìn)的算法。Hirsch［27］開發(fā)了一種運(yùn)行時(shí)間為O*（1.239m）的SAT算法，后來Yamamoto［28］用一種在時(shí)間O*（1.234m）中運(yùn)行的算法對(duì)其進(jìn)行了改進(jìn)。Chu等［29］也報(bào)告了運(yùn)行時(shí)間為O*（1.223m）的SAT算法。

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

4 基于參數(shù)L的算法

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

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

如果｜C1｜≤3，則不難驗(yàn)證消解不會(huì)增加公式長(zhǎng)度。

當(dāng)使用L作參數(shù)時(shí)，有以下過程：

過程－L

L1.F是明確的；

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

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

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

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

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

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

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

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

定理8SAT問題能在時(shí)間O*（1.124L）內(nèi)求解，其中，L是輸入公式的長(zhǎng)度。

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

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

可以根據(jù)變量度數(shù)來分配不同權(quán)重的變量。分支搜索算法不僅考慮了公式長(zhǎng)度的減少，而且還考慮了公式中變量度數(shù)的變化。

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

w1＝0.32，w2＝0.45，w3＝0.997，w4＝1.897，當(dāng)i≥5時(shí)，wi＝i／2，0.32·L（F）≤L′（F）≤L（F）。分支和搜索過程嘗試對(duì)導(dǎo)致權(quán)值長(zhǎng)度L′最大減少的變量進(jìn)行分支。

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

5 結(jié) 論

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

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

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

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

這些新的算法和分析技術(shù)仍處于非常初級(jí)的階段，前景很好，對(duì)發(fā)現(xiàn)更快的SAT算法具有重要作用。

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

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

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