第7卷第6期 智能系统学报 Vol.7 No.6 2012年12月 CAAI Transactions on Intelligent Systems Dec.2012 D0I:10.3969/i.i8sn.1673-4785.201206010 网络出版t地址：htp://www.cnki.net/kcma/detail/23.1538.TP.20121116.1701.009.html 基于分支回溯的NAE-3SAT问题求解算法 谷文祥12，傅琳璐，周俊萍1，姜蕴晖 (1.东北师范大学计算机科学与信息技术学院，吉林长春130117；2.长春楚筑学院基础教学部，吉林长春130607) 摘要：NAESAT问题是可满足性问题的一个重要扩展，在集合分裂、最大割集等NP完全问题中有着重要的应用. 针对NAESAT问题的泛化NAE-3SAT问题，提出了一个基于分支回溯的精确算法NAE.算法给出了多种化简规则， 这些化简规则很好地提高了算法的时间效率.最后证明了算法在最坏情况下的时间复杂度上界为O(1.618),其中 n为公式中的变量数目. 关键词：NAESAT;NAE-3SAT;时间复杂性：NAE-3SAT问题上界：变量数目：分支回溯 中图分类号：TP301文献标志码：A文章编号：16734785(2012)06050606 Solution algorithm for the NAE-3SAT problem based on DPLL GU Wenxiang'2,FU Linlu',ZHOU Junping',JIANG Yunhui (1.School of Computer Science and Information Technology,Northeast Normal University,Changchun 130117,China;2.Department of Basic Subjects Teaching,Changchun Architecture Civil Engineering College,Changchun 130607,China) Abstract:The not-all-equal satisfiability (NAESAT)problem is an important extension of the satisfiability (SAT) problem.It has an important application in many NP-complete problems,such as the SET SPLITTING problem and the MAXCUT problem.An exact algorithm NAE based on Davis-Putnam-Logemann-Loveland (DPLL)for the not- all-equal 3-satisfiability (NAE-3SAT)problem is proposed.In the algorithm some new reduction rules are used to simplify the formula.The reduction rules increase the efficiency of the algorithm.The worst-case upper bound for the algorithm is proved to be 0(1.618"),where n is the number of variables in the formula. Keywords:not-all-equal satisfiability;not-all-equal 3-satisfiability;time complexity;upper bounds for Not-All-E- qual 3-satisfiability;number of variables;DPLL 可满足性问题(satisfiability,SAT)作为计算机 算法在效率上获得指数级别的提高.多年来，研究人 理论与应用的核心问题，在智能规划、机器视觉、逻 员不断改进SAT问题及其约束子问题的求解算法 辑推理机以及电子设计自动化等领域中有着重要的 在最坏情况下的时间复杂度上界6】.以3SAT问题 理论研究与实际应用价值141.SAT问题的计算复杂 为例，最初Monien和Speckenmeyer在文献[6]中给 性是NP完全的]，这意味着如果P≠NP成立，则无 出了求解3SAT问题的上界为O(23),其中m是命 法在多项式时间内解决SAT问题.这时从理论上分 题公式中的子句数目，目前获得的最好上界为 析该问题在最坏情况下的时间复杂性上界尤为重 0(1.234)8].SAT问题理论上的不断发展使得其 要，因为此时对该问题上界的一个微小的改进，例如 系统的求解能力有了很大的提高.目前Zchaff、Sur- 从O(c)改进为O((c-ε))就会使得问题求解的 vey Propagation等SAT求解系统已可以求解包含 100000个以上变量的SAT问题实例24) 收稿日期：2012-0608.网络出版日期：2012-11-16. NAESAT（not-all-equal satisfiability)问题作为 基金项目：国家自然科学基金资助项目(61070084,60803102)：中央 高校基本科研业务费专项资金资助项目(11QNJJ006):浙 SAT问题的一个重要扩展，判断是否存在一组真值 江师范大学计算机软件与理论省级重中之重学科开放基 赋值使得给定的命题公式为可满足，并且使公式的 金资助项目(ZSDZZZZXK37). 通信作者：傅琳路.E-mail:fl820@nenu.ed.cm. 每个子句中所有文字的取值不全为真.NAESAT和
第6期 谷文祥，等：基于分支回溯的NAE-3SAT问题求解算法 ·507· NAEk-SAT(即公式中所有子句的长度都小于等于 定义4子句.子句由一组文字的析取而成，如 k,k≥3)都是NP完全问题517]，其在集合分裂、最 C=lVL2V…Vl.当且仅当C中至少有一个文字 大割集等问题中都有着重要的应用16].近来，从理 取值为tue,子句C在赋值μ下为可满足.子句的长 论上研究NAESAT问题及其约束子问题在最坏情 度是指子句中文字的个数，用符号|C|表示.把长度 况下的时间复杂度上界受到了广泛的关注.Monien 为k的子句称为k-子句，长度为0的子句称为空子 等提出NAESAT问题可在O(1.587)时间内求解， 句，用empty表示.空子句为不可满足 其中m为公式中的子句数目Iu81.Riege等将NAE 定义5合取范式.合取范式(conjunctive nor- SAT问题算法在最坏情况下的时间复杂度上界改进 mal form,CNF)由一组子句的合取而成，如F=C,∧ 为0(1.5228“)[9.2010年，Shi等则运用生物学 C2∧…∧C.CNF范式也称为公式F.当且仅当F 方法提出了一种基于DNA的NAE-3SAT求解算 中每一个子句都为可满足，公式F在赋值4下为可 法120 满足，空公式为可满足. 事实上，算法的时间复杂度是根据问题实例的 定义6 NAESAT问题.NAESAT问题对于一 大小计算所得.而对于涉及命题公式的问题，问题实 个给定的命题公式F,判断是否存在一组赋值使得 例的大小不仅依赖于公式中子句的数目，还依赖于 公式F为可满足并且使公式F的每个子句中所有 变量的数目.以变量数目为参数研究NAESAT问题 文字的取值不全为真，即要求公式F的每个子句中 及其约束子问题在最坏情况下的时间复杂度上界， 至少有一个文字为真，至少有一个文字为假.如果存 不仅可以从另一个角度衡量算法的好坏，而且在某 在这样的一组赋值，则称公式F为NAE-可满足的，否 种程度上更能准确地反映出算法的性能.本文正是 则称公式F为NAE-不可满足.使得公式F为NAE可 以此为着眼点，从变量数目的角度探讨NAE-3SAT 满足的赋值称为该公式的NAE-可满足赋值， 问题在最坏情况下的时间复杂度上界，提出了一个 如果给定的命题公式F中所有子句长度都小 基于分支回溯(DPLL)的精确算法NAE.该算法给 于等于3，则判断是否存在一组赋值使得公式F为 出了多种化简规则，证明该算法在最环情况下的时 可满足并且使公式F的每个子句中所有文字的取 间复杂度上界为0(1.618")，其中n为公式中的变 值不全为真的问题称为NAE-3SAT问题， 量数目 另外需要说明的是，在文中符号F[x/false]表 1基本概念 示将公式F中的x赋值为false,相应地一x赋值为 true后得到的子公式；符号F[x/y]表示替换x三 文中符号x,y,z…表示布尔变量；符号1,1，l2 y,即将公式F中的x用y替换，x用y替换后 表示文字.符号C,C1,C2…表示子句.符号F,F,F2 得到的子公式；符号F[y,/y]则表示替换z=y …表示CNF公式， 和t=y,即同时将公式F中的z用y替换，t用y 定义1布尔变量.布尔变量（简称变量）取值 替换，并相应地将z用y替换，t用y替换后得 为{tue,false}.布尔变量x的度p(x)为变量x在 到的子公式 公式中出现的次数.把在公式中只出现一次的变量 2算法NAE 称为singleton. 定义2真值赋值.设变量集合X={x1,2, 2.1化简规则 “,xn},定义在变量集合X上的真值赋值是一个函 在求解NAE-3SAT问题时，使用化简规则对公 数u:X→{tue,false}.在变量集合X上存在2”组 式进行约简.应用化简规则的目的是减少公式中的 不同的真值赋值.文中把真值赋值简称为赋值， 变量数目，缩小搜索空间，提高算法的效率。 定义3文字.设x是一个变量，则称x和x 规则1：若公式F中存在1-子句，则进行如下 为文字，其中称x是正文字，x是负文字.当且仅 化简： 当变量x赋值为tnue,正文字x在赋值u下取真值； x∧F,→empty A F. 当且仅当变量x赋值为false,文字x在赋值μ下 规则2：若公式F中存在2个相同的子句，则进 取真值；当且仅当F中恰好包含i个文字l,文字L 行如下化简： 称为文字；当且仅当公式F中恰好包含i个文字1 C1ACAF1→C∧F 和j个文字1，文字1称为(i,)-文字公式中已经被 规则3：若公式F中存在包含重复变量的子句， 赋值为true(false)的文字称为true(false)文字， 则进行如下化简：
·508· 智能系统学报 第7卷 1)(xVx)ΛF1→empty AF1; 个规则的条件满足，该规则就可被执行，且所有规则 2)(xVx)∧F→F1; 按照顺序依次执行，即后面的规则只有在前面的规 3)(xVxVx)AF-empty AF1; 则都不适用时才会被执行.待处理的公式F重复地 4)(xVxV-x)AF,→F1; 被以上8条规则化简，直到所有规则的条件都不满 5)(xVxVy)∧F,→f1; 足为止 6)(xVxVy)AF→F[y/x]; 定理1以上8条化简规则都是正确的，不会 7)(true VxVa)∧F,→F,[x/false]; 影响算法对公式F的NAE-可满足性的判断！ 8)(false VxVx)∧F1→f,[x/tue]; 证明由NAE-3SAT问题的定义可得规则1~ 9)(true VxVx)∧F,→F; 5是正确的.在化简过程中，把NAE-可满足的子句 10)(false VxVx)∧F,→F. 直接从公式中消去，把NAE-不可满足的子句赋为空 规则4：若公式F中存在2-子句，则进行如下 子句，即empty. 化简： 规则6化简包含一个true或false文字和in- l)(false Vfalse)∧F,+empty∧Fi; gleton的子句，因为对singleton的赋值不影响公式 2)(true Vtrue)AF-empty AF; 中其他变量的取值，可直接把singleton赋值为false 3)(false Vtrue)∧F,→F1; (规则6中1))或ue(规则6中2))使子句为NAE- 4)(false Vx)∧F,→f,[x/true]; 可满足.因此可直接把该子句从公式中消去.规则7 5)(trueVx)AF-F[x/false] 与规则6类似. 6)(xVy)AF→F[y/x]. 在规则8的1)中，假设公式F包含2个子句为 规则5：若公式F中存在包含2个或以上ue （xVyVz)和(xVyV-z),如果y=x=tue或y= 或false文字的3-子句，则进行如下化简： x=false,则2个子句中肯定有一个是NAE-不可满 1)(false V false V false)AF,→empty∧F,; 足，所以必须使y=x;规则8中2)与规则8中1) 2)(true V true Vtrue)AFI-emptyA F; 类似；规则8中3)，2个子句的文字皆为互补，由 3)(false Vtrue V false)∧F,→F; NAE-3SAT问题的定义可得若存在一组赋值使得其 4)(false Vtrue Vtrue)AF-F1; 中一个子句为NAE-可满足，则该赋值肯定也能使另 5)(true Vtrue Vx)AFF[x/false ] 一个子句为NAE-可满足，所以可消去其中一个子 6)(false V false Vx)∧F,→f,[x/ue]; 句.因此规则8是正确的. 7)(false Vtrue Vx)∧F,→F. 综上所述，8条化简规则都是正确的，化简过程 规则6：若公式F中存在包含1个true或false 不影响公式的可满足性，即若化简后的公式F'∈ 文字和singleton的3-子句，则进行如下化简： NAE-3SAT,则可判定原公式F∈NAE-3SAT. 1)(true VxVy)AF1→F:; 化简后公式中将不存在1-子句、2-子句、包含重 2)(false VxVy)AF,→F. 复变量的子句、包含2个或以上tue或false文字的 其中x或y为singleton或者x、y是singleton. 3-子句、包含1个true或false文字和singleton的3- 规则7：若公式F中存在包含2个或以上的 子句、包含2个或以上的singleton的3-子句，且不会 singleton的3-子句，则进行如下化简： 存在2个包含3个相同变量的3-子句. (xVyV)AF→F 2.2NAE算法框架 其中x、y、z或者x、y是singleton. 算法NAE的基本思想是给定任意的3-CNF公 规则8：若公式F中存在2个子句，它们包含的 式F,首先利用2.1节中的化简规则对公式进行简 变量都相同，则进行如下化简： 化；然后在化简后的公式中选取某些变量进行分支， 1)(x Vy V a)∧(x V yV 7z)∧F,→ 分别判断各个分支的NAE-可满足性，进而判断出原 F[y/x]; 公式的NAE-可满足性；递归地执行这个过程直到公 2)(x V y V z)∧(x VyVz)∧F1→ 式为空或者判定公式为NAE-不可满足后停止· F [y/]; 算法的输入是一个待处理的3-CNF公式F,输 3)(xVyVa)∧(xV-yV-)∧F,→(xV 出为true或者false,true表示公式F为NAE-可满 yVz)AF. 足，false表示公式F为NAE-不可满足.下面给出了 化简规则的执行时间均为多项式时间.一旦某 算法的基本框架
第6期 谷文祥，等：基于分支回溯的NAE-3SAT问题求解算法 ·509· 算法NAE(F) 都进行分支，分别判断2个子公式F[x/y]和F[x/ 输入：A formula F in3-CNF y]的NAE-可满足性；第8步：若以上情况都不存 输出：If F is NAE-satisfiable,return true; 在，则公式中的任意2个子句间至多包含一个相同 Else,return false. 变量，算法任意选择公式中的一个子句进行分支，分 1)Apply the rule 1~8 to F as long as one of them 别判断2个子公式F[x/y]和F[x/y]的NAE-可 is applicable. 满足性。 2)If F is empty,return true. 综上所述，算法NAE是正确并且完备的，能正确 3)If F contains an empty clause,return false. 判断一个给定的3-CNF公式是否为NAE-可满足 4)If F contains a clause with one true or false lit- eral,C =trueVxVy or C =false VxVy,then return 3算法NAE时间复杂性分析 (NAE F[x/y])VNAE(F[x/y])). 在本节中，用分支树的方法来分析算法NAE的 5)If F contains two clauses C=(xVyVz), 时间复杂性，并证明了其在最坏情况下的时间复杂 C2=(xVyVt),then retur (NAE(F[x/y])VNAE 度上界为0(1.618")，其中n为公式中的变量数目. (F[x/y]). 首先给出分支树的概念 6)If F contains two clauses C=(xVyVz)and 分支树是一个由(i>0)个结点组成的集合T, C2 =(xVyVt),then return (NAE(F[x/y])V 是一棵层级结构树[12].分支树的每个结点标记一 NAE (F[x/-y])). 个CNF公式，其中一个特定的结点为根结点，标记 7)If F contains two clauses C=(xVyVz)and 为公式F,除根结点外的其他结点被划分为j≥0) C2=(xVyVt),return NAE(F[x/y])VNAE 个互不相交的有限集合T,T2,…,T,每一个集合 (F[x/y])). 又都是分支树，称为根的子分支树，分别标记为公式 8)Else choose a clause C=(xVyVz),return F1,F2,…,F公式F,F2,…,F是对公式F中的 (NAE(F[x/y])VNAE(F[x/y])) 某些变量进行赋值后得到的公式，为公式F的子公 9)End. 式.分支树的叶子结点标记的是空公式或者包含空 定理2算法NAE能正确地判断一个3-CNF 子句的公式 公式是否为NAE-可满足. 分支树中的每一个结点都有一个分支向量.设 证明下面的证明过程将对算法的每一行进行 分支树中某一个结点是F。,它的子结点分别是F, 分析. F2,…,F,则结点F。的分支向量为T(1,2,…, 算法首先对公式F进行化简（第1步），当所有 re),其中T:=f(F)-f(F),f(F:)(0≤i≤k)是公 化简规则都不可用时，进行判断：因为在化简过程中 式F,中变量的数目.每个结点所对应的分支向量的 将NAE-可满足的子句直接从公式中消去，所以若化 值称为该结点的分支数，可用式(1)计算： 简后的公式F为空，则说明公式为NAE-可满足，返 ∑x1=1,x>0. (1) 回true(第2步)；因为在化简过程中将NAE-不可满 足的子句赋为空子句，所以若化简后公式F包含空子 所有结点分支数中最大的被定义为分支树的分 句，则说明公式为NAE-不可满足，返回flse(第3步). 支数，用符号Tma表示 若化简后的公式F既不为空也不包含空子句， 定理3)设分支树T的根结点标记为公式 则算法进入分支过程（第4~9步）.分支过程根据 F,则分支树T中叶子的个数不超过(r)”,n是公 化简后的公式分几种情况进行：第4行：考虑公式中 式F中变量的数目. 存在true或false文字的情况.由定理1可知包含该 因为分支树的构造过程相当于基于分支回溯算 文字的子句一定为C,=（true Vx Vy)或C,= 法的执行过程，它们逐一地对公式F中的变量进行 (false VxVy),其中xy为非singleton..不失一般性， 赋值，直到确定公式的可满足性为止.所以可用分支 假设子句C1=(true VxVy)并对C,进行分支，分别 树的方法对基于分支回潮的算法进行时间复杂性的 判断2个子公式F[x/y]和F[x/y]的NAE-可满 分析.假设算法在分支树T中任意一个结点执行的 足性，只要其中一个为NAE-可满足，则可说明原公 操作都是多项式时间，那么算法的执行时间t为 式为NAE-可满足；第5~7步：考虑公式中存在2个 t≤#{Tae}×poly(F,)≤ 子句包含2个相同变量的3种情况.对每一种情况， (2×（#{Tism})-1)×poly(F:)≤
.510. 智能系统学报 第7卷 (Tmr)”×poly(F:), (2) 算法的时间复杂性，如measure and conquer方法.后 式中：符号#{T表示分支树T中结点的个数，符 续的工作将考虑利用非标准测度来分析算法的时间 号#{Ti}表示分支树T中叶子结点的数目，符号 复杂性 ploy(F:)表示每个结点操作所用的时间是多项式时 间.在本文中，忽略多项式时间. 参考文献： 定理4算法NAE在最坏情况下的时间复杂 [1]COLMERAUER A.Opening the Prolog III universe J]. 度上界为0(1.618")，其中n为公式中变量的数目. Byte Magazine,1987,12(9）):177-182. 证明下面将对算法NAE的每一行进行时间 [2]KLEER J.Exploiting locality in a TMS[C]//Proceedings of 复杂度分析。 the 8th National Conference on Artificial Intelligence.Bos- ton,USA,1990:264-275. 第1~3步：多项式时间内时间复杂变为0(1). [3]GU J.Local search for satisfiability (SAT)problem[J]. 第4步：不失一般性，假设子句C:=true VxV IEEE Transactions on Systems,Man and Cybernetics, y.在分支F[x/y]中C,=(true VyVy),由化简规则 1993,23(4):1108-1129. 3中7)可得，y=flse,因此消去x、y2个变量.在分 [4]李未，黄文奇.一种求解合取范式可满足性问题的数学 支F[x/y]中C1=(true VyVy),由化简规则3 物理方法[J].中国科学：A辑，1994,24(11)：1208- 中9)可得子句C,可直接消去，因此消去x一个变 1217. 量.执行时间为0(r(2,1)")=0(1.618). LI Wei,HUANG Wengi.A mathematic physical approach 第5步：在分支F[x/y]中子句C,=(yVyV to the satisfiability problems[J].Science in China:Series z),C2=(yVyVt),由化简规则3中6)可得，z=t= A,1994,24(11):1208-1217. y,消去x、a、t3个变量.分支F[x/y]中C,= [5]COOK S A.The complexity of the theorem-proving proce- (yVyVa),C2=(yVyVt),由化简规则3中 dures[C]//Proceedings of the Third Annual ACM Symposi- um on Theory of Computing.New York,USA,1971:151- 5)可得子句C1、C2可直接消去，消去x一个变量.执 158. 行时间为0(x(3,1))=0(1.466”). [6 ]MONIEN B,SPECKENMEYER E.Upper bounds for cover- 第6步：在分支F[x/y]中由化简规则3中5) ing problems[R].Universitat-Gesamtho Chschule -Pader- 和6)可得，2=y,消去x、z2个变量.同理在分支 bomn:Reihe Theoretische Informatik,1980. F[x/y]中可消去x、t2个变量.执行时间为 [7]HIRSCH E A.New worst-case upper bounds for SAT[J]. 0(r(2,2))=0(1.414"). Journal of Automated Reasoning,2000,24(4):397-420. 第7步：在分支F[x/y]中由化简规则3中6) [8]YAMAMOTO M.An improved 0(1.234)-time determin- 可得，2=y,t=y,消去x、云、t3个变量.在分支 istic algorithm for SAT[J].Lecture Notes in Computer Sci- F[x/y]中由化简规则3中5)可得子句C1、C2可 ence,2005,3827:644-653. 直接消去，消去x一个变量.执行时间为 [9]MONIEN B,SPECKENMEYER E.Solving satisfiability in less than 2n steps[J].Discrete Applied Mathematics, 0(r(3,1)")=0(1.466"). 1985,10(3):287-295. 第8步：在分支F[x/y]中由化简规则3中6) [10]BRUEGGEMANN T,KERN W.An improved local search 可得，2=y,消去x、z2个变量.在分支F[x/y] algorithm for 3-SAT[J].Theoretical Computer Science, 中由化简规则3中5)可得子句C,可直接消去，消 2004,329(1/2/3):303-313. 去x一个变量.执行时间为0(r(2,1)")= [11]DANTSIN E,GOERDT A,HIRSCH E A,et al.Adeter 0(1.618"). ministic (2-2/(+1))n algorithm for k-SAT based on lo- 由以上分析可得，算法NAE最坏情况下的时间 cal search[J].Theoretical Computer Science,2002,289 复杂度上界为0(1.618"). (1):69-83. [12]ZHANG Lintao,MADIGN C F,MOSKEWICZ M H,et 4结束语 al.Efficient conflict driven learning in a Boolean satisfi- ability solver[C]//Proc of the ACM/IEEE ICCAD 2001. 本文从变量规模的角度探讨了NAE-3SAT问题 New York,USA,2001:279-285. 在最坏情况下的时间上界.针对NAE-3SAT问题新 [13]ZECCHINA R,MEZARD M,PARISI G.Analytic and al- 提出的8条化简规则有效地提高了算法的时间效 gorithmic solution of random satisfiability problems[J]. 率.对于算法时间复杂性的分析，本文采用的是标准 Science,2002,297(5582):812815. 测度.近年来，众多学者也在采用非标准测度来分析 [14]ZECCHINA R,MONASSON R,KIRKPATRICK S,et al
第6期 谷文祥，等：基于分支回湖的NAE-3SAT问题求解算法 ·511· Determining computational complexity from characteristic 24rd AAAI Conference on Artificial Intelligence.Atlanta, phase transitions[J].Nature,1999,400(6740):133- USA,2010:217-222. 137. [22]周俊萍，殷明浩，周春光，等。最坏情况下粉SAT问题 [15]THOMAS J S.The complexity of satisfiability problems 最小上界[J].计算机研究与发展，2011,48(11)： [C]//Conference Record of the Tenth Annual ACM Sym- 2055-2063. posium on Theory of Computing.New York,USA,1978: ZHOU Junping,YIN Minghao,ZHOU Chunguang,et al. 216-226. The worst case minimized upper bound in #3-SAT[J]. [16]PORSCHEN S,RANDERATH B,SPECKENMEYER E.Lin- Joumal of Computer Research and Development,2011,48 ear time algorithms for some not-all-equal satisfiability prob- (11):2055-2063. lems[C]//Proceedings of the 6th International Conference on 作者简介： Theory and Application of Satisfiability Testing (SAT2003). 谷文样，男，1947年生，教授，博士 Santa Margherita Ligure,Italy,2003:172-187. 生导师，主要研究方向为智能规划与规 [17]WALSH T.The interface between P and NP:COL,XOR, 划识别、形式语言与自动机、模糊数学 NAE,1-in-k,and Horn SAT C]//Eighteenth National 及其应用.主持国家自然科学基金项目 Conference on Artificial Intelligencet.Edmonton,Canada, 3项，发表学术论文100余篇。 2002:685-700. [18]MONIEN B,SPECKENMEYER E,VORNBERGER O. Upper bounds for covering problems[J].Methods of Op- 傅琳璐，女，1988年生，硕士研究 erations Research,1981,43:419-431. 生，主要研究方向为自动推理和智能 [19]RIEGE T,ROTHE J,SPAKOWSKI H.An improved exact 规划. algorithm for the domatic number problem[J].Information Processing Letters,2006,101(3):101-106. [20]SHI Nungyue,CHU Chihping.A DNA-based algorithm for the solution of not-all-equal 3-SAT problem[C]//ASE In- ternational Conference on Information Engineering. 周俊萍，女，1981年生，讲师，博士， Taiyuan,China,2009:94-97. 主要研究方向为自动推理和智能规划， [21 ZHOU Junping,YIN Minghao,ZHOU Chunguang.New 主持东北师范大学青年基金项目1项， worst-case upper bound for #2-SAT and #3-SAT with the 发表学术论文10篇. number of clauses as the parameter[Cl//Proceedings of