（基础数学专业论文）dpll到（11）消解的转换及其复杂性分析.pdf

摘要 命题公式的满足性问题( 简称s a t 问题) 是指布尔表达式的可满足性问 题它是理论计算机科学中的一个重要问题在数理逻辑、人工智能、约束满 足问题、v l s i 集成电路设计与检测以及计算机科学理论等领域具有广阔的应用 背景。s a t 问题是第一个n p 一完全问题，并且是一大类n p 一完全问题的核心。 一个c n f 公式( c o n j u n c t i v en o r m a lf o r m ) 是有限个子旬的合取，( r s ) 一c n f 公 式是指每个子句恰恰含有r 个不同的文字，且每个变量出现的次数最多出现s 次的c n f 公式类，( r s ) - s a t 是限定在( r s ) 一c n f 上的命题满足性实例。一个 s a t 算法能在有限时间内判定任意给定的c n f 公式是否可满足，d p l l 算法和 消解反驳法是判定s a t 问题的两个重要方法。o l g at v e r e t i n a 和h a n sz a n t e m a 已经详细分析了d p l l 算法到消解的转换，并证明了，如果有一个长度为s 的 d p l l 反驳，结点数为r ，且每个结点标记的单位消解序列是完备的，则存在一 个长度为s - r 的消解反驳，显然这个长度已经优于s 。我们已经知道，对于任意 一个m u ( 1 ) 公式对应一个( 1 ，1 ) 一消解。极小不可满足公式的研究是近年来兴起的 问题的一个热点方向。德国学者h k l e i n eb i i n i n g ，o k u l l m a n n 等人在这方面做了 许多重要的工作。极小不可满足公式的一些结构和性质将有助于判定s a t 算法 的研究。 本文通过研究极小不可满足公式的树消解证明及极小不可满足公式的分 裂，构建了( r ，s ) 一s a t 中的一些极小不可满足实例。并在此基础上，表示了( r ，s ) 一 s a t 中的一些n p 一完全实例。 进一步，在极小不可满足公式的构建方法及分裂定理的基础上，将消解转 换到了( 1 ，1 ) 一消解，由此，得到了d p l l 到( i ，i ) 一消解的转换，从而建立了一套完 备的消解证明系统。 关键词：s a t ( r ，s ) 一s a t 极小不可满足公式d p l l 消解 中图分类号：文献标识码：a l l l a b s t r a c t t h e s a t i s f i a b i l i t yp r o b l e m ( s a tp r o b l e m ) o f p r o p o s i t i o n a lf o r m u l a sr e f e r st os a t i s f i a b i l i t yp r o b l e mo fb o o l e a nf o r m u l a s am a j o rp r o b l e mi nt h e o r e t i c a lc o m p u t e rs c i e n c e ，w h i c hc a nb ew i d e l yu s e di ns u c hf i e l d sa ss y m b o l i ci o 百c ，a r t i f i c i a li n t e l l i g e n c e ， c o n s t r a i n ts a t i s f a c t i o np r o b l e m ，d e s i g na n dd e t e c t i o no fv l s ii n t e g r a t ec i r c u i t ，a n d t h e o r i e so fc o m p u t e rs c i e n c e s a tp r o b l e mi st h ef i r s tn p - c o m p l e t ep r o b l e ma n d t h en u c l e u so ft h ec a t e g o r yo fn p - c o m p l e t ep r o b l e m s ac nff o r m u l ai st h ec o n - j u n c t i o no ff i n h ec l a u s e s ( t ，s ) 一c n ff o r m u l a sm e a na l lt h ec ff o r m u l a st h a t c o n t a i nrv a r i a b l e sa n de v e r yv a r i a b l eo c c u r sa tm o s tst i m e s ( r ，8 ) 一s a ti st h e 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 e mi n s t a n c e si n ( r ，s ) 一c n f as a ta l g o r i t h mc a r l d e t e r m i n ew h e t h e ra n yg i v e nc n ff o r m u l ai ss a t i s f i a b l ei nl i m i t e dt i m e d p l l a l g o r i t h ma n dr e s o l u t i o nr e f u t a t i o na r et w ok e ym e t h o d sr e s o l v i n gs a ? p r o b l e m s o l g at v e r e t i n aa n dh a n sz a n t e m ah a v ea n a l y z e di nd e t a i l st h et r a n s f o r m a t i o nf r o m d p l la l g o r i t h mt or e s o l u t i o n 、i m p r o v i n gt h a ti fi nt h ed p l lp r o c e d u r esu n i t r e s o l u t i o ns t e p sa r ee x e c u t e da n drr e c u r s i v ec a l l sa r ed o n e ，ar e s o l u t i o nr e f u t a t i o n e x i s t so fl e n g t ha tm o s ts r b e i n ge s s e n t i a l l yb e t t e rt h a ns a sw ek n o w f o ra n y f o r m u l ai nm u ( 1 ) ，t h e r ei sac o r r e s p o n d i n g ( 1 ，1 ) 一r e s o l u t i o nr e f u t a t i o n r e s e a r c h o fm i n i m a lu n s a t i s f i a b l ef o r m u l a si st h ef o c u sp r o b l e m st h a th a v ee m e r g e di nr e c e n t y e a r s ，o nw h i c hg e r m a n ys c h o l a r ss u c ha shk l e i n eb f i e n i n g ，0 k u l l m a n ne t c h a v ed o n em u c hw o r k ，s o m es t r u c t u r e sa n dp r o p e r t i e so fm i n i m a lu n s a t i s f i a b l e f o r m u l a sw i l lp r o m o t er e s e a r c ho fa l g o r i t h mo fs o l v i n gs a t t h r o u g hs t u d y i n gt r e er e s o l u t i o np r o o f so fm i n i m a lu n s a t i s f i a b l ef o r m u l a sa n d s p l i t t i n go fm i n i m a lu n s a t i s f i a b l ef o r m u l a s ，w ec o n s t r u c t sm i n i m a lu n s a t i s f i a b l ei n s t a n c e si n ( r ，s ) 一s a ta n dp r e s e n t ss o m em i n i m a lu n s a t i s f i a b l en p c o m p l e t ei n s t a n c e si n ( r s ) 一s a ri nt h i sp a p e r f u r t h e r m o r e ，o i lt h eb a s i so fc o n s t r u c t i o nm e t h o do fm i n i m a lu n s a t i s f i a b l ef o r m u l a s ，ac o n c r e t et r a n s f o r m a t i v em e t h o df r o mr e s o l u t i o np r o o ft o ( 1 ，1 ) 一r e s o l u t i o n p r o o fi sf o u n d ，a n da c c o r d i n g l yg e t t i n gat r a n s f o r m a t i o nf r o md p l la l g o r i t h mt o ( 1 ，1 ) 一r e s o l u t i o np r o o f k e yw o r d s ：s a t ，( r ，8 ) 一s a t ，m i n i m a lu n s a t i 妒a b l ef o r m u l a ，d p l l ，r e s o 1 u t i o n l l c h a p t e r1 i n t r o d u c t i o n t h es a t i s f i a b i l i t yp r o b l e mo fl o g i cf o r m u l ai st h ef a m o u sp r o b l e mi nt h e o r e t i c a lc o r n p u t e rs c i e n c ea n da r t i f c i a li n t e l l i g e n c el o g i ci st h eb a s i co fc o m p u t e rs c i e n c e ，t h e r e r l r e m a n yl e a r n e dm e nw i t hd e f e r e n tb a c k g r o u n db ee n g a g e di nr e s e a r c ho fs a t a l o to fs c i e n t i f i cp a p e r sa p p e a ri nm a n yf a m o u sm a g a z i n e sa n dc o n f e r e n c ep r o c e e d i n g s o fe v e r yf i e l dw h i c hi n c l u d e ：a r t i f i c i a li n t e l l i g e n c e ，( 1 0 9 i cp r o g r a m m i n gd e s i g na n d a u t o m a t i ci n f e r e n c e ) ，o p e r a t i o n a lr e s e a r c h a l g o r i t h m ，d i s c r e t em a t h e m a t i c ，e t c al i t e r a l 厶，i ni sap r o p o s i t i o n a lv a r i a b l eo ran e g a t e dp r o p o s i t i o n a lv a r i - a b l e ac l a u s eci sad i s j u n c t i o no fl i t e r a l s ：c = ( l lv 一vl 。) ，w ec a l l e dt h e n u m b e ro ft h el i t e r a l st h el e n g t ho ft h ec l a u s eac l a u s ew i t ho n el i t e r a ln a m e du n i t c l a u s e ，a n dac l a u s ew i t h o u tl i t e r a li se m p t yc l a u s ed e n o t e db y 上af o r m u l afi n c o n j u n c t i v en o r m a lf o r m ( c n f ) i sac o n j u n c t i o no fc l a u s e s ：f = ( c la ag ) w ec a n 、+ i e wac l a u s e ( l 1v vl m ) a sas e to fl i t e r a l s l 1 l m ) ac n ff o r m u l a ( c 1a ac n ) a sas e to fc l a u s e s c l ，g ) o ral i s to fc l a u s e sf c l ) 一，g 】 t i l es i z eo fc n ff o r m u l afi sd e f i n e da s s i z e ( f ) = c fl c l t , a r ( f ) i st h es e t o fv a r i a b l e so c c u r r i n gi nt h ef o r m u l afa n dl i t ( f ) i st h es e to fl i t e r a l so v e rf w ed e n o t e # c l ( f ) a st h en u m b e ro fc l a u s e so ffa n d # v a r ( f ) a st h en u m b e ro f v a r i a b l e so c c u r r i n gi nf f o rac n ff o r m u l af ，w ed e n o t eb yp o s ( x ，f ) ( r e s p n e g ( x ，f ) ) t h en u m b e ro fo c c u r r e n c e so fp o s i t i v e ( r e s p n e g a t i v e ) l i t e r a lzi nf ，a n d d e f i n eo c c ( z ，f ) = p o s ( z f ) + n e g ( x ，f ) f o rf i x e dp o s i t i v ei n t e g e r ska n ds ，w e d e n o t eb y ( ，s ) 一c n ft i l es e to ff o r m u l a s f c n ff b re a c hc l a u s ec f l c l = a n df o re a c hv a r i a b l ez v a r ( f ) ，o c c ( x ，f ) s ) ，a n d ( 7 1 ，s ) 一s a ti st h ep 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 e mr e s t r i c t e dt oi n s t a n c e si n ( r ，s ) 一c n f t h e & f i c i e n c yo f af o r m u l afi sd e f i n e da s # c t ( f ) 一# v a r ( f ) ，d e n o t e db yd ( f ) ac o n j u n c t i o nn o r m a lf o r m ( c n f ) p r o p o s i t i o n a lf o r m u l ai sm i n i m a lu n s a t i s f i a b l e ( m u ) i ft h ef o r u m l ai su n s a t i s f i a b l ea n dt h er e s u l t i n gf o r m u l aa f t e rd e l e t i n g a na r b i t r a r yc l a u s ef r o mt h i sf o r m u l ai sas a t i s f i a b l cf o r m u l a f o rn ，r 1l e t 2c h a p t e r1 i n t r o d u c t i o n c n f ( n ，r ) b ec l a s so fc n f f o r m u l a sw i t hnv a r i a b l e sa n drc l a u s e s g e n e r a l l y , w e c o n s i d e rt h ec l a s so fc ff o r m u l a sf ( k ) = u n 1 c n f ( n ，n + 女) f o r 女1 w h e r e t h ei n t e g e rki sc a l l e dt h ed e f i c i e n c yo ff o r m u l a s c h p a p a d i m i t r i o ua n dd 、 b l f e 【p w 8 8 1s h o w e dt h a ta nu n s a t i s f i a b l ef o r m u l ac a nb et r a n s f c i r m e di n t oam i n i m a l u n s a t i s f i a b l ef o r m u l ai np o l y n o m i a lt i m e l e tm u ( k ) b et h es e to fm i n i m a lu n s a t i s 矗a b l ef o r m u l a si nf ( k ) f o rk 1 i n d d k b 9 8 ，g d a v y d o v ，i d a v y d o v aa n dh k l e i n eb i i n i n gp r o v e dt h a tfi sn o t m i n i m a lu n s a t i s f i a b l ei fd ( f ) 0 w h e t h e ro rn o taf o r m u l af b e l o n g st om u ( k ) c a l lb ed e c i d e di np o l y n o m i a lt i m e k s l 1 1 b a c k g r o u n da n dm o t i v a t i o n t h es a t i s f i a b i l i t yp r o b l e m ( s a tp r o b l e m ) i st od e t e r m i n ef o rag i v e np r o p o s i t i o n a l f o r m u l a ，w h e t h e rt h e r ee x i s t sas a t i s f y i n ga s s i g n m e n t i e ，w h e t h e ri t i sn o te q u i v a - l e n tt of a l s e i no u rp a p e r ，w ec o n s i d e rp r o p o s i t i o n a lf o r m u l a si nc o n j u n c t i v en o r m a l f o r m ( c n f ) s a tp r o b l e mi s t h ef i r s tnpp r o b l e m a n di ti st h ec o r eo fab i g k i n do fn p c o m p l e t ep r o b l e m s 、c 0 0 7 1 i ti sp r o v e di nm a n yf a c t st h a tm a n ynp c o m p l e t ep r o b l e m sh a v ev i t a lm e a n i n gf o rc o m p u t e rs c i e n c e a sw e l la sa p p l i c a t i o n o fp r o j e c t z j 0 0 t h er e s e a r c hf o rm i n i m a lu n s a t i s f i a b l ef o r m u l a si sah o tt o p i co i ls a t p r o b l e m t h a tb e g i n st os u r f a c ei nr e c e n ty e a r s s o m es t r u c t u r e sa n dt r a i t so ft h em i n i m a l u n s a t i s f i a b l ef o r m u l aw i l lb eo fb e n e f i tt ot h er e s e a r c ho ft h ea l g o r i t h m sf o rs o l v i n g s a tp r o b l e m s m u ( 1 ) f o r m u l a sa r et h es e to fm i n i m a lu n s a t i s f i a b l ef o r m u l a sw i t h d 西c i e n c yk = 1 f o r m u l a si nm u ( 1 1h a v eas i m p l es t r u c t u r ea n db ec o n s t r u c t e d i nar e c u r s i v ew a yi d d k b 9 8 t h e r e f o r e ：t h et r a n s f o r m a t i o nb e t w e e nf o r m u l a si n m u ( k ) a n df o r m u l a si nm u ( 1 ) b e c o m e sm o r ei m p o r t a n t a na l g o r i t h mo fs a t c a nd e c i d ew h e t h e ro rn o ta n yg i v e nf o r m u l ai nc nfi ss a t i s f i a b l ei nf i n i t et i m e d p l li sam e t h o df o rt e s t i n gc n f sf o rs a t i s f i a b i l i t y a n yp r o p o s i t i o n a lf o r m u l a ， o rc o n j u n c t i o no fp r o p o s i t i o n a lf o r m u l a si s e q u i v a l e n tt o ( h a st h es a m et r u t ht a b l e a s ) ac o n j u n c t i o nn o r m a lf o r ma n dt h i sc n fc a bb ef o u n da ne f f i c i e n tm a n n e r ( e g s e ec h a p t e r1 2o f 【d s w 9 4 ) ；s od p l l ，c a na l s ob ec o n s i d e r e dam e t h o df o rt e s t i n g p r o p o s i t i o n a lf o r m u l a so rc o n j u n c t i o no fp r o p o s i t i o n a lf o r m u l a s ，f o rs a t i s f i a b i l i t y s o l u t i o n st os o l v es a tp r o b l e mc a nb ed i v i d e di n t ot w ot y p e s ：c o m p l e t ea l g o r i t h m a n di n c o m p l e t ea l g o r i t h m a m o n gt h e m ，t h ed p l la l g o r i t h mf d p 6 0 a n dr e s o l u t i o nr e f u t a t i o ni nt h ec o m p l e t ea l g o r i t h ma r et w om e t h o d o l o g i e sf a i r l y i m p o r t a n t a n dc o m m o na n dt h e ya r ea l s ow h a tw ea r eg o i n gt og i v eas p e c i f i cd i s c u s s i o ni n t h i st h e s i s d p l la l g o r i t h mf i r s tp r e s e n t e db yd a v i sa n dp u t n a m ，w ec a l l e di t j 2 m a i nw o r ka n df u t u r ew o r k 3 d a v i s - p u t n a ma l g o r i t h m ( d e n o t e da sd p ) av a r i a n to fd pa l g o r i t h mi n t r o d u c e d b yd a v i s ，l o g e m a n na n dl o v e l a n d s ow ea l s oc a l l e di td p l la l g o r i t h m r e s o l u t i o nr e f u t a t i o ni sr e g a r d e da st h eg e n e r a l i z a t i o no ft h er u l ef o ru n i tc l a u s ei nd p l l a l g o r i t h m i ti sw e l lk n o w n ( g o l 7 9 ) t h a tap r o o ft h a tac n f i su n s a t i s f i a b l eb ，r d p l lc a nb et r a n s f o r m e dt oar e s o l u t i o nr e f u t a t i o n o f1 i n e a rl e n g t hi nt h es i z e o ft h ed p l lp r o o f i ti sr e f u t ep r o o fm e t h o df o rm i n i m a lu n s a t i s f i a b l ef o r m u l a s a n dt h e r ee x i s t sa ( 1 ，1 ) - r e s o l u t i o np r o o fc o r r e s p o n d i n gt oaf o r m u l ai nm u 0 l g e t v e r e t i n aa n dh a n sz a n t e m ah a v ed e s c r i b e dt h et r a n s f o r m i n gf r o md p l la l g o - r i t h mt or e s o l u t i o n r e f u t a t i o ni nm o r ed e t a i l 【t z a n di m p r o v e dt h a ti fi nt h e d p l lp r o c e d u r esu n i tr e s o l u t i o ns t e p sa r ee x e c u t e da n drr e c u r s i v ec a l l sa r ed o n e ar e s o l u t i o nr e f u t a t i o ne x i s t so fl e n 酗ha tm o s ts r b e i n ge s s e n t i a l l yb e t t e rt h a n sf t z 1 2m a i nw o r ka n df u t u r ew o r k i nt h i st h e s i s ，w ew i l ld i s c u s st h es p l i t t i n gt h e o r e ma n dt h eh o m o m o r p h i s mo fm i n i m a lu n s a t i s f i a b l ef o r m u l a s h k l e i n eb r i n i n ga n dx i s h u nz h a op r o v e dt h a tf o ra n y k ，t 1a n da n yf o r m u l af m u ( k ) t h e r ee x i s t saf o r m u l a 日i nm u ( k ) a n da h o m o m o r p h i s m 圣f r o mh t ofs u c ht h a t ( h ，圣) i sar e p r e s e n t a t i o no ff ，a n dh c a nb ec o n s t r u c t e di np o l y n o m i a lt i m eo ft h el e n 豇ho ff k b z 0 2 w jw i l le x p r e s sac o n s t r u c t i o nm e t h o df o rf o r m u l a si nm ub a s e do nt h es p l i t t i n g t h e o r e m e s p e c i a l l y ，w ec a nc o n s t r u c tac o r r e s p o n d i n gf o r m u l ai nm u ( 1 ) f o ra n y g i v e nf o r m u l af i nm u i nt h i sp a p e r ，w eg i v eaf o r m a ln o t a t i o no ft h et r e e r e s o l u t i o np r o o f w ew i l l i n v e s t i g a t et h eh o m o m o r p h i s mr e p r e s e n t a t i o no fam u ( k ) f o r m u l a s ，i tw i l lb es h o w n t h a tat r e e r e s o l u t i o np r o o fo ffc a nb eg o tf r o mat r e e r e s o l u t i o np r o o fo fh ( h m u ( 1 ) 1b yt h eh o m o m o r p h i s mm ( r 8 ) 一s a ti st h ep 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 e mr e s t r i c t e dt o ( r ，s ) 一c f i ti sk n o w nt h a t ( r ，2 ) 一鲥丁i ss o l v a b l ei np o l y n o m i a lt i m e ( r o ) ，a l li n s t a n c e so f ( r r ) 一s 4 丁a r es a t i s f i a b l ea n dt h e r ee x i s t sac r i t i c a lf u n c t i o n ，s u c ht h a tf o rr 3a l l i n s t a n c e so f ( r ，( r ) ) 一s a ta r es a t i s f i a b l ea n d ( r ，( r ) + 1 ) 一s a ta r e p c o m p l e t e i n t o v 8 4 ，t h ea u t h o r si n t r o d u c e da nu p p e rf u n c t i o n o f ，s u c ht h a t = ，1f o r r = 3 ，4 i nt h i st h e s i s ，w ew i l lg i v ean e we x p r e s s i o no ff lb ys p l i t t i n gt h e o r e ma n d c o n s t r u c tm i n i m a lu n s a t i s f i a b l ei n s t a n c e si n ( r ，s ) s a t f u r t h e r ，w ew i l lp r e s e n t s o m em i n i m a lu n s a t i s f i a b l e p c o m p l e t ei n s t a n c e si nf r s 1 一s a t ，eh a v ek n o w nt h a td p l la n dr e s o l u t i o na r et w oi m p o r t a n tm e t h o df o rs o l v i n gs a t f o ra n yg i v e nf o r m u l af m u ( 1 ) ，t h e r ee x i s t sa ( 1 ，1 ) 一r e s o l u t i o np r o o f , 4 c h a p t e r1 1 n t r o d u c t l o n a n df o r m u l a si nm u ( 1 ) h a st h es i m p l es t r u c t u r e ，a n dc a r lb ec o n s t r u c t e di nr e c u r s i v e r e g i m e i n t z ，t h ea u t h o r sd e s c r i b et h et r a n s f o r m a t i o nf r o md p l lt or e s o l u t i o n w ew i l ls h o wt h et r a n s f o r m a t i o nf r o mr e s o l u t i o nt o ( 1 ，1 ) 一r e s o l u t i o no nt h eb a s i s o fc o n s t r u c t i o nm e t h o do fm i n i m a lu n s a t i s f i a b l ef o r m u l a s ，a n dc o r r e s p o n d i n g l yg e t t i n gat r a n s f o r m a t i o nf r o md p l la l g o r i t h mt o ( 1 ，1 ) 一r e s o l u t i o np r o o f i np o l y n o m i a l t i m e t h e r ei ss t i l lal o to fw o r kt ob ed o n e t h ef i r s to n ei st h a tf o r 西y e nm i n i m a l u n s a t i s f i a b l ef o r m u l a ，h o wt of i n dab e t t e rt r e e - r e s o l u t i o np r o o fb a s e do nt h es p e c i a l c o n s t r u c t i o no fm u ( 1 ) f o r m u l a sa n dt h et r a n s f o r m a t i o nf r o mr e s o l u t i o nt o ( 1 ，1 ) 一 r e s o l u t i o n ；a n o t h e ro n ei sh o wt of i n dt h ee x a c tv a l u eo ff u n c t i o nf 1 3 o r g a n i z a t i o no ft h et h e s i s t h i st h e s i si so r g a n i z e db y5c h a p t e r s c h a p t e r2g i v e ss o m ei m p o r t a n tn o t i o n s w h i c hc o n t a i n st w op r o o fs y s t e m s ( d p l la l g o r i t h ma n d r e s o l u t i o n ) a n dt h em i n i m a l u n s a t i s f i a b l ef o r m u l a s c h a p t e r3d i s c u s ss o m e p c o m p l e t ei n s t a n c e si n ( r ，s ) 一 s a t a n dt h ec o n s t r u c t i o n m e t h o do ft h em i n i m a lu n s a t i s f i a b l ef o r m u l a si n ( r ，s ) s a t c h a p t e r4d e s c r i b et h et r a n s f o r m a t i o nf r o md p l lt o ( 1 ，1 ) 一r e s o l u t i o ni n m o r ed e t a i l c h a p t e r2 p r e l i m i n a r i e s i nt h i sc h a p t e r ，w ew i l lo v e r v i e ws o m eb a s e dd e f i n i t i o n sa n ds e v e r a li m p o r t a n tn o - t i o n sw h i c ha r ed p l la l g o r i t h m ，r e s o l u t i o n ，a n dm i n i m a lu n s a t i s f i a b l ef o r m u l a s 2 1b a s i cd e f i n i t i o n sa n dl e m m a s i nt h i sp a p e r ，t h es y m b o l s ，z ：y ，z ，w i l lb er e f e r r e dt oa sp r o p o s i t i o n a lv a r i a b l e sa n d a r et h es i m p l e s t