（计算机软件与理论专业论文）sat问题的随机算法及其相变现象研究.pdf

主堕登兰竺查垄兰堡主兰竺丝墨 一! ! 兰 摘要 合取范式c n f ( c o n j u n c t i v en o r m a lf o h n ) 的可满足性s a t ( s a t i s f i a b i l i t y ) 问题 是人工智能、计算理论和理论计算机科学中的最瞩目问题之一s a t 问题的描述 是非常简单的，但它是第一个被证明的n p 完全问题，在计算复杂性理论中起着 很重要的作用。同时该问题在自动推理、计算机辅助设计和制造，机器视觉、数 据库、机器人、集成电路、计算机体系结构设计和计算机网络设计等许多实际问 题中得到广泛的应用。 一仁些求解s a t 问题的最成功的有效算法，如随机爬山法、禁忌搜索法、模拟 退灾法，都是基于随机算法的思想随机化方法已是求解s a t 问题的非常有效 的技术近年来，许多计算实验表明随着子句数与变量数之比增大时，随机k - s a t 问题的可满足概率发生相变现象计算可满足概率不仅仅是一个挑战性的纽合问 题，也是理解随机s a t 问题结构的一种较好途径本文将求解s a t 问题的随机 算法和其相变现象作为研究主题，其主要工作和贡献如下： 基于统计的随机算法：如果搜索不到可满足的真值赋值，传统随机算法难以 做出正确的判断。本文提出了一个利用搜索过程中不满足赋值的信息进行不满足 解数统计的思想，得到了两个有效的m o n t ec a r l o 型随机算法。第一个算法 s a t t e s t l 是在不满足赋值空间中进行搜索和抽样第二个算法s a t t e s t 2 则是在整 个赋值空间中进行搜索和抽样，因此可以搜索到可满足解，即使搜索不到可满足 解时，也能以高概率做出正确的判断，这是对传统随机算法的重要改进实验结 果表明，提出的算法对相变区域的难s a t 实例有较好的求解能力 d p 算法的一种有效折分策略：完全算法是求解s a t 问题的一类重要算法， 是非完全算法所不能替代的d p ( d a v i s p u t n a m ) 算法是最有效的完全算法之一， 提高d p 算法的效率关键在于折勿x - ( s p l i t t i n g ) & 字的选择本文基于前述的对不满 足解数估计的方法，提出了一个有理论依据的有效折分策略基于该策略的d p 算法平均执行时间要比原d p 算法的执行时间快2 倍多 随机算法r d p 的并行化：对d p 算法中的折分文字采用随机选择策略，我们 则得到了一种随机算法r d p 。由于随机算法的运行时间具有不确定性，为异步 主粤登兰垫查苎兰堡主茎竺丝圭苎主 并行化提供了较好的机会随机算法r d p 在各个不同的s a t 实例上有着不同的 运行时间分布，我们研究了异步并行加速与运行时间分布之间的关系理论分析 和计算实验都表明：当处理器数目较少时以及运行时间分布的单峰位于前部时， 随机算法r d p 的异步并行具有近线性的加速 随机k - s a t 问题可满足概率的近似计算式：对于随机k - s a t 问题，有许多计 算实验表明存在可满足概率的相变现象相变现象的研究对计算复杂性、p 完 全问题的难度、s a t 问题的高效求解算法等许多方面都有着重要影响本文提出 了，赋值组的概念，找出了其与可满足公式之间的关系在相关独立性的假设下， 得到了随机k - s a t 问题可满足概率的一个近似计算式对较小的变量数计算了可 满足概率，所得的结论与以往的结果丁致这是相变研究的一种新方法，目前只 是初步研究需要进一步的深入研究 本文的研究得到国家9 7 3 重点基地研究发展规划项目“难解问题的高效实用 算法及其应用”( n o g 1 9 9 8 0 3 0 4 0 3 ) 和国家教育部博士点基金( n o 9 7 0 3 8 2 5 ) 的 资助 关键词：p 难解问题，s a t 问题，随机算法，d p 算法，并行算法，相变现象 里翌兰垫查苎堂堡主兰堡垒查! ! 兰 a b s t r a c t t h es a t ( s a d s f i a b i l i t y ) p r o b l e mf o rp r o p o s i t i o n a lf o r m u l a si nc n f ( c o n j u n c t i v e n o r m a lf o r m ) i so n eo ft h em o s tp r o m i n e n tp r o b l e m si na r t i f i c i a li n t e l l i g e n c e ，c o m p u t i n gt h e o r y a n dt h e o r e t i c a l c o n l d l l t e rs c i e n c e a l t h o u g ht h ed e s c r i p t i o no fs a tp r o b l e mi sv e r ys i m p l e ，i ti st h e f i r s tp r o b l e m s h o w nt ob en p c o m p l e t ea n dp l a y sa ni m p o r t a n tr o l ei nt h et h e o r yo fc o m p u t a t i o n a lc o m p l e x i t y f u r t h e f m o r e i th a saw i d ev a r i e t y o fa p p l i c a t i o n si n s o l v i n gm a n yp r o b l e m s i na u t o m a t e d r e a s o n i n g ，c o m p u t e r a i d e dd e s i g n ，c o m p u t e r - a i d e d m a n u f a c t u r i n g ，m a c h i n ev i s i o n ，d a t a b a s e ， r o b o t i c s ，i n t e g r a t e dc i r c u i td e s i g n ，c o m p u t e r a r c h i t e c t u r ed e s i g n ，a n dc o m p u t e rn e t w o r kd e s i g n s o m eo ft h em o s ts u c c e s s f u la n dp o w e r f u la l g o r i t h m sf o rs a tp r o b l e ml i k e r a n d o m i z e d h i l l c l i m b i n g ，t a b us e a r c h ，a n d s i m u l a t e da n n e a l i n ga r eb a s e do nr a n d o m i z e da l g o r i t h m s r a n d o m i z a t i o nh a sp r o v e dt ob eav e r yu s e f u lt e c h n i q u ei ns o l v i n gf o rs a tp r o b l e m i nr e c e n t y e a r s ，m a n ye x p e r i m e n t sh a v es u g g e s t e dt h a tt h e r ee x i s t s as a t i s f i a b i l i t yt h r e s h o l dp h e n o m e n o n w i t hr e s p e c tt ot h er a t i oo ft h en u m b e ro fc l a u s e st ot h en u m b e ro fv a r i a b l e so fs a tf o r m u l a e c a l c u l a t i n gt i l es a t i s f i a b l ep r o b a b i l i t y , b e s i d e sb e i n gac o m b i n a t o r i a lc h a l l e n g e ，h a sa p p e a r e da sa b e t t e rw a yt ou n d e r s t a n dt h es t r u c t u r eo fr a n d o ms a tp r o b l e m i nt h i st h e s i s ，r a n d o m i z e d a l g o r i t h m sf o rs a tp r o b l e ma n di t sp h a s et r a n s i t i o np h e n o m e n o nh a v eb e e ns t u d i e d t h em a i n c o n t r i b u t i o n so ft h i st h e s i sa r ei nt h ef o l l o w i n g a l g o r i t h m s b a s e do ns t a t i s t i c ：i fn os a t i s f i a b l es o l u t i o n s a r ef o u n d ，t h ec o n v e n t i o n a l r a n d o m i z e da l g o r i t h m sf o rs a tp r o b l e m sa r ed i f f i c u l tt oj u s t i f yt h es a t i s f i a b i l i t yo fs a tp r o b l e m s c o r r e c t l y i nt h i st h e s i s ，w ep r e s e n ta ni d e at h a ti st oc o u n tu n s a t i s f i a b l es o l u t i o n sb yt h em e s s a g e o fu n s a t i s f i a b l ea s s i g n m e n t si n s e a r c h i n g ，a n dd e s i g nt w oe f f i c i e n t m o n t ec a r l or a n d o m i z e d a l g o r i t h m s f o rf i r s ta l g o r i t h ms a t t e s t l s e a r c h i n ga n ds a m p l i n g a r ei nt h es p a c eo fu n s a t i s f i a b l e a s s i g n m e n t s f o rs e c o n da l g o r i t h ms a t t e s t 2 ，s e a r c h i n ga n ds a m p l i n ga r ei nt h ew h o l es p a c eo f a s s i g n m e n t s h e n c ei tc a nf i n dt h es a t i s f i a b l es o l u t i o n e v e nn os a t i s f i a b l es o l u t i o n sc a nb ef o u n d ， i ti ss t i l lt ot e s tt h es a t i s f i a b i l i t yo fs a tp r o b l e mw i t hh i g hp r o b a b i l i t y t h i si sa ni m p o r t a n t i m p r o v e m e n to ft h ec o n v e n t i o n a lr a n d o m i z e da l g o r i t h m s e x p e r i m e n t a lr e s u l t s ，c o n d u c t e do na n u m b e ro fs a ti n s t a n c e sn e a rt h ep h a s et r a n s i t i o n ，i n d i c a t et h a to u rm e t h o d sl e a dt os i g n i f i c a n t p e r f o r m a n c ei m p r o v e m e n t sf o rh a r ds a tp r o b l e m s a ne f f i c i e n ts p l i t t i n gs t r a t e g yf o rd p a l g o r i t h m ：t h ec o m p l e t ea l g o r i t h m sa r ea ni m p o r t a n t t y p e o fa l g o r i t h m sf o r s o l v i n gs a tp r o b l e m ，w h i c hc a n n o tb er e p l a c e db yt h ei n c o m p l e t e a l g o r i t h m s d p ( d a v i s - p u t n a m ) a l g o r i t h mi s o n eo ft h em o s te f f i c i e n tc o m p l e t ea l g o r i t h m s t h e k e yo fe f f i c i e n c yo fd pa l g o r i t h mi st h ec h o i c eo fs p l i t t i n gl i t e r a l b a s e do na b o v em e t h o do f c o u n t i n gu n s a t i s f i a b l es o l u t i o n s ，a ne f f i c i e n ts p l i t t i n gs t r a t e g yo ft h e o r e t i c a lf o u n d a t i o nh a sb e e n p r o p o s e d t i l ed pa l g o r i t h mb a s e do nt h i ss p l i a i n gs t r a t e g yi sab i to v e rt w ot i m e sf a s t e rt h a nt h a t o fd p a l g o r i t h mi na v e r a g e 苎苎兰苎查查兰堡主兰竺丝圭 一 一! ! 墨 p a r a i l e l i z a t i o no fr a n d o m i z e da l g o r i t h mr d p ：t h er a n d o m i z e da l g o r i t h m r d pc a nb e o b t a i n e db yr a n d o m i z e ds p l i t t i n gs t r a t e g ya p p l i e di nd pa l g o r i t h m t h eu n c e r t a i n t yo fr u n n i n g t i m eo fr a n d o m i z e da l g o r i t h m sp r o v i d e sab e a e ro p p o r t u n i t yf o ra s y n c h r o n i z e dp a r a l l e l i z a t i o n t h er a n d o m i z e da l g o r i t h mr d ph a sv a r i o u sr u n n i n gt i m e so nd i f f e r e n ti n s t a n c e so fs a t t h e r e l a t i o no fa s y n c h r o n i z e dp a r a l l e l i z a t i o na n dr u n n i n gt i m ed i s t r i b u t i o n sh a sb e e ni n v e s t i g a t e d b o t ht h e o r e t i c a la n a l y s i sa n dc o m p u t i n ge x p e r i m e n ti n d i c a t e st h a ta s y n c h r o n i z e dp a r a l l e l i z a t i o no f r a n d o m i z e da l g o r i t h mr d p i so f n e a rl i n e a ra c c e l e r a t i o nw h e n p r o c e s s o r si sl e s sa n ds i n g l ep e a ki s l o c a t e dn e a rt h ef r o n to f r u n n i n g t i m ed i s t r i b u t i o n s a p p r o x i m a t ec o m p u t a t i o n o fs a t i s f i a b l ep r o b a b i l i t yo fr a n d o m i z e dk - s a t ：f o rr a n d o m i z e d k - s a t , t h e r eh a v eb e e nm a n ye x p e r i m e n t sv e r i f y i n ge x i s t e n c eo fp h a s et r a n s i t i o np h e n o m e n o ni n s a t i s f i a b l e p r o b a b i l i t y r e s e a r c h o n p h a s e t r a n s i t i o n p h e n o m e n o n h a s i m p o r t a n t e f f e c t so n c o m p u t a t i o nc o m p l e x i t y ，n p - c o m p l e t ep r o b l e m ，e f f i c i e n ta l g o r i t h m sf o rs o l v i n gs a tp r o b l e m ，a n d s oo n i nt h i st h e s i s ，t h ec o n c e p to f - a s s i g n m e n t sg r o u p sh a sb e e np r o p o s e d ，a n dt h er e l a t i o no f - a s s i g n m e n t sg r o u pa n d s a t i s f i a b l ef o r m u l ah a sb e e ns t u d i e d m o r e o v e r , a n a p p r o x i m a t e c o m p u t a t i o no fs a t i s f i a b i l i t yp r o b a b i l i t y o fr a n d o m i z e dk - s a tu n d e r a s s u m p t i o n o fc e r t a i n i n d e p e n d e n c eh a sb e e ng i v e n w h e nn u m b e ro fv a r i a b l e si s n o tb i g ，c o m p u t i n gr e s u l to ft h e s a t i s f i a b l ep r o b a b i l i t yi sc o n s i s t e n tw i t ht h ep r e v i o u sf a c t st h i sr e s e a r c hs h o w san e w t y p eo f m e t h o d n o w ，t h et h e s i si so n l yap r e l i m i n a r yr e p o r ta n df u r t h e rs t u d yi sn e e d e d t h i sr e s e a r c hi s s u p p o r t e db yt h e n a t i o n a l9 7 3f u n d a m e n t a lr e s e a r c ha n dd e v e l o p m e n t p r o g r a mp r o j e c t ”e f f i c i e n t a n dp r a c t i c a l a l g o r i t h m s f o rn p h a r dp r o b l e m sa n dt h e i r a p p l i c a t i o n s ”t w o g t9 9 8 0 3 0 4 0 3 ) k e yw o r d s ：n p h a r dp r o b l e m ，s a tp r o b l e m ，r a n d o m i z e da l g o r i t h m ，d pa l g o r i t h m ，p a r a l l e a l g o r i t h m ，p h a s et r a n s i t i o np h e n o m e n o n 里翌堂垫查查兰堡主芏竺垒查一墨土兰塑 第1 章绪论 s a t 问题是人工智能、运筹学和理论计算机科学共同关注的重要问 题，在理论和应用领域都有非常重要的研究意义，其快速求解算法的研 究成为计算机科学的中心课题之一本章首先给出了s a t 问题及其相 关定义，然后对研究历史、现状和发展作一个综述，最后引出了本文研 究的主题，即s a t 问题的随机算法及其相变现象研究 1 is a t 问题概述 实际应用领域中存在大量的p 难解问题，寻求其有效算法一直是计算机理 论和工程一p 的核心任务。s a t ( s a t i s f i a b i l i t y ) 是 垆难解问题中的典型问题，不仅 在汁算复自 性、a r 尸完全理论等方面有着举足轻重的研究地位，而且在自动推理、 计算机辅助设计和制造、机器视觉、数据库、机器人、集成电路、计算机体系结 构设计和计算机网络设计等应用领域有着广泛的应用。近十年来，s a t 问题的研 究取得了瞩目的进展，成为人工智能、运筹学和理论计算机科学的研究热点。在 这1 7 我们将对其定义、求解算法、生成模型等作一简要的介绍。 1 1 1 基本定义 合取范式c n f ( c o n j u n c t i o n n o r m a lf o r m u l a ) 是命题逻辑公式的标准形式，具 有一般的意义。p l a i s t e d 和n i l s s o n 1 ，2 讨论了机器定理证明中的合取范式c n f 的优缺点，指出任何一个命题逻辑公式都能转换为一个等价的合取范式c n f 。 并且能够使用辅助命题( a u x i l i a r yp r o p o s i t i o n s ) 的方法在多项式时间内进行这种 转换 3 】。因此本文只考虑合取范式的s a t 问题。首先，设己，_ f “，”2 ， 表 示 个布尔变量”。，u ：。，u 。构成的集合。下面给出s a t 问题及其相关定义。 定义1 - 1 ( 真值赋值) u 的真值赋值是一个函数，：u 。 t r u e ，f a l s e ”。每个真 堕壁兰垫查苎鲎堡主兰堡垒叁 一墨! 二! ! 鱼 值赋值可以用一个n 元布尔向量表示，那么在u 上存在2 ”个不同的真值赋值。 对于某个布尔变量u ，如果t ( u ) = t r u e ，称“在赋值，下取真值；如果，( “) 2 f a l s e ， 称“在赋值f 下取假值。 定义1 2 ( 文字) 如果“是u 中的一个布尔变量，称u 和，“( 或记为“) 是 u 的文字，其中“是正文字，u 是反文字。文字在赋值，下取真值当且仅当 变量“在赋值f 下取真值。文字一u 在赋值，下取真值当且仅当变量u 在赋值f 下取假值。 定义1 3 ( 子句) 子句c = l ，v l ，v v 厶，其中厶为u 上的文字，v 为析 取运算符。在赋值，下，子旬c 可满足当且仅当至少有一个文字厶在赋值，下取 真值。符号icf 表示子句c 中的文字个数，即子句c 的长度。 定义1 - 4 ( 合取范式c n f ) 合取范式f = c ，ac ， a 巳，其中g 为子 句，a 为合取运算符。f 也称为公式，记作f c n f 。公式f 在赋值，下是满足 的当且仅当每个子句c f 均满足。如果存在赋值r 使得，满足，则称，是可满足 公式。 定义1 - 5 ( s a t 闯题) 给定布尔变量集u 上的一个c n f 范式f ，问是否存在 u 的一个真值赋值t ，使得f 满足? 特别规定：任意赋值都不满足空子句，任意赋值都满足空公式。 例1 - 1 合取范式f = ( “iv i ) ( “4v “5v u 1 ) ( “3v “4v i ) ，只要赋值 ( f ( “1 ) ，t ( u 2 ) ，t ( u 3 ) ，t ( u 4 ) ，t ( u 5 ) ) = ( t r u e ，t r u e ，f a l s e ，办“p ，f a l s e ) 时，就使得公式f 满足， 这样可满足的真值赋值有许多。为方便起见，上面的真值赋值简记为 ( ，u 2 ，u 3 ，u 4 ，“5 ) = ( 1 ，1 0 1o ) ，这里1 表示t r u e ，0 表示f a l s e 。 定义1 - 6 ( 重言子句) 若u 和，“同时出现在某一子句中，则称该子句为重言 子句。 定义1 7 ( 七一s a t 公式) 若公式中每个子句长度均为k ，则称该公式为k - s a t 公式。 s a t 问题是约束满足问题c s p ( c o n s t r a i n ts a t i s f a c t i o n p r o b l e m s ) 的特例，s a t 公式中的子句视为c s p 中的约束，因此任何c s p 算法可以应用到s a t 问题中。 c s p 问题是极其常见的，许多n p 完全问题最初表述为个c s p 问题。s a t 问 2 里型兰垫查苎兰堡主兰堡笙查一j 王l ! l 堡 题与c s p 问题的关系【4 1 ( 如图l - 1 ) c s p f n q u e u e p r o b l e m d i s c r e t e c s p g r a p h c o l o r i n gp r o b l e m is c h e d u l i n g p r o b l e m f 鲥t p r o b l e m 尉阳，) ， 凹1 胍一删7 1p r d 6 如m 图1 - 1s a t 与c s p 的关系 1 1 2 n p 完全和n p 难解问题 一、多项式时间算法与有效算法 对于给定的问题，我们感兴趣的是寻找解决问题的“有效”算法。如果算法 本身耗费的资源过于庞大，甚至无法在实际的计算机模型上实现，这样的算法当 然不能认为是有效的算法。算法的资源主要分为：时间资源和空间资源。一般来 说，时问足决定算法效率的主要因素，本文中我们主要考虑时间资源。不同的算 法有着不同的时间复杂度函数。通常人们认为算法如果不能在多项式时间内求解 问题，则这样的算法不是有效算法，因为这样的算法在输入规模增加时，运行时 间将以指数速度增加，以至于达到无法接受的地步。 定义1 - 8 ( 多项式时间算法) 多项式时间算法定义为时间复杂度函数是d ( p ( 帕) 的算法，其中n 是问题实例的规模，p ( ”) 是一个多项式函数。 定义1 - 9 ( 指数时间算法) 对于时间复杂度高于d ( p ( ”) ) 的算法称为指数时间 算法。 多项式时间算法和指数时间算法在问题规模增长时的表现是相当不同的。假 设一台计算机的计算速度为每秒1 0 亿次，这接近目前最快的微处理器的速度。 比较了具有几种不同时间复杂度函数的算法在输入规模增加时运算时间增长的 情况，从表l 一1 中可以看出，指数时间算法在输入规模增加时运算时间急剧增长， 最终将达到天文数字的量级。 3 中田科学技术大学博士学位论文 第1 幸绪论 表1 - 1 不同时间复杂度函数下算法性能的比较 时间输入规模n 复杂度 1 02 03 04 0 1 0 0 1 0 纳秒2 0 纳秒3 0 纳秒4 0 纳秒1 0 0 纳秒 n l o g n1 0 纳秒 2 6 0 纳秒4 4 3 纳秒6 4 ，1 纳秒2 0 0 纳秒 1 0 0 纳秒4 0 0 纳秒9 0 0 纳秒1 6 微秒1 0 微秒 2 “ i 0 微秒1 0 毫秒1 1 秒1 8 3 分4 0 世纪 n 1 3 6 毫秒7 7 1 年 8 4 1 0 。3 世纪2 6 1 0 2 9 世纪3 0 1 0 1 3 9 世纪 我们定义的多项式时间算法与指数时间算法均是时间复杂性为最坏情形下 的度量。不幸的是有些问题很难甚至不可能存在最坏情形下的多项式时间算法， 如s a t 问题就是这类“难解”问题之。因此，要研究这类问题的其他意义下 的有效算法。如，可以研究一个问题的部分实例集的有效算法，也可以以牺牲解 的质量和求解成功概率来获取多项式时间算法，即近似算法和随机算法。实际应 用中这些意义下的有效算法都是非常有用的。 二、难解问题 一个问题往往有多种算法，很有可能其中一些是有效的。而另一些是无效的。 然而有可能存在这样一个问题，它根本不存在有效的算法，也就是说，问题困难 到不可能用多项式算法求解。这时，我们称这个问题是难解的。 证明一个问题的难解性也并不是一项简单的工作。给定一个问题，说明它是 一个难解问题也许并不比为它寻找一个有效算法简单。我们只有尝试其它的途 径，也就是证明它与大量的其它问题一样“困难”。证明两个问题相关的基本手 段是通过给出一个构造性变换将一个问题的任意实例映射到另一个问题的等价 实例，从而把一个问题归约到另一个问题。如果问题a 可以归约到问题b ，则 可以将求解b 的算法变换成求解a 的算法，这样，问题b 就至少是和问题a 一 样“困难”。 三、p 与n p n p 完全理论是为了确定不同问题的难度，检验各个问题在难易程度上的相 互关系而建立的理论。p 和p 是该理论中的两个基本概念，其定义如下： 定义l - 1 0 ( p 与n p ) p 是所有可以在多项式时间内用确定图灵机求解的判定 问题的集合。n p 是所有可在多项式时间内用非确定图灵机求解的判定问题的集 合。 这样，如果一个问题属于p ，则可以认为它是易于求解的。如果一个问题属 4 里翌兰垫查垄兰堡主兰垡丝查 一! j j 生! ! 堡 于 甲但不属于尸，则它不一定存在多项式时间的算法。p 是否等于n p 是在计 算机科学领域中至今尚未解决的一个著名难题。人们一般认为p 不等于p ，也 就是泌，存在一些p 问题，它们无法在多项式时间内用确定图灵机求解。 1 9 7 1 f ，s t e ：p h e nc o o k 在a c m 计算理论年会( s t o c ) 上发表的论文“t h e c o m p l e x i t yo f t h e o r e m p r o v i n gp r o c e d u r e s ”奠定了n p 完全性理论的基础【5 。他 在该文中证明了所有的n p 问题都可以多项式时间归约为s a t 问题。 这样，只要解决了s a t 问题，也就解决了所有的n p 问题，因此可以认为 s a t 问题足n p 问题中“最难”的问题。后来，人们又证明了还有许多的这样的 n p 问题。例如旅行商问题、图着色问题等和s a t 问题一样，都具有这种“最难” 的性质，人们将它们归结为一类，称为n p 难问题。 定义1 - 1 f ( n p 难解与n p 完全) 如果s a t 问题归约成问题厶则称问题三 足_ 7 ) 难解的。如果工是n p 难解的且l n p ，则称问题上是n p 完全的。 这样，有些问题是n p 难解的，但不是n p 完全的。例如n p 完全问题必须是 判定问题，其对应的优化问题就可能是n p 难解的。 p 完全问题的应用非常广泛，在【6 】的附录中列出了1 2 大类，3 0 0 多个p 完全问题，它们来自图论、网络设计、排序调度和数学规划等众多领域。然而， 赢至目前还无法找到这些问题的有效算法，计算机科学家普遍认为找不到n p 完 全问题的多项式时间的有效算法。另一方面，人们从三个方面研究这些难解问题 的实际有效算法【8 】： 寻求解决某个问题的子类的有效算法 研究有效的近似算法 使用随机化方法 1 1 3 求解算法分类 s a t 问题的算法主要分为两大类：完全算法和非完全算法。完全算法能够保 证正确判定任何输入实例( 公式) 的可满足性，特别对于不满足的公式的判断是 非完全算法所不能替代的。非完全算法不能保证j 下确判断可满足性，但这类算法 采用启发式策略指导搜索，普遍快于完全算法。 除了上面的一般划分之外，g u 4 ，7 】将已有的求解s a t 问题的算法分为以下 璺登兰垫查苎兰堡主兰竺堡圭j ! _ l 兰! ! ：兰 几类： 离散约束算法( d i s c r e t e ，c o n s t r a i n e da l g o r i t h m s ) 离散无约束算法( d i s c r e t e ，u n c o n s t r a i n e da l g o r i t h m s ) 约束规划算法( c o n s t r a i n e dp r o g r a m m i n ga l g o r i t h m s ) 无约束非线性优化算法( u n c o n s t r a i n e d ，n o n l i n e a ro p t i m i z a t i o na l g o r i t h r n s ) 并行离散约束算法( p a r a l l e l ，d i s c r e t e ，c o n s t r a i n e da l g o d t h r n s ) 并行离散无约束算法( p a r a l l e l ，d i s c r e t e ，u n c o n s t r a i n e da l g o f i t h m s ) 并行约束规划算法( p a r a l l e l ，c o n s t r a i n e dp r o g r a m m i n ga l g o r i t h m s ) 并行无约束非线性优化算法( p a r a l l e l ，u n c o n s t r a i n e d n o n l i n e a r o p t i m i z a t i o n a l g o r i t h m s ) 1 1 4 生成模型与难解性 为了测试一个求解s a t 问题算法的效率，同时也为了保证不同算法的测试环 境的公平性，人们先后提出了许多s a t 实例生成模型，并形成了标准测试实例 集b e n c h m a r k 。主要有以下三种生成模型 9 】： 1 实际问题模型 这些问题一类来自图着色、n 皇后等理论问题；一类来自实际应用中的 问题，如，大规模集成电路设计v l s i 、移动通讯、计算机体系和网络设计、 调度和规划( s c h e d u l i n g a n dp l a n n i n g ) 等。这种模型下的实例明显带有原问 题的一些结构特征，有时也称此种模型为结构问题模型。现在有许多这样的 实例在i m e m e t 上发布，具体参见1 1 5 节。 2 固定概率模型 此模型由o o l d b e r g 10 在19 7 9 年提出。每个实例由三个参数嘲，棚，矿决 定， n 是变量数，m 是子句数，p 是每个变量在予句中出现的概率且0 l 时，随m 足够大时随机赋值就能依概率1 求得c n f 范式的满 足解。因此，现在人们主要研究实际问题模型和随机k - s a t 模型。一般认为如果 算法在随机k - s a t 模型上有好的性能，对于实际问题模型也有好的性能【1 3 】，但 也有人对此提出异议 1 4 ，不过人们首先考虑的还是算法在随机k - s a t 模型上的 性能。即使对于同一生成模型的不同实例也会导致算法的不同表现，例如，1 w a m a 算法f 15 1 求解有较多解的实例快于求解有较少解的实例，而简单回溯算法 1 6 】正 好相反。 另外，i 于随机k - s a t 模型的对称性和均匀性，使得该模型更适合作为算法 的解析分析。 1 1 5 重要文献资源 关于s a t 问题的研究资源已有不少，包括综述性书籍、论文、网上资源和重 要国际会议等。 s a t 问题已有大量的研究论文，这里仅介绍几篇有影响的综述文章。1 9 9 7 年，g u 、p u r d o m 、f r a n c o 和w a h l 4 对s a t 问题写了一个全面的综述，从对算法 空m 的划分出发，论述了各类算法的原理、技术、特点等，并对应用和未来工作 进行了深入的探讨，内容非常翔实，是s a t 问题研究的重要参考资料。有两篇 博二仁论文必须提一下，一篇研究了完全算法，另一篇研究了非完全算法。1 9 9 5 年，f r e e m a n 的博：b 论文【9 对s a t 问题的完全算法进行了深入研究，特别是对 提高完全搜索算法的计算能力方面提供了有用的技术和方法。1 9 9 8 年，h o o s 的 博：i ：论文【8 1 对一类非完全算法随机局部搜索法( s t o c h a s t i cl o c a ls e a r c h ) 进行 了全而的研究，探讨了方法、模型和应用。还有一些不错的文章可供参考： 苎型鲎垫查垄兰堡主兰堡堡查墨主! ! 鱼 d o u g l a s 1 7 ，g e n t 和w a l s h 1 8 ，堵丁柱等【1 9 】，d u b o i s 等 2 0 】，顾钧【2 1 】，k u m a r 2 2 。 1 9 9 8 年6 月h 0 0 s 等人建立了一个专门研究s a t 及其相关问题的网址 s a t l i b ( h t t p ：w w w i n f o r m a t i k t u - d a r m s t a d t d e a l s a t l i b ) ，它主要提供了s a t 算 法的测试用例库( b e n c h m a r kl i b r a r y ) 、各种s a t 算法、研究文献和研究人员情况 等资源，这些资源都可以免费下载得到，大大方便了s a t 算法的计算实验和研 究信息的交流。在s a t l i b 之前已有两个b e n c h m a r k ，一个是第二届美国的离散 数学和理论计算机科学研究中心d i m a c s竞赛库 ( f i p ：d i m a c s m t g e r s e d u p u b c h a l l e n g e s a t i s f i a b i ! i t y b e n c h m a r k s e n f ) 2 3 ，另一个是 北京竞赛库( h t t p ：w w w c i r l u o r e g o n e d u j c b e i j i n g ) 。 尽管没有专门讨论的学术刊物，但s a t 问题是许多数学、运筹学、理论计算 机、人工智能等刊物的重要内容。一些著名的学术刊物如s i a mt r a n s a c t i o no n c o m p u t i n g 、j o u r n a lo f t h e a c m 、t h e o r e t i c a lc o m p u t e rs c i e n c e 、j o u r n a lo f a r t i f i c i a l i n t e l l i g e n c er e s e a r c h 、j o u r n a lo f a l g o r i t h m s 和a l g o r i t h r n i c a 等。