可满足性问题的精确算法和计算复杂性

陈建二，杨 伟

（广州大学计算机科学与网络工程学院，广东 广州 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］。可满足性问题定义如下：

可满足性（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总是可满足的。可以忽略子句Ci（不需要确定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的大小｜Ci｜是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中的至少一个。总共有7组对文字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随机算法是近年来非常热门和活跃的研究课题。可以参考文献［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是可满足的，从公式中删除。现在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问题启发式算法的发展历史悠久，是计算机科学与工程领域一个非常活跃和热门的研究领域。启发式算法以实例结构中的直觉和实践经验为基础，试图有效地解决SAT问题。在某些情况下启发式算法可能无法正确地解决问题（如在YES实例中可能输出NO），而且可能无法保证某些输入实例的计算效率。一些SAT算法被称为“启发式”算法，即使它们能够在所有输入实例上正确有效地解决SAT问题，但是不能为这些性能提供正式的证明。许多文献中发表的启发式算法在大多数SAT实例上运行良好，并在实际中得到了成功的应用。关于SAT问题启发式算法的更多细节可参阅文献［34］。

这些求解SAT问题的启发式算法在文献中被称为SAT求解器。在本文中详细讨论的两种基本技术消解和分支与搜索一直是SAT求解器开发中的主要工具。尽管在最坏的情况下，所有已知的SAT算法的运行时间复杂度都具有很强的指数因子，但现代SAT求解器能够求解涉及数万个变量和数百万个子句的SAT实例［35］。某种程度上快速SAT求解器的存在与基于最坏情况分析的SAT算法时间复杂度的最佳理论上界相矛盾，这表明该研究领域的理论研究与实际实现之间存在着巨大的差距。显然为了更好地求解SAT问题和更准确地分析SAT算法，还需要新的技术和更深入的研究。