（计算机软件与理论专业论文）maxsat求解中的搜索和推理.pdf

m 拇s a t 求解中的搜索和推理 专 业： 计算机软件与理论 博士生：林瀚 指导老师：苏开乐教授 摘要 命题逻辑的可满足性问题( s a t ) 是计算机科学中的核心问题最大可满 足问题( m 措s a t ) 是s a t 问题的一个自然的扩展对于给定的c n f 公式，m 册 s a t 问题的目标是找到一个赋值使其满足最多的子句m 孵s a t 是一个重要 的n p 一难优化问题由于人工智能、电路自动设计、统计物理、生物信息学等领 域的许多问题都可以转化为m 抒s a t 问题，所以近十年来，m 觚_ s a t 问题引起 越来越多的兴趣和关注。 求解m 错s a t 的算法可以分为完备算法和不完备算法就不完备算法而 言，m 觚- s a t 和s a t 并无很实质的区别，所以当前对m a x s a t 算法的研究主要 集中在完备算法设计高效完备算法的关键在于如何进行快速的搜索和有效的 推理本文的工作正集中于这两方面 在推理方面，本文提出一个比前人更一般的m a x s a t 逻辑框架，给出 了m a x s a t 推理中等价、蕴含以及a 一等价等概念的形式化定义在这一基础 上，本文进一步给出若干a 一等价规则的例子，扩充了求解m a x s a t 的推理规 则作为运用推理规则的例子，本文利用已有的推理规则改进了前人给出的一 个不可满足子句数目的下界 在搜索方面，当前的完备算法多数采用分支定界的搜索机制提高分支定 界算法效率的关键在于求得紧的下界本文分析了前人计算下界方法的不足， 提出了基于学习的计算方法具体而言，学习分成两方面一方面，搜索树中除 根结点外的每个结点都向自己的父结点学习不相交的矛盾子句集。另一方面， 一种被称之为失败文字检测( f a i l e dl i t e r a ld e t e c t i o n ，f l d ) 的方法被之前的一 些m a x s a t 求解工具用于计算下界；在本文的算法中，搜索树中的每个结点都 向过去搜索过的结点学习f l d 的有效性，并根据之前的效果来决定在当前结点 m a x - s a t 求解中的搜索和推理 是否运用f l d 这种基于学习的计算方法，既避免了不必要的计算，又保证了下 界的单调性 带权重的m 噼s a t 问题是m a x s a t 问题的扩展，它们具有更强的描述问 题的能力和更广泛的应用本文将上述方法进一步扩展到带权重的问题，并 开发了一系列的求解工具实验结果表明，这些新的方法，无论是在随机实 例还是在由实际问题转换而来的结构化实例，都提高了已有求解工具的性能 值得一提地，其中一个工具l b s a t 在2 0 0 7 年的国际m a 珏s a t 求解评比中，解 决了最多的带权实例而在2 0 0 8 年的m 册s a t 求解评比中，我们开发的新求解 器i n c m a x s a t z i n c w m a x s a t z 在全部1 1 项评比中，获得3 项第一名和4 项第二名 除了设计和实现实用的求解工具以外，本文也从理论上关注m a x s a t 算法 复杂度的改进本文定义了和前人不同的非标准复杂性度量，对m 擗2 一s a t 和 问题，给出了d 。( 2 k 5 6 2 5 ) 的算法，其中k 是公式的子句数用类似的方法，本文 还得到m a x c u t 问题0 + ( 2 5 6 2 5 ) 的算法，其中m 足图中所有边的权重之和 关键词：s a t ，m a 治s a t ，分支定界算法，下界的计算，m a x c u t s e a r c ha n di n f e r e n c ei nm a x s a ts o l v i n g m a j o r ： p h d c a n d i d a t e ： s u p e r v i s o r ： c o m p u t e rs o 危w a r ea n dt h e o r y h a nl i n p r o f e s s o rk a i l es u a b s t r a c t i i h ep r o p o s i t i o n a ls a t i s 矗a b i l i t yp r o b l e m ( s a t ) i sac e n t r a lp r o b l e mi nc o l - p u t e rs c i e n c e i h em a x i m u ms a t i s f i a b i l i t y ( m a 静s a t ) p r o b l e mi san a t u r 出e x _ t e n s i o no fs a t g i v e nac n f f o r m u l a ，m a x s a ti st of i n da na s s i g n m e n tw h i c h s a t i s f i e sm a x i m u mn u m b e ro fc l a u s e s ，m a x s a ti sa ni m p o r t a n tn p - h a r do p t i m l z a t l o np r o b l e m s i n c em a l l yr e a l w o r l dp r o b l e m si nv a r i o u s 丘e i d s ，e g ，a r t i ：丘c i a i i n t e l h g e n e e ，e l e c t r o n i cd e s i g na u 乞o m a t i o n ，s t a t i s t i e a lp h y s i c sa n db i o i n f o r m a t i c s ， c a nb ee x p r e s s e da sm a 静s a ti n s t a n c e s ，m a x s a th a l sa t t r a c t e di n c r e a s i n gi n - t e r e s ta n da t t e i 】t i o n a l g o r i t h m sf o rm a x s a - tc a nb ed i v i d e di n t ot w oc l a s s e s ： c o m p l e t ea l g m r 】t h m sa n dj n c o m p l e t ea l g o r i t h m s a st h ed i f f e r 锄c e sb e t w e e ni n c o m p l e t ea l g o r i t h m sf o rm 躲s a ta n ds a ts e e mn o te s s e n 乞i a l ，t h ee u r r e n tr e s e a r c h 。nm 躲 s a ta l g o r i t h m sh a sb e e nm a i n l yf o c u s e do nc o m p l e t ea l g o r i t h m s t h e k c yp o i n t 8 t oi m p r o v et h ee 伍c i e n c yo fc o m p l e t ea l g o r i t h m s1 i ei nh o w t op e r f o r mf a s ts e a r c h a n d 疆e c t i v ei n f e r e n c e t h i st h e s i sf o e u s e so nt h e s et w oa s d e c t s f 0 ri n f e r e n c e ，t h i st h e s i sp r o p o s e sam o r eg e n e r a ll o 西c a l 矗a m e w o r kf o rm a 洛 s a t r e a s o n i n g i i lt h i sf r a m e w o r k ，t h ec o n c e p t so fs e m a n t i ce n t a i l m e n t ，e q u i v a - l e n c ea n da e q u i v a l e n c ei nt h ec o n t e ) ( to fm a x s a t 盯ei n t r o d u c e d t h i st h e s i 8 f u r t h e rs h o w st h a ts o m ei n f e r e n c er u l e sa r ea e q u i v a l e n t ，t h e s er u l e sa r es o u n d a n dc a nb eu s e dt o g e t h e rw j t he q u i v a 】e n to n e si nm a x - s a t s 0 1 v i n g a sac a u s e s t u d y ，t h i st h e s i sd e m o n s t r a t e sh o wt oe x p l o i tas i m p l ei n f e r e n c er u l et oi m d r o 、他 ap r e v i o u sl a w rb o u n do ft h en u m b e ro fu n s a t i s 丘e dc l a u s e s f o rs e a r c h ，m o s ts t a t e _ o f - t h 争a r ta l g o r i t h m sa r eb a s e do nt h eb r a n c ha n d b o u n d ( b n b ) s c h e m e t h ek e yp o i n tt oe n h a n c eb n ba l g o r i t h m si st oo b t a i n t i g h t e rl o r e rb o u n d s t h i st h e s i sa n a l y z e ss e v e r a ld r a w b a u c l 【so ft h ee 妇s t i n gl o 他r b o u n dc o n l p u t i n gm e t h o d s ，a n dp r o p o s e san e w a p p r o a c hc a u e dw i t h i n p r o b l e m 1 e a r n i n g m o r es p c c i f i c a l l y t h e1 e a r n i n gi n c l u d c st w os t e p s f i r s t ，e a c hn o d e e x c e p tt h e r o o to ft h es e a r c ht r e el e a m sd 蚓o i n ti n c o n s i s t e n ts u b f o r m u l a sf r o m i t sp a r e n tn o d e s e c o n d ，ap r o c e d u r ec a l l e df a i l e dl i t e r a ld e t e c t i o n 门? l d li s u s e d t oc o m p u t el o w e rb o u n d sb ys o m ee 姬s t i n gm a x s a ts o l v e r s i nt h el e a r n i n g a l g o r i t h m ，e a c hn o d eo ft h es e a r c ht r e el e a r n si n f o r m a t i o na b o u te 丑b c t i v e n e s s o ff l df o mt h en o d e se x p l o r e dp r e v i o u s l ya n dd e c i d e sw h e t h c rf l ds h o u l d b ei n v o k e da tt h ec u r r e n tn o d ea c c o r d i n gt os u c he 虢c t i v e n e s s t h i sl e a r n i n g m e t h o dn o to n l ya 、r o i d su n n e c e s s a 巧c o m p u t a t i o n ，b u ta l s og u a r a 础e e st h a tt h e l a w e rb o u n di sm o n o t o n e w 西g h t e dm a x s a ta n dp a r t i a lm a * s a t ，t w oe x t e n s i o n so fm a x s a t h a 鹏 s t r o n g e re x p r e s s i v ep 0 w e ra n dw i d e ra p p l i c a t i o n t h i st h e s i sg e n e r a i i z e st h e a b o v ea p p r o a c h e st o 、7 l r e i g h t e dm a x s a ta n dp a r t i a lm a x s a t s e v e r a ls o l v e r s h a v eb e e nd e v e l o p e d ，a n dt h ee x p e r i m e n t a lr e s u l t sd e m o n s t r a t et h a tt h en e w s 0 1 v e r so u t p e r f o r mt h es t a t e o f t h e a r ts o l v e r so naw i d er a n g eo fi n s t a n c e si n c l u d i n gr a n d o ma n ds t r u c t u r e do n e s l b s a t ，o n eo ft h e s et o o i s s o l v e dm o r e i n s t a n c e st h a no t h e r si nt h e ，e i g h t e dc a t e g o r yo ft h em a ) ( - s a te v a l u a 七i o n2 0 0 7 i i lt h em a x - s a te v a l u a t i o n2 0 0 8 ，i n c m a 弼a t za n di n c w m a x s a t z w h i c hw r e r e a l s od e v e l o p e db yu s ，a r et h ew i n n e r si nt h r e ec a t e g o r i e sa n dt h es e c o n db e s t o n e si na n o t b e rf o u rc a t e g o r i e s b e s i d e sd e s i g n i n ga n di m p l e m e n t i n gp r a u e t i c a lm a x - s a ts o l v e r s ，t h i st h e s i s a l s oc o n c e r n st h et i m ec o m p l e x i t ya n a l y s i sf o rt h em a x s a ta l g o r i t h m st h e o r e t i c a l l y b yt h ec h o i c eo fan o n s t a n d a r dc o m p l e x i t ym e a s u r e ，t h et h e s i sp r o p o s e s a na l g o r i t h mf o rm 冰2 一s a ti n0 + ( 2 k 5 。6 2 5 ) w h e r eki st h en u m b e ro ft h eg i v e n f o r m u l a w i t ha8 i m i l a r 印p r o a c h ，t h et h e s i sa l s op r e s e n t sa n o t h e ra l g o r i t h mf o r m a x - c u ti no + ( 2 驯5 6 2 5 ) w h e r emi st h es u mo ft h ew e i g h t so ft h ee d g e si nt h e g i v e np ，a p h k e y 、 ，0 r d s ：s a t ，m a x - s a t ，b r a n c ha n db o u n d ( b n b ) ，l o w e rb o u n dc o i i 卜 v p u t a t i o n ，m a x c u t 论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究工作所取得的成果。除文中已经注明引用的内 容外，本论文不包含任何其他个人或集体已经发表或撰写过 的作品成果。对本文的研究作出重要贡献的个人和集体，均 已在文中以明确方式标明。本人完全意识到本声明的法律结 果由本人承担。 学位论文作者签名：瘀喻 日期：声黾年厂月旷日 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规定，即： 学校有权保留学位论文并向国家主管部门或其指定机构送 交论文的电子版和纸质版，有权将学位论文用于非赢利目的 的少量复制并允许论文进入学校图书馆、院系资料室被查 阅，有权将学位论文的内容编入有关数据库进行检索，可以 采用复印、缩印或其他方法保存学位论文。 、 学位论文作者签名：糟 导师签名：澎矗岛 日期：加g 年厂月f 歹日日期：触8 年厂月f 厂日 第一章引言 命题逻辑公式的可满足问题( s a t ) 是计算机科学和人工智能领域的核心 问题s a t 问题的研究既有深刻的理论意义，又有着广阔的应用前景近二十 年来，对s a t 问题的研究更加深入，求解s a t 问题的高效算法和工具层出不穷， 与s a t 相关的研究领域取得长足进展f 1 1 然而，尽管s a t 的求解工具在智能规 划、模型检测和电路验证等方面有着很成功的应用，但由于s a t 问题本身相对 简单，使得s a t 的求解工具在很多应用领域，依旧鞭长莫及于是，近年来，越来 越多的学者开始研究s a t 的扩展问题，如m o d e lc o u n t i n g ，q b f ，和m a x s a t 等 问题 本文的研究重点是m a 汝s a t 问题的高效完备算法本章介绍m a x - s a t 的背 景知识，当前求解m a x s a t 的主要方法，以及本文的主要贡献和各个章节的主 要内容 1 1背景 现实生活中，人们的活动总是受到各种“约束条件”的制约学生选修课 程，上课时间不能冲突，所选课程的总学分必须达到院系的要求物流公司配送 货物，运输工具不能超载，货物送达的时间也要符合客户预先的要求这样的例 子，小到每个人的日常生活，大到企业和政府的重要决策，可以说是不胜枚举 由于这类问题无处不在，它引起了众多领域，特别是运筹学、计算机科学 和人工智能领域学者的关注他们将这类问题称之为约束满足问题( c o n s t r a i n t s a t i s f a c t i o np r o b l e m ，c s p ) 下一节要介绍的s a t 问题就可以看作约束满足问 题的一个特例非形式化地讲，约束满足问题就是给定一组变量，每个变量有各 自的值域，再给定一组约束，每个约束指定若二f 个变量，并规定这些变量如何取 值才满足约束，问题的目标是找到对所有变量的赋值，使得其满足所有的约束 例如，对于一个学生选课的问题，我们可以这样定义对应的c s p 问题：每一门待 选的课程对应一个变量，变量的取值是“选”或“不选”，约束是上课时间有交 叉的课程不能同时取值为“选”等而这个问题的解便是一组对所有课程“选” 或“不选”的赋值，这组赋值满足所有的约束 2 m a x s a t 求解中的搜索和推理 但在许多场合，我们发现，对给定的问题，要找到一个解让其满足所有的约 束是不可能的( 有些约束相互矛盾) ，或者是没有必要的例如，在选课时，有 些学生可能会有这样的要求( 也就是约束) ：只选在校本部上的课，只选开卷考 试的课等如果这些约束都要满足的话，那可能导致另外一些约束( 比如一学期 选修课的学分不能低于1 0 ) 不能满足在这种情况下，我们往往先把约束分为硬 约束( 危n 纪c d 礼s 化i 秕) 和软约束( s 妒c d 竹z m 溉) 所谓硬约束是指一定要满足 的约束，例如选课中的“所选课程上课时间不能冲突”，“选修学分总和应大于 等于1 0 ”等；而软约束则是最好要满足的约束，如“只选开卷考试的课”等这 个时候，我们的目标便是寻找一组赋值，使其满足所有的硬约束，并满足尽可 能多的软约束，这样的问题我们称之为约束优化问题( c o n s t r a i n to p t i m i z a t i o n p r o b l e m ) 显然，如果约束优化问题在所有约束都是硬约束，那它就是约束满 足问题所以，约束问题可以看作约束优化问题的特例 在一些具体问题中，除了硬约束比软约束重要以外，不同的软约束也可能 会有不同程度的重要性例如，学生选课时，町能更看重“在校本部上课”这一 要求，而相对而言，“考试开卷”并不那么重要这种情况下，我们可以对不同约 束赋以不同的权值( 伽e 匆耽) ，而我们的目标就变为：寻找一组赋值，使其满足所 有的硬约束，并使满足的软约束的权值之和最大这类问题我们称为带权的约 束满足问题( w e i g h t e dc s p ) 本文讨论的m a x s a t 便是一类重要的约束优化 问题，而w e i 曲t e dm a x s a t 是其带权的版本关于约束满足问题和约束优化问 题的形式化定义和更详细的介绍，读者可以参考文献2 ，3 1 另一个相关的，并且在计算机科学和人工智能的知识表示领域常常涉及到 的问题是关于不协调知识库的问题在实际应用中，一个专家系统的的知识库 的知识常常有多种来源这些不同来源的知识可能产生矛盾这样的知识库我 们称之为不协调知识库例如，在一个知识库中，同时存在三条知识：“所有鸟都 会飞”，“企鹅是鸟”和“企鹅不会飞”；这三条知识不可能同时成立，于是便构 成了一个不协调的知识库在传统的逻辑框架下，对不协调知识库的所有命题 查询都将得到肯定的结论这是因为在命题逻辑中，一旦前提为假，那所有的结 论都为真在这种情况下，知识库中所有的知识将变得毫无意义解决这一问题 的一个自然的做法是删除一些知识，以保证知识库中的知识保持协调，并且使 得保留的知识尽可能多例如，在上面所举的例子中，我们可以删除三条知识中 的任一条，以保证知识库的协调知识库的维护也是m a x s a t 问题的一个应用 背景 第一章引言3 1 2s a t 和m a x - s a t 问题 s a t 问题是c s p 问题的一个特例。它是第一个被证明为n p 完备的问题f 4 1 由于具有重要的理论意义，几十年来，s a t 问题一直是理论计算机学界关注和 研究的热点问题另一方面，由于包括电路自动设计f 5 1 、智能规划f 6 1 、模型检 测 7 、协议验证 8 、密码分析 9 和生物信息学 1 0 】等诸多领域的实际问题可以自 然地转化为s a t 问题，设计和开发高效的s a t 求解工具也成为近二十年来许多 学术团体的研究热点 由于近二十年来广泛而深入的研究，s a t 领域也日趋成熟，对s a t 求解器 效率的大幅改进已经越来越难另一方面，人们也发现，对于很多问题，如最优 化问题，计数问题，概率推理问题等，s a t 无法直接应用其中学者们开始将目 光投向比s a t 更一般的问题，如q b f ，m o d e ic o u n t i n g ，m a x - s a t 等，这些问题 都可以看作s a t 问题很自然的扩展，而且由于它们更一般，因而应用的范围也 更广 本文关注的问题是m a x s a t 问题m 躲s a t 问题在电路设计1 1 1 与调试f 1 2 1 ， 生物信息学 1 3 ，统计物理 1 4 ，概率推理 1 5 ，智能规划与调度f 1 6 ，17 1 等领域 都有相关的应用图论中的最大团和最大割问题也可以很自然地转化为m a x s a t 问题因此，近五年来，我们看到了m a x s a t 的求解计数获得了迅速的 发展，当今的m a 治s a t 求解工具和五年前相比，效率上提高了好几个数量级 从0 6 年开始，每年举行的m a x s a t 评估比赛见证并且推动了m a x s a t 求解技术 的发展 求解m a x s a t 问题的算法可以分为完备算法和不完备算法完备算法可以 保证在算法结束时得到问题的最优解，不完备算法则往往只能得到近似解本 文主要研究m a x s a t 的完备算法 m a x s a t 完备算法中采用的技术大体上可以分为搜索和推理两部分这两 部分往往可以相互结合 m a x s a t 的搜索通常都是基于分支定界算法的因而，m a x s a t 求解中的 搜索技术往往关注如何快速有效地组织搜索，这方面关注的问题，如变量的选 择策略，值的选择策略，如何进行l o o ka h e a d ，如何进行回溯或回跳等，而重中 之重是如何计算下界，下界的计算由于和剪枝的效果密切相关，因而在分支定 界算法中扮演着极为重要的角色 m a x - s a t 的推理类似于s a t 中的c l a u s el e a r n i n g 技术，它关心的是如何从原 4m a x s a t 求解中的搜索和推理 有的子句中推导出更多的信息，从而让问题中隐含的约束显性化，以帮助我们 尽快的缩减搜索的空间 s a t 和m a x s a t 的定义以及m a x - s a t 的主要算法将在第2 章介绍 1 3论文的主要贡献和章节安排 本文的贡献主要在m a x s a t 的推理和搜索这两个方面下一章将简要介 绍m 躲s a t 的基本知识和当前的主要算法和工具 在m a x s a t 的推理方面，本文提出一个更一般的逻辑框架，在这一框架 中，给出了m a x s a t 语境下的公式蕴含，等价和a 一等价的定义本文还给出了几 个人一等价规则的例子，证明了它们的正确性作为推理规则应用的例子，本文运 用已有的推理规则改进了前人关于m a x s a t 问题的一个下界函数这部分内容 见第3 章 在m a x s a t 的搜索方面，本文分析了前人计算下界方法的不足，提出了基 于学习的下界计算方法这一方法分为“向父亲学习”和“向过去学习”两部分 通过学习，本文的计算方法不仅避免了重复的计算，而且保证了下界的递增这 部分内容见第4 章 第5 章是给出w c i g h t e dm 躲s a t 求解器的实现这一章介绍了如何将 前面章节中的一些算法扩展到带权的公式中这一章还给出了l b s a t 参 加0 7 年m a x s a t 评比的结果以及i n c m a 瑚a t z 和i n c w m a 潲a t z 参加0 8 年评比的结 果 第6 章是对m a x s a t 算法的理论分析在这一章中，我们改进了m 躲s a t 以 及m a x c u t 的算法在最坏情况下的时间复杂度上界 最后一章是结论和展望 第二章m a x s a t 的算法 本章介绍当前求解m 躲s a t 的主要算法，其中的分支定界算法是本文所提 出的改进算法的基本框架2 1 节介绍相关的基本概念和一系列与m 觚- s a t 有关 的问题2 2 节介绍分支定界算法 2 1基本概念 在命题逻辑中，一个变量可以取值为真( 也用1 表示) 或为假( 也用。表示) 真和假也是命题逻辑中仅有的两个常量 常量和变量之间的运算符包括一元运算符非，( 本文为表示方便，对变量的 非也常用在变量名上加上划线表示如变量z 的非，z 也常写作孟) ，二元运算符 析取v ，合取八等其中，牙为真，当且仅当z 为假；zv 为真，当且仅当z 和可至 少有一个为真；z 爹为真，当且仅当z 和爹都为真显然，对于任意变量z ，我们 有i = z ，ovz ：z ，1vz = 1 ，0az = 0 和1 八z = z 成立 文字是变量或变量的非文字f 中的变量我们用记号u n r ( z ) 表示子句是0 到 有限多个文字的析取不失一般性，本文规定同一个变量不能在一个子句中出 现多次只包含1 个文字的子句我们称为单元子句包含0 个文字的子句称为空 子句，空子句是永假的子句c 的长度是指c 中包含文字的数目，用l c l 表示一 个带权子句是一个有序对( e 叫) ，其中c 是一个子句，而伽是一个数值，代表该 子句的权重不失一般性，本文规定权重彬是非负的整数 m a x s a t 问题的每个实例是一个c n f ( c o n j u n t i v en o r m a lf o r m ，合取范 式) 公式一个c 凇式是0 到有限个子句的合取由于合取运算满足交换律 和结合律，因而我们也常常将一个c n f 公式看作一个子句集包含0 个子句 的c n f 公式称为空公式，空公式是永真的类似地，一个带权c n f 公式是一个 带权子句的集合一个带界公式是一个有序对只七，其中f 是一个带权c n f 公 式，南是一个非负整数在下一章的逻辑框架中，我们可以看到野实际上代表了不 可满足子旬个数的上界如无特殊声明，本文提到的公式都是指c n f 公式，带 权公式都是指带权c n f 公式 对于一个( 带权) 公式f ，f 的一个赋值是变量集x 到集合 0 ，1 上的一个 6m j 吼s a t 求解中的搜索和推理 映射如果我们规定了x 中变量的顺序，那么赋值也可以用n 元向量文表示， 其中，文f 0 ，1 ) n ，n 是x 中变量的总数t ( z ) 也表示作文( z ) 对于赋值文，如 果我们将公式f 中包含的所有变量的集合记作y ，当y 是x 的子集时，我们称 赋值灾是完备赋值，否则称为部分赋值对于赋值戈及文字f ，令z = u a 7 “) ， 当2 = z 时，叉满足2 当且仅当叉( z ) = 1 ；当2 = 牙时，戈满足2 当且仅当文( z ) = 0 赋值灾满足子句c ，当且仅当戈满足c 中的至少一个文字空子句记作口，它不能 被任何赋值满足赋值灾满足公式f ，当且仅当戈满足f 中的所有子旬如果一 个公式可以被一个完备赋值满足，我们称这个公式为可满足公式；否则，称为不 可满足公式或矛盾公式有时为了方便起见，我们也将赋值文表示为其中取值 为真的文字的集合例如x = z 1 ，z 2 ，z 3 ) ，灾( z ，) = 1 ，文( z ：) = 0 ，又( z 3 ) = 1 ， 则文也表示为文字集合( z ，而，z 3 ) 对于公式f ，我们记其中出现的所有变量 的集合为y a 兄( f ) 同样地，对于文字集合l ，我们记y a r ( l ) = z i 存在z l 使得 o r ( f ) = z ) f f 表示令公式中的文字2 为真根据命题逻辑运算的性质，f f 1 意味着 删去f 中的r 以及包含f 的子句在一些文献中，也将这一处理过程称为对公 式f 应用单文字规则( o n e - l i t e r a l r u l e ) 例如，f = ( zv 可) 八( 牙vz ) 八( 雪八牙) ， 则f 吲= ( 可) 八( 雪八互) 设l = f 1 ，f 2 ，k ，f f 1 f 2 】 1 。 也记作f 纠 s a t 问题是指对给出的一个公式f ，判断是否存在一个完备赋值使其满 足f 中所有的子句如果给出的公式f 的子句长度都不大于乃，我们将其称之 为七一s a t 问题 m a x - s a t 问题是指对给出的一个公式f ，寻找一个完备赋值使其满足f 中 最多的子句，或者换句话说，寻找一个完备赋值使得f 中不被满足的子句 数目最少同样，如果给出的公式f 的子句长度都不大于南，我们将其称之 为m a x 一七一s a t 问题 w b i g h t e dm 躲s a t 问题是指对给出的一个带权公式f ，寻找一个完备赋值 使其满足的子句的权重之和最大，或者换句话说，寻找一个完备赋值使得f 中 不被满足的子句权重之和最小 p a r t i a lm a x s a t 问题是m 觚- s a t 的一个扩展给出一个公式f ，f 中的子 句分为硬子句和软子句，p a r t i a lm a x s a t 问题的目标是要找到一个赋值，使其 在满足所有硬子句的前提下满足最多的软字句 类似地，我们可以定义w b i g h t e dp a r t i a lm 觚- s a t 问题：给出一个带权公 第二章m a x - s a t 的算法 7 式f ，f 中的子句分为硬子句和带权软子句，p a r t i a lm a x s a t 问题的目标是要 找到一个赋值，使其在满足所有硬子句的前提下，满足的软字句的权重之和最 大 显然，s a t 问题可以多项式图灵归约到m a x - s a t 问题，由于s a t 问题 是n p 完备的，所以m a x - s a t 问题是n p 一难的事实上，m a x s a t 要比s a t 难很 多这方面的一个例证是2 一s a t 是p 问题f 1 8 1 ，但m a x 一2 一s a t 却是n p - h a r d 的 1 9 1 m a x s a t 问题的难度还体现在它的难近似性上 2 0 】对计算复杂性感兴趣的读 者可以参考上述文献 对于w e i g h t e dm a 静s a t 而言，由于m a x s a t 是、e i g h t e dm a 静s a t 问题在 所有子旬权重都为l 时的特例，所以w e i g h t e dm a x _ s a t 也是n p 一难的另一方 面，如果我们将带权公式的每个带权子句( c ，伽) 看作叫个不带权的子句c ，那 么w a i g h t e dm a 补s a t 也可以看作是一般的m a x s a t 问题 对于p a r t i a lm a x s a t 而言，由于m a x s a t 可以看作是p a r t i a lm a * s a t 在 所有子句都是软子句时的特例，所以p a r t i a lm a x s a t 比m a x s a t 更一般，因而 也是n p 一难的对于w b i g h t e dp a r t i a lm a x s a t 问题我们也可以通过类似的分析 得知它是n p 一难的另一方面，如果我们对( w e i g h t e d ) p a r t i a lm a * s a t 的( 带 权) 硬子句赋以比所有( 带权) 软子句的数目( 权重之和) 更大的权重，那么它 也转化为w 6 i g h t e dm a x s a t 问题 在不至于引起混淆的情况下，本文常用m a x s a t 统称上述问题 m i n i c o s t s a t ( m i n i m u mc o s ts a t i s f i a b i l i t vp r o b l e m ，最小费用满足问题) 是w b i g h t e dp a r t i a lm a x s a t 问题的一个特例问题的定义如下：给出一个 公式f ，f 中含有礼个变量z 1 ，z 2 ，z 。，每个变量翰对应一个花费龟，g 是非负 整数，m i n i c o s t s a t 的目标是找到一个赋值又【0 ，1 】“满足f ，并且使得总花 费c = ：，q 甄最小 在m i n i c o s t s a t 问题中，只要我们将公式f 中的子句作为硬子句，再对于每 个变量z ；及其花费c i 加入带权软子句( 最，q ) ，便可将其转化为一个w 6 i 曲t e dp a r - t i a lm a x - s a t 问题的实例m i n i c o s t s a t 在自动测试图形向量生成( a u t o m a t i c t e s tp a t t e r ng e n e r a t i o n ，a t p g ) ，f p g a 路由( f p g ar o u t i n g ) 等方面有着 很直接的应用，这也是m a x s a t 求解工具的开发日益受到重视的一个原因 对m i n i c o s t s a t 问题专门算法及其应用的研究可参见文献f 2 1 1 s o f t s a t 是m a x - s a t 的另一个扩展s o f c s a t 问题中，公式f 的子句被分 8m a x - s a t 求解中的搜索和推理 成七个不相交的子公式日，b ，r ，使得f = f 1u 马u u 凡，每个子公 式e 对应一个权重叫t ，s o f 一s a t 的目标是找到f 的一个完备赋值，使得被满足的 子公式的权重之和最大类似地，我们也可以将子公式分为硬子公式和软子公 式提出s o f t s a t 问题的一个原因是在实际应用中，我们发现许多约束优化问 题在转化为m 躲s a t 实例时，一个实际问题中的约束往往需要用多个子句( 一 个子公式) 来表示，那么原约束的权重也就理应对应一个子公式而不是一个子 句的权重关于s o f t s a t 问题专门算法的研究可参见文献 2 2 1 和 2 3 由于m 册s a t 的诸多实际应用，近年来，设计高效的m a x s a t 求解算法和 开发相应的求解工具成为人工智能领域研究的一个热点事实上，当前的m a x s a t 求解工具和五年前相比，其效率提高了几百乃至上千倍m 觚一s a t 的求解 算法可以分为完备算法和不完备算法所谓完备算法，是指一旦程序终止，能够 保证得到最优解的算法而如果算法在终止时，可能求得最优解，也可能只能得 到一个近似解，我们将之称为不完备算法基于不完备算法的求解工具往往比 基于完备算法的工具的运行时问要快很多局部搜索( l o c a ls e a r c h ) 算法是最 主要的一类不完备算法，但由于m a x s a t 的局部搜索算法和s a t 的局部搜索算 法没有很实质的差别，所以当前对m a x s a t 的算法研究主要集中于完备算法 m a x s a t 最主要的完备算法是分支定界( b r a n c ha n db o u n d ，b n b ) 算法， 本文的算法也是基于分支定界算法当前大多数的m a x s a t 求解工具也是基于 这一算法下一节将简要回顾这些工具及其算法 2 2m a x s a t 的主要算法和工具 当前主流的m a x _ s a t 求解工具，如t o o l b a r 2 4 ，2 5 ，2 6 1 ，m i n i m a x s a t 2 7 ， 2 8 1 ，u p f 2 9 1 ，l a z y 3 0 1 ，m a x s a t z 3 1 ，3 2 1 ，p m s 3 3 1 和m a 潲a t z l 4 i c s s f 3 4 1 等都基于 分支定界的算法框架 对于输入的个c n f 公式( 也称为实例) f ，分支定界算法是以深度优先 搜索( d e p t h 一丘r s ts e a r c h ) 的方式遍历所有可能的赋值空间，或者说遍历这些可 能赋值构成的搜索树( 二叉树) 在搜索树中，每个巾间结点代表对f 的个部 分赋值；每个叶结点代表对f 的一个完备赋值在每个结点，算法计算结点的下 界三b 所谓下界是指对将当前结点所代表的部分赋值扩展为完备赋值后不被完 备赋值所满足的子句的最少数目的一个保守估计这一保守估计值不能大于实 际不可满足子句的最少数目( 满足这一条件时，我们称求得的下界是安全的) ， 第二章m a x - s a t 的算法9 否则算法就可能找不到最优解同样，这一估计值也不能比实际不可满足子句 的最少数目小太多，否则算法就不能有效地剪枝( 剪去搜索树上那些不可能存 在最优解的分支) ，算法的效率就会很低求得下界己召之后，我们将l b 和当前 结点的上界v b 比较所谓上界是指目前搜索过的完备赋值所不满足的子句数 目的最小值，也就是当前结点为止，所找到的最优解那么，如果l b u b ，那 么意味着扩展当前结点所代表的部分赋值是不