第7卷第3期 智能系统学报 Vol.7 No.3 2012年6月 CAAI Transactions on Intelligent Systems Jun.2012 D0I:10.3969/j.i8sn.1673-4785.201109003 网络出版t地址：htp://www.cnki.net/kcma/detail/23.1538.TP.20120510.1619.001.html 最坏情况下Min-2SAT问题的上界 谷文祥12，姜蕴晖，周俊萍，般明浩 (1.东北师范大学计算机科学与信息技术学院，吉林长春130117；2.长春建筑学院基础教学部，吉林长春130607) 摘要：最坏情况下MaxSAT问题上界的研究已成为一个热门的研究领域.与MaxSAT问题相对的是MinSAT问题， 在求解某些组合优化问题时，将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度，因此对MinSAT问题 进行研究.针对Min-2SAT问题提出算法MinSATAlg,该算法首先利用化简算法Simplify对公式进行化简，然后通过分 支树的方法对不同情况的子句进行分支.从子句数目的角度分析算法的时间复杂度并证明Mi2SAT问题可在 0(1.1343")时间内求解，对于每个变量至多出现在3个2-子句中的情况，得到最坏情况下的上界为0(1.1225)， 其中n为变量的数目. 关键词：MaxSAT:MinSAT;Min-2SAT;MaxSAT问题的上界：Min-2SAT问题的上界；子句数目；分支树 中图分类号：TP301文献标志码：A文章编号：16734785(2012)030241-05 New worst-case upper bounds for Min-2SAT problems GU Wenxiang2,JIANG Yunhui',ZHOU Junping',YIN Minghao' (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 rigorous theoretical analyses of algorithms for solving the upper bounds of maximum satisfiability MaxSAT)problems have been proposed in research literature.The opposite problem of MaxSAT is the minimum satisfiability (MinSAT)problem.Solving some combinatorial optimization problems by reducing them to MinSAT form may be substantially faster than reducing them to MaxSAT form,so the MinSAT problem was researched in this paper.An algorithm(MinSATAlg)was presented for the minimum two-satisfiability (Min-2SAT)problem.In this paper,first,the simplification algorithm Simplify was used for simplification of formulas.Secondly,the branching tree method was used for branching on different kinds of clauses.It was proven that this algorithm can solve the Min-2SAT problem in 0(1.134 3),regarding the number of clauses as parameters.The upper bound in the worst case was derived as 0(1.122 5"),where n is the number of variables in an input formula for a particu- lar case of Min-2SAT in which each variable appears in three 2-clauses at most. Keywords:maximum satisfiability;minimum satisfiability;minimum two-satisfiability;upper bounds for maximum satisfiability;upper bounds for minimum two-satisfiability;number of clauses;branching tree 人工智能研究领域存在着很多计算困难的问 时间的求解算法.这时从理论上分析这些问题在最 题，如SAT(satisfiability)问题、QBF(quantified boole- 坏情况下的时间复杂性上界尤为重要，因为此时对 an formula)问题、智能规划问题、模型诊断问题等. 该上界的一个微小的改进，例如从O(c)改进为 若P≠NP成立，人们将无法为这些问题找到多项式 O((c-ε))，就会使得问题求解的算法在效率上获 得指数级别的提高.以SAT问题为例，作为第一个 收稿日期：20110906.网络出版日期：201205-10. 基金项目：国家自然科学基金资助项目(61070084)；国家自然科学青 被证明是NP完全的问题，改进其在最坏情况下的 年基金资助项目(60803102)；中央高校基本科研业务费专 时间上界受到了研究人员的广泛关注.MaxSAT 项资金资助项目(11QNJJ006) 通信作者：姜蕴晖.E-mail:jiangyh2l5@nenu.ed血.cn (maximum satisfiability)问题是SAT问题的扩展，它
·242 智能系统学报 第7卷 指的是给定一个命题逻辑公式，找到一组使真值赋 一个子句都可满足时，公式F在赋值“下可满足， 值同时满足最多的子句.与SAT问题一样，MaxSAT 公式F同时可满足的最少的子句数记为 问题在计算机科学领域有着十分重要的地位，因为 PesVal(F).称文字l出现在子句中如果子句包含l, 它是求解人工智能和组合优化问题的基础12].当 称变量x出现在子句中如果子句包含x或x,本文 公式中子句的长度至多为2时称之为Max-2SAT 中，用#(F,)表示文字1出现在公式F中的次数，用 (maximum two-satisfiability)问题，它是一个NP完全 #(F,)表示文字l在公式F中的k子句中出现的 的问题3].近年来，众多学者对Max-2SAT问题进行 次数. 了研究4，已经将其最坏情况下的上界缩小到 用F[门表示将F中所有包含1的子句替换为 O(2m.32)[8I.与MaxSAT问题相对的是MinSAT T,消去所有1和所有F中的空子句.用F[L=L2] (minimum satisfiability)问题，它指的是给定一个命 表示将所有的1用12替代，并将所有的11用12 题逻辑公式，找到一组使真值赋值同时满足最少的 替代. 子句.虽然人们对MaxSAT问题已经做了非常多的 定义6Min-2SAT问题.给定一个命题逻辑公 研究，但对MinSAT问题的研究却并不深入.目前， 式F,找到一组使真值赋值满足最少的子句，如果子 对MinSAT问题的求解主要采用近似方法[9-o].此 句的长度至多为2，则称其为Min-2SAT问题. 外，LI等在文献[11]中将MinSAT问题转换为Max 定义7变量的度.变量x的度是指包含x的 SAT问题，给出了一个MinSAT求解器.事实上，在 2-子句的个数，也就是说，如果变量x的度为k,则 求解某些组合优化问题时，将其转化为MinSAT问 #2(F,x)+#2(F,7x)=k 题比转化为MaxSAT问题有着更快的速度，所以研 定义8变量的邻居.变量x的邻居是指所有 究MinSAT问题也有着十分重要的理论意义和实际 和x一起出现在同一个2-子句的变量， 应用价值.正如人们对MaxSAT问题的研究主要集 用V(F)表示F中所有变量的集合，对于变量 中在Max-2SAT问题上，笔者同样着眼于MinSAT问 集合VCV(F),用N(F,V)来表示变量集合V的 题中子句长度不超过2的情况，即对Min-2SAT问题 所有邻居， 进行研究，提出了一种求解Min-2SAT问题的算法， 用G(F)表示一个无向图，V(F)是所有顶点的 并证明了算法在0(1.1343m)时间内可解. 集合，如果F中2个变量出现在同一个2子句中， 1基础知识 则在这2个顶点之间添加1条边 1.2复杂性分析方法 1.1基本概念 本节介绍分支算法的复杂性分析方法，首先给 为了讨论方便，首先介绍本文需要的相关概念 出分支树的概念 定义1真值赋值.给定一个布尔变量集合V= 分支树是由(i>0)个结点组成的有限集合Q, {x1,x2,…,xn},定义在V上的真值赋值是一个函数 其中一个特定的结点为根结点，标记为公式F,除根 u:V→{ue,false.每个真值赋值可以用一个n元 结点以外的其他结点被划分为(G≥0)个互不相交 布尔向量表示.对V中任意一个布尔变量，若它在 的有限集合Q1,Q2,…,Q,分别标记为公式F,F2, 真值赋值μ下取真，则(x)=1,否则μ(x:)=0. …,F其中每一个集合又都是分支树，称为根结点 定义2文字.对任意一个布尔变量x,称符号 的子分支树，分别表示对公式F中的某些变量进行 x和x是其文字，其中x是正文字，x是负文字. 赋值后得到的公式，即公式F的子公式.叶子结点 定义3纯文字.给定一个公式F和F中任意 标记的公式为空公式或者其中存在一个空子句. 一个布尔变量x,若x只以正文字或负文字的形式 分支树中的每一个结点都有1个分支向量.设 出现在公式F中，则称x为纯文字 分支树中某一个结点是F。,它的子结点分别是F1, 定义4子句.子句是若干文字的析取，用集合 F2,…,F则结点F的分支向量为T=(r1,2,…, C表示，C=l1V2V…Vl,其中l1,2,…,l是文字. re),其中r:=f八F)-f(F),(F)=m(F)是公式 子句C中文字的个数称为子句的长度，记作IC1. F。中子句的数目，f(F)=n(F。)是公式F。中变量 k子句是指子句长度为k的子句.永真子句T指 的数目 的是对子句的变量任意赋值时子句都是可满足的. 每个结点的分支向量的值被称为结点的分支 定义5CNF范式.CNF范式是若干子句的合 数，可用式(1)计算 取，用F表示，F=C1∧C2∧…AC,其中C1,C2, k (1) …,C:是子句.CNF范式F也称为公式，当且仅当每 ”=,>0
第3期 谷文祥，等：最坏情况下Min-2SAT问题的上界 ·243· 定理112】设分支树T的根结点标记为公式 b)如果&=false,B=tue,则返回Simplipy F,则分支树T中叶子的个数不超过(rm),其中 （Fx1=7x2]). (F)是公式F中子句的数目或变量的数目. c)如果a=true,B=false,则返回Simplipy 由分支树的定义可以看出，分支树的构造过程相 (F[x1=2]). 当于基于DPLL(Dais-Putnam-Logemann-Loveland)算 d)如果a&=true,B=true,则返回Simplipy 法的执行过程.算法逐一对公式F中的变量进行赋值， (F[x1]). 直到确定任意一个赋值满足或不满足公式F为止.假 对于给定的范式，重复使用化简算法 设基于DPL的算法在分支树T中任意一个结点执行 Simplify(F)对其进行化简，直到范式不能再应用算 的操作都是多项式的，那么从子句数目的角度考虑，算 法中任何一条化简规则为止.这样在求解Min-2SAT 法的执行时间t为 问题时可以减少算法需要考虑的情况，以减弱算法 t≤#{To}x ploy(F:)≤ 的复杂性。 (2×(#{1Tees})-1)×ploy(F:)≤ 根据化简规则，可以得到下面的引理。 (rmm)m×ploy(F:). 引理1令F是一个2-CNF范式，F'= 若从变量数目的角度考虑，算法的执行时间t为 Simplify(F),则F'中不包含度至多为2的变量. t≤#{Tde}x ploy(F:)≤ 证明若变量的度为1，则可通过化简算法 (2×(#{Tme})-1)×ploy(F:)≤ Simplify(F)中化简规则2)对其化简；若变量的度为 (rmm)"×ploy(F:) 2,则可通过化简规则4)进行化简.因此公式化简后 用F表示2-CNF公式，用N,(F)表示在公式F 只包含度至少为3的变量. 的2子句中出现次的变量的个数.很容易得到 引理2令F是化简后的公式，a、x是邻居，a K(P)=∑xX(P 的度为3，则在F[x]和F[x]中，至少有一个化简 2 规则会对a赋值. 式中：K2(F)表示F中2-子句的数目.根据文献 证明考虑变量a所有可能出现的情况. [13]可以对其稍作修改，得到新的复杂性测度为 1)当(aVx)∧(aVx1)∧(aVx2)时，若x= =(D+Lw(回+四xX9 0,则由化简规则3)可知a=1. 2 2)当(aVx)∧(aV1)∧(aVx2)时，若 2化简规则 x=1,则由化简规则2)可知a=0. 3)当(aVx)(aVx)A(aVx2)Aa时，若 在给出求解Min-2SAT问题的算法之前，首先 x=0,则由化简规则1)可知消除了a和一a,再由化 给出一个化简算法如下， 简规则2)可知a=1. 化简算法Simplify(F) 4)当(aVx)A(aVx1)∧(aVx2)AaAa 输入：一个2-CNF范式F. 时，若x=1,则由化简规则3)可知a=0. 输出：一个化简后的2-CNF范式F. 5)当(aVx)A(aVx1)∧(aVx2)Aa时， 1)如果F=FU{C,D},并且对于一个文字L 若x=1,则由化简规则3)可知a=0. 有C\{l}=D\{l},则返回Simplipy(FoU{C\{l, 6)当(aVx)∧(aVx1)∧(aVx2)∧a时， T}) 若x=0,则由化简规则3)可知a=1. 2)如果F中存在一个文字1满足#(F,)= 由于公式F已化简，所以不存在其他情况，引 0,则返回Simplipy(F[l]). 理得证 3)如果F中存在一个文字1满足#(F,)≥ #(F,I),则返回Simplipy(F[l]). 3算法MinSATAlg 4)如果F中存在2个变量x1和x2,并且1至 本文给出一个求解Min-2SAT问题的算法Min- 多出现在一个不含x2的2-字句中，令α和B分别为 SATAlg,它是一个典型的分支算法.具体算法描述 F[x2]和F[2]中通过化简规则对1所赋的布尔 如下. 值(tue或者false),则根据&和B的值将公式F化 输人：一个2-CNF范式F. 简的方法为： 输出：PesVal(F). a)如果a=false,B=false,则返回Simplipy 1)F=Simplify(F). (F[x]) 2)如果F只包含T字句，则返回L(F)
.244 智能系统学报 第7卷 3)如果F=F1UF2,并且F,和F2没有相同的 情况下很容易看出r(F)=N(F),所以只需要证明 变量，则返回MinSATAlg(F,)+MinSATAlg(F2). 以变量数目为参数时的复杂度为0(r(6,6)")= 4)选择变量x使r(r(F)-r(Simpli断(FLx]), 0(1.1225).由于变量的度均为3，所以变量的个 r(F)-r(Simplify(F[,x])最小，并返回min(MinSATAlg 数必为偶数，F的每一次分支都为(2k,2),其中k F[x]),MinSATAlg (F[x])). 和1都是整数. 在算法MinSATAlg中，首先，应用化简规则对 a)如果公式F中包含3个变量且其中任意2 公式进行化简；第2步是指如果公式中只包含永真 个变量都出现在同一个2子句中，则在图G(F)中 子句T,则返回公式中子句的数目；第3步考虑公式 形成1个三角形.令a、b、c为形成三角形的3个变 中包含组件的情况，即将公式分支成2个更简单的 量，可以看出N({a,b,c})包含至少2个变量，至少 公式并对其递归调用；最后根据每次递归调用返回 1个邻居只和{a,b,c}中的1个一起出现，将其标记 的结果得到最后的结果.定理1中给出了算法的时 为d并和c一起出现，如图1(a)所示.对d进行分 间复杂度 支的复杂度为0(r(6,6)”)=0(1.1225").这是因 定理2给定一个2-CNP范式，算法Mim 为对d赋值后，c只和a、b一起出现，或出现在单元 SATAIg在0(1.1343")时间内返回公式中同时可以 子句中，化简规则或者对c直接赋值，或者用包含 满足的最少的子句数. a、b的子句替代含c的子句.对于前一种情况，a、b 证明 也会通过化简规则被消去，对于后一种情况通过化 1)当公式F中包含个度大于6的变量时.由化 简规则4)会消去a、b中的一个.所以对d赋值后还 简规则可知，F中的所有变量至少出现在2个没有x出 会至少再消去4个变量，因此对d进行分支的复杂 现的2子句中.度至少为3的变量使r至少减少1/2， 度为0(r(6,6)")=0(1.1225"). 这是因为N:的2个系数的差至少为1/2.这样，当对x b)考虑图G(F)中不包含三角形的情况.假设 赋值后，r至少减少(w/2(x被消去)+o/2(x的邻居 F包含一个变量x,其邻居为a、b、c,这样在F[x]和 的度减少).因此，对x进行分支的复杂度至少为 F[x]中化简规则会对a、b、c中至少一个赋值.很 0(r(6,6)m)=0(1.1225m). 容易看出对x进行分支的复杂度为0((6,6)")= 2)当公式F中变量的度都不超过5时.令x是 0(1.1225). 个度为5的变量，用k表示在公式F中出现j次 c)下面需要考虑的是对F中的一个变量进行分 且和x一起出现i次的变量个数，其中1≤i≤j≤5. 支时，化简规则会在一个分支中对其全部邻居赋值的 由于F已化简，所以当j≤2或j-i≤1时k:=0.由 情况.考虑一个变量，W({x})={a,b,c.如果 于x出现在5个2-子句中，所以有 1N({a,b,c{)1≥5，则对x分支的复杂度为 k13+k14+k15+2k4+2k25+3k35=5. 0(r(4,10))C0(1.1120).如果N({a,b,c})1<5, 对于共出现j次并且与x一起出现次的变量， 这就意味着或者存在一个变量y≠x并且N(y)={a, 在对x赋值后其出现在2子句中的次数为j-,令 b,c(如图1(b)所示)，或者存在2个变量y,z≠x并且 F'为对F中的变量x赋值后得到的公式，则有 IN(y)U{a,b,cI=2,IN(z)U{a,b,cI=2(如图1 r(F)-r(F)=(k3+1.9(k4+k4)+ (c)所示).前一种情况对b分支的复杂度为O(r(6, 2.5(k15+k25+k35+1))-（k14+k25+1.9k5)≥ 6)")=0(1.1225),后一种情况对x赋值的复杂度为 0.6(k13+k14+k1s+2k24+2k25+3k35)+2.5= 0(r(4,10)")C0(1.1120). 0.6×5+2.5=5.5. 由此可见，对x进行分支的复杂度至少为 0(r(5.5,5.5)m)=0(1.1343m) 中式 3)当公式F中变量的度都不超过4时.与第2 (b) (c) 种情况类似可得到 k13+k4+2k4=4, 图1情况4)的不同例子 r(F)-r(F')=(kg+1.9(k4+k4+1)-(k4)≥ Fig.1 Different cases in 4) 0.9(kg+k4+2hm)+1.9=0.9×4+1.9=5.5. 由此可见，以变量数目为参数时的复杂度为 因此，对x进行分支的复杂度至少为0(r(5.5, 0(r(6,6)")=0(1.1225).从而得到一个化简后 5.5)m)=0(1.1343m). 的公式F只包含度为3的变量时，则对其中一个变 4)当公式F中所有变量的度均为3时.在这种 量进行分支的时间复杂度为0(r(6,6)m)=
第3期 谷文祥，等：最坏情况下Min2SAT问题的上界 ·245· 0(1.1225m) [7]BINKELE-RAIBLE D,FERNAU H.A new upper bound for 综上所述，给定一个2-CNF范式，算法Min Max-2-SAT:a graph-theoretic approach[].Joumal of Dis- SATAlg在O(1.1343m)时间内返回公式中同时可 crete Algorithms,2010,8(4):388-401. [8]GASPERS S,SORKIN G B.A universally fastest algorithm 以满足的最少的子句数，即定理2得证 for Max 2-Sat,Max 2-CSP,and everything in between[J]. 4结束语 Joural of Computer and System Sciences,2012,78(1): 305-335. MaxSAT问题是求解人工智能和组合优化问题 [9 AVIDOR A,ZWICK U.Approximating MIN 2-SAT and 的基础，而在求解某些组合优化问题时，将其转化为 MIN 3-SAT[J].Theory of Computing Systems,2005,38 MinSAT问题比MaxSAT问题有着更快的速度，因此 (3):329-345. 求解MinSAT问题并分析其复杂度有着很高的实际 [10]MARATHE M V,RAVI S S.On approximation algorithms for the minimum satisfiability problem J].Information 价值.本文研究了MinSAT问题中每个子句长度不 Processing Letters,1996,58(1):23-29. 大于2的情况，即Min-2SAT问题，提出了一个求解 [11]LI Chumin,MANYA F,QUAN Zhe,et al.Exact MinSAT Mn-2SAT问题的算法并证明了算法的时间复杂度 solving[C]//Proceedings of the 13th Interational Confer- 为0(1.1343)，其中m为公式中子句的数目.笔者 ence on Theory and Applications of Satisfiability Testing. 运用了一种新的复杂性测度来测量算法的运行时 Berlin/Heidelberg,Germany:Springer-Verlag,2010: 间.另外还证明了对于每个变量至多出现在3个2 363-368. 子句中的情况，其最坏情况下的时间复杂度为 [12]ZHOU Junping,YIN Minghao,ZHOU Chunguang.New 0(1.1225"),其中n为变量的数目. worst-case upper bound for #2-SAT and #3-SAT with the number of clauses as the parameter[C]//Proceedings of 在今后的工作中，可以进一步修正复杂性测度 the Twenty-Fourth AAAI Conference on Artificial Intelli- 或通过加入冲突子句等方法，来改善算法并减少算 gence.Atlanta,USA,2010. 法的时间复杂度 [13]KOJEVNIKOV A,KULIKOV A S.A new approach to pro- ving upper bounds for MAX-2-SAT[C]//Proceedings of 参考文献： the Seventeenth Annual ACM-SIAM Symposium on Dis- [1]HANSEN P,JAUMARD B.Algorithms for the maximum crete Algorithms.New York,USA:ACM,2006:11-17. satisfiability problem[J].Computing,1990,44(4):279- 作者简介： 303. 谷文祥，男，1947年生，教授，博士 [2]WALLACE R J.Enhancing maximum satisfiability algo- 生导师，主要研究方向为智能规划与规 rithms with pure literal strategies[C]//Proceedings of the 划识别.主持或参与国家自然科学基金 11th Biennial Conference of the Canadian Society for Com- 项目5项、教育部重点项目2项、省科 putational Studies of Intelligence on Advances in Artificial 委项目1项.发表学术论文130余篇， Intelligence.London,UK:Springer-Verlag,1996:388- 出版专著《智能规划与规划识别》，2011 401. 年获得吉林省专著类一等奖， [3]NIEDERMEIER R,ROSSMANITH P.New upper bounds for MaxSat[C]//Proceedings of the 26th Interational Col- 姜蕴晖，女，1987年生，硕士研究生， loquium on Automata,Languages and Programming.Lon- 主要研究方向为智能规划与自动推理。 don,UK:Springer-Verlag,1999:575-584. [4]GRAMM J,HIRSCH E A,NIEDERMEIER R,et al. Worst-case upper bounds for MAX-2-SAT with an applica- tion to MAX-CUT [J].Discrete Applied Mathematics, 2003,130(2):139-155. [5]KNEIS J,ROSSMANITH P.A new satisfiability algorithm 周俊萍，女，1981年生，讲师，主要 with applications to Max-Cut:Technical Report AIB2005-08 研究方向为智能规划与自动推理，发表 [R].Aachen,Germany:Department of Computer Science, 学术论文5篇. RWTH Aachen University,2005. [6]KULIKOV A S,KUTZKOV K.New bounds for MAX-SAT by clause learning C]//2nd International Symposium on Computer Science in Russia.Ekaterinburg,Russia,2007: 194-204