（计算机软件与理论专业论文）命题可满足性问题（sat）的局部搜索算法研究与改进.pdf

命题可满足性问题( s a t ) 的局部搜索算法研究与改进 专业：计算机软件与理论 硕士生：龙胜 指导教师：苏开乐教授 摘要 命题可满足性问题( s a t ) 是判定一个给定的c n f 形式的命题逻辑公式是否 存在可满足的赋值的问题。s a t 问题是数理逻辑、人工智能和理论计算机科学 中的核心问题，也是解决许多实际问题的基础。因此研究和改进s a t 问题的求 解算法不仅具有重大的理论意义，而且应用前景广阔。对于某些类型的s a t 问 题，局部搜索算法比一些完备搜索算法更为有效。 通过对现有s a t 局部搜索算法的研究，本文发现这些算法使用的前看一步 策略存在贪心程度不够的问题。为了加强s a t 局部搜索的贪心程度、减少翻转 次数从而提高算法的求解能力，本文在前看一步策略的基础上提出了一种改进策 略前看两步策略对算法中翻转变量的选取方法进行改进。前看一步策略 和前看两步策略共同组成了本文的前看两次策略。将前看两步策略应用于 w a l k s a t 算法类中的w s a t 、t s a t 和n o v e n y 对它们进行改进，产生了三组新 的算法变体w s a ta t 、t s a ta t 和n o v e l t ya t 。然后程序实现了这些改进算 法。为了验证前看两步策略对现有算法的改进效果，本文在多个不同规模的均衡 3 s a t 实例、两种不同规模的结构s a t 问题实例以及几个利用相变现象构造的 难解s a t 实例上进行了实验。实验结果表明：改进后的算法的求解能力和收敛 速度不同程度地优于对应的现有算法。 由于本文提出的前看两步策略不是和w a l k s a t 算法很相关，所以该策略也 可以用于对其它s a t 局部搜索算法的改进，并对其它领域的局部搜索算法的改 进具有一定的参考价值。 关键词：可满足性问题( s a t ) ，局部搜索，前看两步策略 中山大学硕士学位论文 命题可满足性问题( s a d 的局部搜索算法研究与改进 r e s e a r c ha n di i n p r o v e m e mo nl o c a ls e a r c ha l g o r i t s f o rt h ep r o p o s i t o n a ls a t i s f i a b i l i t yp r o b l e m ( s a t ) m 萄o r ： c o i n p u t e rs o 舢y a r ea n dt h e o 巧 n a m e ： s h e n gl o n g s u p e r v i s o r ： p r o f e s s o rk a i l es u a b s t r a c t t h ep r o p o s i t o n a ls a t i s f i a b i l i 够p r o b l e m ( s a t ) i sm et a s kt od e d d e 南ra 百v e n p r o p o s i t o n a lf o m u l ai nc o n j u l l c t i v e - n o m a lf o m( c n f )w h e t h e rt h e r ei s a i l a s s i g 呦e n tt oi t sv a d a b l e st h a ts a t i s f i e st h ef o 舯u l a s a ti sac e n t r a lp r o b l 锄i nl o 沓c ， a r t i 矗c a li n t e l l i g e 置1 c e ，m e o r e t i c a lc o m p u t e rs c i e n c ea n dm a n ya _ p p l i c a t i o n s t h e r e f o r e ， i t sv e r yi m p o r t 觚tt or e s e a r c ha n di 珈【p r o v es a ta l g o r i t l l i i l sb o mi nt h e o r ya i l di n p r a c t i c e r e c e n t l y ，i tw a ss h o w nm a t1 0 c a ls e a r c ha l g o r i t h n l sc a l lo u t p e r f o n nm a i l y s y s t e m a t i cs e a r c _ ha l g o r i t h m so ns o n l el a 疆r ec l a s s e so fs a t p r o b l e m s i nt h i st 1 1 e s i s ，l o c a ls e a r c ha l g o r i t h m sf o rs a ta r cr e s e a r c h e df i r s t l y a j c t e r r e s e a r c m n gs o m ee x i s t i n gs a t1 0 c a ls e a r c ha l g o r i t h m s ，w ef i n dt 1 1 a tm es t r a t e 酉e s u s e di nt l l e s ea l g o r i t l l i n sa r el o o k a h e a d - o n e s t e pa n dt h u sh a v es o m ep r o b l e m s i n o r d e rt os t r e l l 垂h e l lm e 伊e e d yd e 笋e eo f1 0 c a ls e a r c h ，d e c r e a s et h en u m b e ro f n i p p i n g 向rf i n d i n gas o l u t i o n ，a i l di m p r o v es e a r c h i n gs 0 1 u t i o na b l i t yo fa l g o r i 如 i l s ，w e p r o p o s ean e wa l g o r i t l l m i cs 仃a t e g y c a l l e dl o o k a h e a d t w o s t e p st oi m p r o v e 廿l e m e t h o dh o wt os e l e c tav a r i a b l et 0n i pi ns a t1 0 c a ls e a r c h t l l el o o k a h e a d - t w i c e s 仃a t e g yp r c p o s e di nt h j st h e s i si sc o m p o s e do fl o o k a h e a d - o n e s t 印s t r a t e g ya 1 1 d l o o k - a h e a d - t w o s t e p ss 仃a t e g y w eg o tt h r e e 目o u p so fn e wa l g o r i t l l i n sb a s e do n w a l k s a tb ya p p l y i n gt h ep m p o s e ds 仃a t e g ) ，o nt h r e ei m p o r t a l l tc u r r e n tl o c a ls e a r c h a l g o r i m m s ，i e w s a t ，t s a t ，a i l dn o v e l t y f u r t h 锄o r e ，w ei i n p l e m e n ts u c h i m p r 0 v e da l g o r i t h m s 1 1 1o r d e rt oc 0 m p a r em e s en e wa l g o r i m m sw i mt h ea c c o r d m 酉y e x i s t i l l go n e s ，m 姐yu n i f o n n3 s a tp f o b l e mi i l s t a n c e s ，s 咖c t u r e ds a tp r o b l e m i i l i n s t a l l c e sa 1 1 dp h a s et r a i l s i t i o n ss a tp r o b l 锄i n s t a l l c e sa r et e s t e d t h ea c t i l a l c x p 舐m e i l tr e s u l t si n d i c a t et h a tm ei m p r o v e da l g o r i so u t p e r f - o 珊n l ec 1 盯e 1 1 tl o c a l s e a r c hs a ts o l v e r sb o t ho ns e a r c h i n gs o l u t i o na b l i t ya 1 1 dc o n v 哪e n ts p e e d c o n s i d e r i n gt h el o o k - a h e a d - r w o s t 印ss t r a t e g ) ri sn o td 印e n d e n to nw a l k s a t a l g o r i t h m s ，i tc a na l s ob ea p p l i e dt oo t t l e rs a tl o c a ls e a r c ha l g o r i t h m st oi m p r o v e t h e i ra b l i t ya 1 1 de 伍c i e l l c y k e y w o r d s ：s a t i s f i a b i l i t yp r o b l e m ( s a t ) ，l o c a ls e a r c h ，l o o k - a h e a d - t w o s t 印s 论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研究 工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人 或集体已经发表或撰写过的作品成果。对本文的研究作出重要贡献的个人和集 体，均已在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。 学位论文作者签名：龙驻 日期：砌矛年万月莎日 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规定，即：学校有权保留 学位论文并向国家主管部门或其指定机构送交论文的电子版和纸质版，有权将学 位论文用于非赢利目的的少量复制并允许论文进入学校图书馆、院系资料室被查 阅，有权将学位论文的内容编入有关数据库进行检索，可以采用复印、缩印或其 他方法保存学位论文。保密的学位论文在解密后使用本规定。 学位论文作者签名：龙胜导师签名：易季 日期：翮年歹月8 日日期：7 扩嘭年乡月参旧 中山大学硕士学位论文命题可满足性问题( s a d 的局部搜索算法研究与改进 1 1 研究背景与现状 第1 章绪论 命题逻辑【1 翻中合取范式( c n f ) 的可满足性问题( s a t ) 是计算机科学理论与应 用的核心问题，是解决人工智能和计算理论中许多实际问题的基础。s a t 问题 是一个典型的n p 完全问题【3 1 ，研究其快速、有效的求解算法不仅具有重大的理 论意义，而且在智能规划4 ，5 1 、演绎推理【6 1 、电路综合7 1 和模型检测等诸多领域都 有很大的应用价值。 考虑一个c n f 形式的命题逻辑公式，它是一些子句的合取，每个子旬是一 些文字的析取，而每个文字是一个命题变量或者命题变量的非。s a t 问题就是 判定这个给定的c n f 公式是否存在可满足的赋值，使公式中所有的子句在通常 的解释下为真。 s a t 问题的研究主要分为两个大的方面：一是理论研究，二是研究高效求 解器( s l o v 砷的实现，即对s a t 算法的改进与实现。 s a t 问题由c o o k 在1 9 7 1 年证明为第一个n p 完全问题【8 】。国内外多篇论文 对s a t 问题的难度分布9 1 、相变现象1 0 ，1 1 ，1 2 1 以及如何产生s a t 问题实例的方法 【1 3 ，1 4 】进行了深入的研究。k a u t z 和s e l m a l l 分别于1 9 9 7 年和2 0 0 3 年先后两次列举 了s a t 搜索面临的十大挑战性问题【1 5 ，1 6 1 并于2 0 0 1 年和2 0 0 5 年对s a t 研究现状 进行了全面的综述【1 7 ，18 1 。 s a ts l o v e r 的实现是s a t 研究的主流，其中s a t 算法又分为完备算法和不 完备算法两大类。 s a t 问题的完备算法比不完备算法出现得更早。d a v i s 和p u t i l 锄于1 9 6 0 年 提出的d p l l 算法【1 9 ，2 0 1 是最著名的完备算法之一，后来完备算法的研究与发展大 都是基于d p l l 算法的。完备算法的优点是理论上保证能正确地判断s a t 问题 的可满足性，即要么能够求出问题实例的所有的解，要么能在问题实例无解的情 况下给出一个完备的证明。但是，由于s a t 问题是一个n p 完全问题，所以必 须提高完备算法的效率才能有效地解决s a t 问题。近年来提出了多种启发策略， 中山人学颂：f ：学位论文 命题可满足性问题( s a d 的局部搜索算法研究与改进 使得完备算法的效率得到了很大的提高，并涌现出了一批高效的s a t 完备 s o l v e r ，其中z c h a f j f 类算法【2 1 】代表了完备算法的最高性能水平。 不完备算法主要是局部搜索( l o c a ls e a r c h ) 算法。基本的局部搜索算法是在二 十世纪六、七十年代求解组合优化问题时发展起来的，它是解决很多n p 难问题 的一种常用方法。虽然局部搜索算法在运筹学界一直很活跃，但是它直到九十年 代才应用于人工智能界。 1 9 9 0 年，m i n t o n 【2 2 1 将皇后问题转化成优化问题，得到了比传统的回溯搜索 算法好很多的求解结果。 1 9 9 2 年开始，顾钧提出了一系列求解s a t 问题的局部搜索算法2 3 ，2 4 1 ，有人 认为，顾钧最早将局部搜索算法用于s a t 。 1 9 9 2 年s e l m a l l 等人提出的g s a t 算法【2 5 】有力地证明了局部搜索算法可以用 来解决有挑战的s a t 问题，并成为s a t 局部搜索算法的基础。从此，s a t 局部 搜索算法得到了广泛而深入的研究【2 6 4 5 1 。 1 9 9 4 年s e l m a l l 又把随机行走策略引入局部搜索，产生了著名的w a l k s a t 算 法【2 8 1 。随后，人们在w a l k s a t 算法框架下加入或提出了多种算法改进策略，产生 了多个w a l k s a t 算法变体，它们共同组成了w a l k s a t 算法类。 局部搜索算法虽然不能保证一定能找到解，但是其求解速度快，实用性高。 对于某些类型的s a t 问题，局部搜索算法要比d p l l 等完备算法更为有效。 近年来，在高效的局部搜索算法的开发上取得了重大的进步，研究成果也很 丰富，其中具有代表性的是n o v e l t y ，i l n o v e l t y 【3 0 1 ，n o v e l t y + ，r - n o v e l t y + 【3 5 】， s d f 【3 6 1 和s a p s 跚等。国内在这方面的研究成果也很突出，黄文刮3 2 1 提出了并行 的s o l a r 算法，该算法在北京第三届s a t 问题快速算法国际比赛中获得了第一名， 李未描述了求解s a t 问题的数学物理方法，梁东刨3 4 】对w s a t 进行了子句加 权改进，张德富利用人类日常生活中解决问题的一些技巧实现了拟人退火算 法，杨晋吉【钢提出用初始概率的方法对局部搜索算法进行改进等。 1 2 研究思路和主要工作 鉴于s a t 问题在人工智能和计算理论方面的基础地位和广阔的应用前景以 及局部搜索算法的高效实用，本文对s a t 问题的局部搜索算法进行研究与改进。 2 中山大学硕士学位论文 命题可满足性问题( s a d 的局部搜索算法研究与改进 本文首先介绍了s a t 问题及其求解算法的相关知识，包括s a t 问题的定义、 类型、相变现象和问题难度，局部搜索算法以及s a t 问题的两类求解算法：完 备算法和不完备算法等。然后对现有s a t 局部搜索算法进行了研究。在分析和 总结了s a t 局部搜索算法的一般结构和基本概念之后，介绍并分析了两类s a t 局部搜索算法：g s a t 算法类和w a l k s a t 算法类。 研究发现s a t 局部搜索算法在选取变量进行翻转时使用的前看启发策略即 变量排序策吲4 3 】都是前看一步( 次) 策略因此存在贪心程度不够的问题。为了 加强s a t 局部搜索的贪心程度、加快算法收敛速度从而提高算法的求解能力， 本文提出了前看两步策略( l o o k a h e a d t w o s t 印s ) 和前看两次策略 ( l o o k - a h e a d t w i c e ) 对现有s a t 局部搜索算法的变量选择策略进行改进在 前看一步策略的基础上( 第一次前看) ，增加第二次前看( 使用前看两步策略) ， 形成前看两次策略。 前看两次策略可以简单描述为：第一次前看按照前看一步策略从当前考虑的 变量中选取若干个候选变量；然后第二次前看按照前看两步策略从这些候选变量 中选出最终的翻转变量。 本文先提出了和前看两步密切相关的几个新概念：两个变量的“同时产生数” ( m a l ( e s i m u l t c o u n t ) 和“共同破坏数”( b r e a k t o g e t h e r c o u n t ) ，即两个变量的“同时产 生子句”和“共同破坏子句 的数量；两个变量的“联合产生数”( m a k e u l l i o n c o u n t ) 和“联合破坏数”( b r e a l ( u 1 1 i o n c o u n t ) ，即两个变量的“联合产生子句”和“联合 破坏子句”的数量，并给出了它们的计算方法。然后在它们的基础上定义了前看 两步策略中需要使用的两个变量的联合效益函数( s c o r e u 血o n ) 和单个变量的预期 效益函数( s c o r e 肌u r e ) ，其中每个变量的预期效益值的大小将作为前看两步中选 取变量的标准，预期效益值利用多个联合效益值( 第一个变量对应的第二个变量 有多个) 按一定的计算方式( 使用某个计算函数) 计算出来。 联合效益函数与预期效益函数的计算方式的不同组合对应了不同的预期效 益函数。考虑到现有局部搜索算法的前看一步策略中使用的单个变量的效益函数 ( s c o r e ) 的定义方式主要只有2 种，本文选取和这2 种效益函数对应的2 种联合效 益函数( s c o 舢l i o n b 和s c o r e u n i o n i b ) 供改进策略使用。关于预期效益函数的计算方 式，本文考虑了3 种与优化计算、贪心策略密切相关且常用的计算函数：求最小 3 中山大学硕j ：学位论文命题可满足性问题( s a d 的局部搜索算法研究与改进 值函数( m i n ) 、求最大值函数( m a x ) 和求平均值函数( a v 曲。我们从预期效益函数 的6 种可能的组合中选取3 个适合于改进前看一次策略的预期效益函数并产生了 对应的3 个具体的前看两步策略版本( a t l ，a t 2 和a t 3 ) 。 然后本文将3 个具体的前看两步策略应用于w a l k s a t 类算法以实现对该类 算法的改进，在3 个典型的w a l k s a t 类算法w s a t ，t s a t 和n o v e l t y 的基础 上应用前看两步策略得到了3 组( 共8 个) 具体的前看两次策略( b e s t - a t ，t a b u - a t 和n o v e l t ya t ) 及其对应的3 组新的w a l k s a t 算法变体( w s a ta t 、t s a ta t 和 n o v e l t l a t ) 。 然后在w a l k s a t 程序框架下新增了相应的数据结构并程序实现了改进后的 算法变体，扩展了w a l k s a t 程序系统。 最后，为了比较改进算法与其基于的现有算法的表现和性能、验证提出的前 看两步( 次) 策略对现有算法的改进效果，本文对3 组改进前后的算法分别进行 了对比实验，并对实验结果进行了分析。 在多个不同规模和难度的均衡3 s a t 问题实例、两种不同规模的结构s a t 问题实例以及多个利用相变现象构造的难解s a t 实例上的实验结果表明：前看 两步策略对3 个现有算法t s a t ，w s a t 和n o v e l t y 总体上都有一定程度的改进 提高了求解成功率，减少了翻转次数，即改进后的算法具有更强的求解能力 和更快的收敛速度。 由于本文提出的前看两步策略不是和w a l k s a t 算法很相关并且是领域无关 的【2 6 4 5 ，4 6 1 ，所以该策略也可以用于对其它s a t 局部搜索算法的改进，并对其它 领域的局部搜索算法的改进具有一定的参考价值。 1 3 论文的组织结构 本文的组织结构安排如下： 第一章绪论，首先介绍了本文研究的背景和s a t 局部搜索算法研究的现 状，然后介绍了本文研究的思路和主要工作。 第二章s a t 问题及其求解算法相关知识，首先介绍了s a t 问题的表示、类 型、相变现象和问题难度。然后介绍了与s a t 问题相关的两种问题约束满 足问题和组合优化问题。接着介绍了局部搜索算法的基本概念和思想。然后对 4 中山大学硕士学位论文命题可满足性问题( s a d 的局部搜索算法研究j 改进 s a t 算法进行了简单的分类介绍。最后介绍了用于测试s a t 算法的基准实例。 第三章s a t 局部搜索算法研究，首先对现有s a t 局部搜索算法的一般结构 和基本概念进行了分析和总结，给出些基本的结论。然后介绍并分析了两类主 要的s a t 局部搜索算法：g s a t 算法类和w a l k s a t 算法类。 第四章算法改进与实现，这一章是本文的重点，首先针对现有算法使用的 前看一步( 次) 策略存在的问题和可以改进的地方，提出了本文的算法改进策略 前看两次策略和前看两步策略并简单描述了它们的基本思想。然后对前看两 步策略进行了详细的描述并得出几个具体的前看两步策略。接着介绍了基于 w a 】k s a t 体系的策略应用与算法改进，即如何将前看两步策略应用于w a l k s a t 类算法实现对该类算法的改进。最后我们介绍了如何在w a l k s a t 程序框架下实 现这些改进后的算法变体，包括数据结构、程序流程和改进策略的实现。 第五章实验结果与分析，在这一章中，我们通过实验分析的方法对改进算 法的性能进行评价，验证提出策略的改进效果。首先介绍了s a t 算法的评价标 准和本文的实验方案。接着介绍了实验系统以及选用的测试实例。然后对三组算 法变体( w s a ta t 组，t s a ta t 组和n o v e l t ya t 组) 的相关实验结果分别进 行了分析，得出了评价改进策略和算法的一些结论。 5 中山大学硕士学位论文 命题可满足性问题( s a d 的局部搜索算法研究与改进 第2 章s a t 问题及其求解算法相关知识 2 1s a t 问题 2 1 1s a t 问题的定义 s a t 问题( p r o p o s i t i o n a ls a t i s f i a b i l i t yp r o b l 锄) 是判定一个给定的命题逻辑公 式( c n f 形式) 是否存在可满足的赋值( 模型) 的问题，相关定义如下： 设v = v l ，v 2 ，v n ) 表示一个命题变量的集合，用i v i 表示v 的元素个数。 定义2 1 真值赋值 关于v 的真值赋值是一个函数：v 专 t ，f ) 。如果矽( v ) = t ，称v 在赋值下 取真值；如果( v ) = f ，称v 在赋值下取假值。真值赋值简称赋值。 定义2 2 文字 对任意一个命题变量x ，称符号x 和1 x 是v 上的文字( 1 i t e r a l ) ，其中x 是正 文字，一x 是负文字。 定义2 3 子句 子句( c l a u s e ) 是v 上若干文字的析取，用集合c 表示。即： 给定文字l i ，1 2 ，k ， c = l l v l 2 v v l k( 2 - 1 ) 定义2 4 合取范式 v 上的合取范式是v 上的一些子句的合取，可以用子句集c 表示成这些子 句组成的集合。即： 给定子句c l ，c 2 ，c l l ， c = c 1 a c 2 八a c n( 2 2 ) 定义2 5 可满足的 如果有一个真值赋值，使公式的值为1 ，那么是可满足的( s a t i s f i a b l e ) 。 使它得到满足的这个赋值就是的一个模型( m o d e l ) 。 7 中山大学硕士学位论文命题可满足性问题( s a d 的局部搜索算法研究与改进 定义2 6s a t 问题 给定命题变量的集合v 和v 上的c n f 形式的公式( 用合取范式c 表示) ， 问是否存在一个关于v 的真值赋值矽，使得是可满足的。 2 1 2s a t 问题的类型 s a t 问题的实例是一个c n f 形式的命题逻辑公式，通常根据产生s a t 问题 实例的方式将s a t 问题分为两种类型：随机s a t 问题和结构s a t 问题。随机 s a t 问题实例是用随机模型生成的，结构s a t 问题实例是从现实世界中的一些 n p 完全问题转化即编码( e n c o d e ) 而来的。由于现实世界问题通常是结构化的，所 以结构s a t 问题实例也是有结构( 如规整性，对称性等) 的；而随机s a t 问题 实例是随机生成、独立于任何特殊领域的，所以没有任何结构，从某种意义上说 它们表现了s a t 的“本质”。 1 随机s a t 问题 随机s a t 实例根据规模和求解难度的不同可以划分为：容易的和难的实例。 这些随机实例可由m i t c h e l l 【9 】的固定子句长度模型产生： 设n 是变量数，k 是每个子句中的文字数，l 为子句的个数。每个实例是通 过产生包含k 个文字的l 个随机子句得到的，而这k 个文字通过随机选择k 个 变量并且每个变量是负的概率为5 0 产生的。 这种随机公式的难度取决于n 和l 的比值。其中最难的公式出现的区域是 随机产生的公式有5 0 的概率可被满足。对于3 c n f 公式( k 芦3 ) ，实验表明这种 情况出现在l 4 2 5 n 时，当比值变小时或变大时，问题都变得易解，这就是所 谓的s a t 问题的相变现象。 2 结构s a t 问题 结构s a t 问题实例是通过实验模型将现实世界中的一些n p 完全问题，如 规划调度问题、图着色问题、n 皇后问题等编码转化成s a t 问题而得到的实例。 由于这些实际问题本身是n p 难问题，由此转化的s a t 问题实例有一定的 难度，且具有一些随机s a t 问题实例所不具有的特性，比如子句包含变量数不 相等，一些子句包含另外一些子句，存在独立变量和非独立变量等【4 6 1 。 8 中山大学硕士学位论文 命题可满足性问题( s 蛆) 的局部搜索算法研究与改进 2 1 3s a t 的相变现象和问题难度 相变现象本是物理学中的术语，指复杂的物理系统从一个相到另一个相的突 变现象。s a t 问题中也有一个相变现象，即问题实例的可满足概率随着问题规 模参数的变化而发生突变5 4 1 。 相变现象是s a t 问题的一个重要特性，通过对这一现象进行研究，有助于 进一步认识s a t 问题的性质【1 0 ，1 1 ，12 1 ，从而设计出更为高效的算法。因此相变现 象是s a t 理论研究的重要内容。 下图描述的是3 s a t 问题的相变曲线，横轴代表子句数和变量数的比值。 可满足概率 1 0 0 5 0 0 图2 1s a t 问题的可满足概率相变曲线和难度曲线( 钟形) 由上图可知可满足概率曲线在渊约等于4 2 5 附近发生突变，一般认为相 变点处的可满足概率等于o 5 ，其它k - s a t 同样存在着相交现象。 s a t 问题的难度和s a t 相变现象有关。图2 1 中的钟形实线是难度的示意， 在相变点两侧较远的地方，大部分问题实例都很容易求解，而在相变点附近，所 有的算法都表现出很差的性能，当子句数与变量数之比大约为4 2 5 时，问题实 例非常难求解。并且相变点附近微小的涨落都有可能被放大，看上去微小的算法 技巧的改进也会提高算法的效率【5 4 1 。 9 中山大学硕士学位论文命题町满足性问题( s a d 的局部搜索算法研究与改进 2 2 与s a t 相关的两种问题 2 2 1 约束满足问题 约束满足问题( c s p ) 【2 9 1 是人工智能领域被广泛研究的一类问题，很多实际问 题都可以表示成约束满足问题。 定义2 7 约束满足问题 给定有限个变量以及每个变量的取值范围，要求找出所有变量的值，使得一 些给定的约束条件被满足。 如果每个变量的取值集合都是有限的，则称这样的问题为有限c s p 。 很多具体的问题都可以看成是c s p 的特例，s a t 是有限域c s p 的一个特殊 类型，其中每个变量的取值范围是真假值集合，而满足的约束条件就是给定的命 题逻辑公式【2 9 】。 2 2 2 组合优化问题 现实世界中很多问题属于组合优化问题【4 7 ，5 5 1 ，或者可以转化为组合优化问题 求解，如旅行商问题、n 皇后问题，s a t 问题也是一种特殊的组合优化问题。 定义2 8 优化问题 设x 为决策变量，d 为x 的定义域，坟x ) 是目标函数，甙x ) 是约束条件集合。 则优化问题可以表示为，求解满足g ( x ) 的f 【x ) 最小值问题。即： m 碘( ，( x ) ig ( 石) ) ( 2 3 ) 定义2 9 组合优化问题 如果在d 上，满足条件g ( x ) 的解是有限的，则优化问题称为组合优化问题。 当问题规模较小时，由于组合优化问题的解是有限的，可以通过枚举法获得 问题的最优解。但当问题的规模较大时，其状态数往往呈指数级增长，很难再通 过枚举方法获得问题的解【5 5 】。 1 0 中山大学硕士学位论文 命题可满足性问题( s a d 的局部搜索算法研究与改进 2 3 局部搜索算法 局部搜索( l o c a ls e 抓灿算法是在二十世纪六、七十年代求解组合优化问题时 发展起来的【4 7 ，5 5 1 ，它是解决很多n p 难问题的一种常用方法。本节介绍局部搜索 算法的基本概念和思想。 在组合优化问题中，变量x 的一个取值看作一个点；如果是多变量的问题， 一组变量的一个取值组合可以看作一个点，即一个点就是一个候选解。邻域，简 单地说就是一个点附近的其它点的集合，它的定义如下： 定义2 1 0 邻域和邻居 设d 是闯题的定义域，若存在一个映射n ，使得： n ：s d 专n ( s ) 2 。 ( 2 - 4 ) 则称n ( s ) 为s 的邻域，称s n ( s ) 为s 的邻居。 在整个定义域上的最优解称为全局最优解；在一个邻域内的最优解称为局部 最优解。现实问题中，f 在d 上往往有多个局部的极值点。一般的局部搜索算法 一旦陷入局部极值点，算法就在该点处结束，这时得到的可能不是一个好的结果， 这就是局部最优问题。解决局部最优问题的一般方法是每次并不一定选择邻域内 最优的点，而是依据一定的概率，从邻域内随机选择一个点。 局部搜索算法的基本思想就是：在搜索过程中，始终选择当前点的邻居中离 目标最近者的方向搜索。 2 4s a t 算法的分类 s a t 问题的求解算法可以分为完备算法和不完备算法。 s a t 完备算法大都是基于分枝回溯策略，是对由n 个变量形成的完全二叉 树的遍历过程。回溯搜索算法的基本过程是不断的扩展当前的部分解，如果当前 部分解己经造成矛盾而无法继续扩展，则立即回溯到更短的部分解继续扩展，直 到找到问题实例的一个完整解或是搜索完整棵树。 不完备算法通常是基于局部搜索。s a t 局部搜索算法的基本思想是：先任 意地给每个变量取一个值，得到一个赋值，它可能使一部分子句的值为真，另一 中山大学硕士学位论文 命题町满足性问题( s a d 的局部搜索算法研究与改进 部分子句的值为假，然后反复地对现有的赋值作局部调整，使得被满足的子句个 数朝越来越多的方向发展，直到找到问题实例的一个解或者达到某个设定的约束 条件而结束搜索过程。 总之，完备算法以回溯搜索算法为主导，而在不完备算法中，局部搜索算法 是主流。本文将在第3 章研究s a t 局部搜索算法，所以接下来以经典的回溯搜 索算法d p l l 为代表简单介绍一下s a t 完备算法。 解决s a t 问题的一个著名的完全算法是d a v i s 和p u t n 锄【2 0 】提出的的方法， 被称为d p 算法。后来d a v i s ，l o g e m 锄和l o v e l a i l d 【侈】对它做了进一步的描述， 所以它有时候也被称为d p l l 。d p l l 算法的简单描述如图2 2 所示。 图2 2 d p l l 算法描述 d p l l 算法的执行过程可以用二叉搜索树来表示：每个结点对应着一组子 句，每个分支代表分裂规则，其左右子树分别对应所选文字取假值和真值的情况， 其它边代表其它规则。叶结点有两种：一种为满足结点，对应子句集为空集，表 明问题实例为可满足实例；另一种为失败结点，宣告子句集合中有一个空子句存 在，它表示不可满足。 1 2 中山大学硕士学位论文 命题可满足性问题( s r ) 的局部搜索算法研究与改进 2 5s a t 基准实例 对s a t 算法的测试评价用例大都是公用基准实例( b c l l d l i i l a r k ) ，由s a t 问题 的类型可知，基准实例也有两种类型：随机s a t 实例和结构s a t 实例。 本文进一步将随机s a t 实例分为均衡k s a t 实例( u n i f o mk s a t ) 和相变 s a t 实例。相变s a t 实例是根据s a t 问题的相变现象生成的难解的s a t 实例， 而均衡k s a t 实例不仅有难解的实例，也有易解的实例，即难度分布是均衡的。 结构s a t 实例可以由很多n p 完全问题编码转化而来，常见的有：n 皇后 问题，图着色问题，电路综合诊断问题和积木规划问题等。 最后，介绍一下s a t 基准实例的文件格式，即一个c n f 公式是如何用实例 文件表示的，这有助于理解s a ts l o v e r 如何将一个a 盯公式表达的信息读入内 存以初始化子句、原子和文字等数据结构。 一个s a t 实例文件的内容包括两个部分：注释部分和正文部分。注释部分 描述的主要是变量总数( 轴邳和子句总数( 斧c 1 ) ，还可以包括其它一些辅助信息， 比如对于随机生成的实例，随机种子值( s e e d ) 可以放在注释里面。正文部分描述 的是所有子句包含文字的信息，其中每个子句从左到右指明该子句包含的所有文 字( 变量或变量的非) ，并以o 表示结束。变量标号从l n ，如果是正文字则 记录文字对应的变量标号值，如果是负文字则记录对应变量标号的负值。如果用 一个文件存储这些信息，则正文部分一般每行对应一个子旬。比如某个子旬为 1 x lv x s v 飞7 ，对应的一行记录为15 2 7o 。 2 6 本章小结 本章介绍了s a t 问题及其求解算法相关的知识。首先给出了s a t 问题的定 义，介绍了其类型、相变现象和问题难度。然后介绍了和s a t 问题相关的两种 种问题：约束满足问题和组合优化问题。接着介绍了本文将要研究的局部搜索算 法的基本概念和思想。并对s a t 算法进行了简单的分类介绍。最后介绍了用于 测试s a t 算法的基准实例。 1 3 中山大学硕+ 学位论文命题可满足性问题( s r ) 的局部搜索算法研究与改进 第3 章s a t 局部搜索算法研究 s a t 局部搜索算法作为一种不完备的搜索方法，虽然不能保证一定能找到 s a t 问题的解，但是大多数情况下它们求解速度快，实用性高。对于某些类型 的s a t 问题，局部搜索算法要比完备算法更为高效实用。 自从g s a t 的提出，s a t 局部搜索算法得到了广泛研究，也取得了很大进 展。现有s a t 局部搜索算法主要分为两大类：g s a t 算法类和w a l k s a t 算法类。 3 1 一般结构和基本概念 s a t 局部搜索算法的基本思想是：先任意地给每个变量取一个值，得到一 个赋值。它可能使一部分子句的值为真，另一部分子句的值为假。然后反复地对 现有的赋值进行局部调整，使得被满足的子句个数朝越来越多的方向发展，直到 找到问题实例的一个解或者达到某个设定的约束条件而结束搜索过程。 s a t 局部搜索和标准局部搜索的差别在于：后者探测和当前考虑的解接近 的潜在的一些解；而前者探测和当前赋值只有一个变量不同的赋值的集合。 图3 1s a t 局部搜索算法一般结构 1 5 中山大学硕士学位论文 命题可满足性问题( s a d 的局部搜索算法研究与改进 s a t 局部搜索算法的一般结构如图3 1 所示，具体分析如下： s a t 问题的解是一个关于变量集合v 的真值赋值，它使得s a t 问题实例即 一个c n f 公式中的所有子句同时得到满足( 即为真) 。 图中的每次外循环是一次完整的寻解过程，称为一次“尝试( ”。外循环 最大次数为预先设定的参数m a x t r i e s ，它确定搜索算法在退出前可以重新开 始的次数。 图3 1 中( 1 ) 处的初始赋值是问题的一个可能解，它一般是随机生成的，也有 少数改进策略对它进行了一定的约束和限制，如下文介绍的g s a t 类算法中的 按位平均策略。 图中的每次内循坏是对当前的赋值进行的一次局部调整，称为一次“翻转”。 内循环最大次数为参数f l i p s ，它确定在放弃和重新开始之前算法将尝试 的翻转数目。 对于不同的问题实例，参数m a x f l i p s 和m a x t r i e s 的设置会有一些不 同，粗略的指导原则是：如果问题规模较大或比较难解，那么m a x f l i p s 和 m a x t r i e s 也应设置较大，而对于规模小或易解的实例，可设置较小的参数值。 内循环中( 3 ) 处的翻转( n i p ) 是指改变当前的真值赋值中待翻转变量p 的赋值， 即t m e 变为f a l s e 或相反。这个变量是在图中( 2 ) 处按一定的策略选取出来的，称 为一次“局部搜索”。现有的各种s a t 局部搜索算法的主要区别就在于该处选 取变量的策略( 即局部搜索策略) 的不同。 虽然各种算法中的局部搜索策略各不相同，但是可以为它们定义一个局部搜 索中通用的目标函数( o b j e c t 劬c t i o n ) 如下： 定义3 1 目标函数 s a t 局部搜索的目标函数是一个从关于变量集合v 的真值赋值集合t 到不 满足子句的个数( 概s a t ) 的映射，即o b j e c t ：t 专n 。 其中值域n = o ，1 ，n 1 1 m c l a u s e ) ，假设l v l - n ，则t 的元素个数为2 n 。 目标函数的全局最优值( 最小值) 为o ，该最优值对应使问题实例得到满足 的真值赋值( 问题的模型) ，即问题的解。对于可满足的s a t 实例，存在一个 或多个全局最优值，即有一个或多个解。每次局部搜索求解的过程就是通过若干 次( 最多f l i p s 次) 的局部调整搜索目标函数的全局最优值。 1 6 中山大学硕十学位论文命题可满足性问题( s 旧的局部搜索算法研究与改进 事实上，每种局部搜索策略中直接使用是一个或多个效益函数( s c o r e 劬c t i o m ，它是关于每个变量的函数，其函数值和目标函数值的变化呈( 近似) 正相关或( 近似) 负相关。下面给出有关概念的定义： 定义3 2 产生数和破坏数 在局部搜索的某个状态下( 对应的真值赋值为) ，对于s a t 问题的变量集合 v 中的每个变量p ，假设它翻转后的真值赋值为，则： ( 1 ) p 的“产生数”为矽未能满足的子句中，翻转p 后变为满足即矽能满足的 子句的数量，用m a l ( e c o u n t ( p ) 表示。称这些子句集合为p 的“产生子句集合”， 并用m a k e ( p ) 表示。 ( 2 ) p 的“破坏数”为矽已能满足的子句中，翻转p 后变为不满足即不能满 足的子句的数量，用b r e a l ( c o u n t ( p ) 表示。称这些子句集合为p 的“破坏子句集合 ， 并用b r e a k ( p ) 表示。 上述定义可以直观地表达为： ( 1 ) p 的“产生数”为该状态下p 出现在其中的不满足子句个数。 ( 2 ) p 的“破坏数”为该状态下p 出现在其中的恰好只有一个真文字( 即p 对应的文字) 的满足子句个数。 定义3 3 效益函数和效益值 在局部搜索的某个状态下，效益函数