·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