（计算机应用技术专业论文）极小不可满足公式在cnf公式类归约中的应用.pdf

摘要 经典逻辑中的s a t 问题是指布尔表达式的可满足性问题，它是计算机科学中 的核心问题。s a t 问题是n p 完全问题，从理论上说，s a t 问题不能在多项式时 间内解决，它超出了现代计算机的能力。所以，s a t 问题是计算机科学发展中的 “瓶颈”问题，计算机科学家们一直都在寻求各种快速策略和方法试i 訇改进s a t 问题的求解。 一个c n f 公式是有限个子句的合取，k c n f 是子旬长度不超过t 的公式类， k s a t 就是判定给定的k c n f 公式是否有可满足的解。众所周知，2 一s a t 问题 是线性时间可解的，而k s a t 问题是n p 完全的。近年来，寻找k s a t 的最优 算法一直没有停止过。最新研究结果表明改进的关于t s a t 的指数时间算法的 复杂度随i 的递增而增加。在文献 i p 9 9 中，r i m p a g i l a z z o 和r p a t u r i 定义了 一个参数一i n f 6 i 存在解决t s a t 的复杂度为0 ( 2 “) 的算法) ，同时，还证明 了在关于t s a t 有指数时间算法的假设下，仅 是一个关于k 的递增序列。于是， 在文献 i p 9 9 中，提出了一个公开问题：如何有效的将k c n f 类公式归约为 f c n f 类公式( t t k ) 。可以看出，解决上述问题对于k s a t 问题的研究有重要 意义。 极小不可满足公式的研究是近年来兴起的关于s a t 问题的一个热点方向。一 个c n f 公式，称为极小不可满足的( m u ) ，如果f 是不可满足，并且在f 中删去 任意一个子旬后所得到的公式是可满足的。m u ( 七) 表示子句数与变元数的差为女 的极小不可满足公式的类。极小不可满足公式的一些结构和性质将有助于研究 c n f 公式类之间的归约。 本文首先提出了一个从c n f 公式归约为3 - c n f 类公式的新算法，与现有的 经典算法相比，我们的新算法在归约过程中需引入的变元更少。然后，我们通过 构造合适的极小不可满足公式，缛到一个将k c n f 类公式归约为f c n f 类公式 ( f t k ) 的有效算法。对于固定的女，t ( 3 s f t k ) ，我们可以在关于公式f 的长度的线 性时间内将个k c n f 类公式f 归约为t c n f 类公式f 。 关键词：s a t ；女一c n f ；极小不可满足公式；公式归约；算法 中图分类号：0 1 4 1 1 文献标识码：a a b s t r a c t s a tp r o b l e mi nc l a s s i c a ll o g i cm e a n st h es 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 i ti sa l le s s e n t i a lp r o b l e mo fc o m p u t e rs c i e n c e s a tp r o b l e mb e l o n g st ot h e pc l a s s ，t h a ti s ，t h e o r e t i c a l l yi tc a n tb es o l v e di np o l y n o m i a lt i m ea n ds o l v i n gi t e x c e e d st h ec a p a b f l i t yo fm o d e r nc o m p u t e r t h e r e f o r e ，s a tp r o b l e mi st h ec h o k e p o i n ti nt h ed e v e l o p m e n to fc o m p u t e rs c i e n c e ，c o m p u t e rs c i e n t i s t sa t et r y i n gt of i n d v a r i o u sk i n d so fs t r a t e g i e sa n da p p r o a c h e st os o l v ei ta l lt h ew h i l e a f o r m u l a f i nc o n j u n c t i v e n o r m a l f o r m ( ) i s a c o n j u n c t i o n o f f i n i t ec l a u s e s ， k c n fi st h ec l a s so ff o r m u l a s i nw h i c ht h el e n g t ho fe a c hc l a u s eo fe v e r yf o r m u l a i sl e s st h a nk t h ep r o b l e mk s a ti st od e t e r m i n ew h e t h e rt h eg i y e nk 口啊 f o r m u l ah a sas a t i s f y i n gs o l u t i o n i ti sw e l lk n o w nt h a tt h ep r o b l e m2 - s a ti s s o l v a b l ei nf i n e a rt i m e w h i l et h ep r o b l e mk - s a ti ss t f f in p c o m p l e t e i tm a y r e q u i r ee x p o n e n t i a lt i m et os o l v ek - s a tf o rk 3 i n 【i p 9 9 ，i m p a g l i a z z oa n d p a t u r id e f i n eap a r a m e t e r8 k = t ， 6it h e r ei sa n0 ( 2 “) a l g o r i t h mf o rs o l v i n g 一 s a t ，a n di n t r o d u c et h ee x p o n e n t i a l - t i m eh y p o t h e s i s ( e t h ) f o rk - s a t ：f o r k 3 ，8 女 0 i no t h e rw o r d s ，f o rk 3 ，k - s a td o e sn o th a v eas u b e x p o n e n t i a l t i m ea l g o r i t h m i na d d i t i o n ，t h e ys h o wt h a t 轧) i sa ni n c r e a s i n gs e q u e n c eu n d e r t h ea s s u m p t i o ne r 日f o rk - s a t i n i p 9 9 1 ，o n eo ft h eo p e np r o b l e m si sh o wt o e f f e c t i v e l yr e d u c ek c n ft ot c n f i tc a nb es e e nt h a ts o l v i n gt h i sp r o b l e mw i l l b eh e l p f u lf o rt h er e s e a r c ho fk - s a r r e s e a r c ho nm i n i m a lu n s a t i s f i a b l ef o r m u l ai sah o tt o p i co ns a tp r o b l e mt h a t b e g i n st os u r f a c ei nr e c e n ty e a r s af o r m u l af i sm i n i m a lu n s a t i s f i a b l ef m u ) i ff i su n s a t i s f i a b l ea n df f g ) i ss a t i s f i a b l ef o ra n yc l a u s eco ff t h ed 币c i e n c y o faf o r m u l afi sd e f i n e da st h em a l - g i nb e t w e e nt h en u m b e ro fc l a u s e so ffa n d t h en u m b e ro fv a r i a b l e so c c u r r i n gi nf ，w ed e n o t em u ( k ) a st h es e to fm i n i m a l u n s a t i s f i a b l ef c l r m u l a sw i t hd e f i c i e n c yk 1 s o m es t r u c t u r e sa n dt r a i t so ft h e m i n i m a lu 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 d u c t i o no ff o r m u l a s i nt h i st h e s i s a na l g o r i t h mf o rr e d u c i n gc n ft o3 - c i sp r e s e n t e d c o m p a r e d w i t haw e l l - k n o w na l g o r i t h m o u ra l g o r i t h mn e e d sl e s sv a r i a b l e st ob ei n t r o d u c e d d u r i n gt h er e d u c t i o n b yc o n s t r u c t i n gp r o p e 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 ，w e i n t r o d u c ea ne f f e c t i v ea l g o r i t h mf o rr e d u c i n gk - c n ft ot 一凹矿f o rt h ef i x e d a n d t ( 3 3 ) ，b yi n t r o d u c i n g ( p 一3 ) d e wv a r i a b l e sy l ，y 2 ，一，如一sa n dc o n s t r u c t i n g0 2 ) c l a u s e s ( 工1v 三2v y 1 ) ，( l 3 v ，1 v 耽) ，( l p 一2 v 、i 一4 vy p 一3 ) ，( l p 一1 vl p v _ 1 一3 ) ，w ec a nr e d u c ea c n ff o r m u l a t oa3 - c n fo n e i n f a c t ，y l a ( 一掣1 v y 2 ) a a ( ，蜘一4 v 跏一3 ) a 一蜘一3 i sam u ( 1 ) f o r m u l a i ti st h a tam u ( 1 ) f o r m u l ai sc o n j o i n e di n t oc i nt h i st h e s i s ，b a s e do nt h ec h a r a c t e r i z a t i o no 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 ep r e s e n tan e wa l g o r i t h mf o rr e d u c i n ga f o r m u l at oa3 - c n ff o r m u l a i n t h ea l g o r i t h m ，f o rac l a u s ecw i t hn ( 3 ) l i t e r a l s ，w ei n t r o d u c eo n l y 翻n e w v a r i a b l e s ，w h i c hi sm u c hf e w e rt h a nt h a to ft h ea b o v ea l g o r i t h m a d o p t i n gt h e s i m i l a ra p p r o a c h ，b yc o n s t r u c t i n gt h ep r o p e rm i n i m a lu n s a t i s f l a b l ef o r m u l a s ，w e p r e s e n ta ne f f e c t i v ea l g o r i t h mf o rr e d u c i n gk ( 珧ft ot c n f f o rt h ef i x e d 奄a n dt ( 3 t 1i sa ni n c r e a s i n gf u n c t i o no fka n d a p p r o a c h e s7 i 2 6 1 ，6 4 4 i n i p 9 9 ，i m p a g l i a z z oa n d p a t u f id e f i n eap a r a m e t e r 讯= i n f 5t h e r ei sa n0 ( 2 “) a l g o r i t h mf o rs o l v i n gk 一黝t ) ，a n di n t r o d u c et h ee x p o n e n t i a l t i m eh y p o t h e s i s ( e t h ) f o rb 姒t ：f o rk 3 ，8 k 0 i no t h e rw o r d s ，f o rk 3 ，k - s a td o e sn o t h a v eas u b e x p o n e n t i a lt i m ea l g o r i t h m i m p a g l i a z z oa n dp a t u r is h o wt h a t s k ) i s a ni n c r e a s i n gs e q u e n c eu n d e rt h ea s s u m p t i o ne t hf o rk - s a t ，t h u sr e d u c i n gt h e c l a s s 一c n fo ff o r m u l a st ot h ec l a s st - c n fo ff o r m u l a sf o r 0 i n 【i p 9 9 1 ，o n eo ft h eo p e np r o b l e m si s h o wt oe f f e c t i v e l yr e d u c ek 一钾t ot - c a t c h a p t e r3 m 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 i n t h i sc h a p t e r ，w ew i l lg i v ea no v e r v i e wo ft h em i n i m a lu n s a t i s f i a b i l i t yp r o b l e m a n dp r e s e n tf o u ri m p o r t a n tm i n i m a lu n s a t i s f i a b l ef o r m u l a st h a tw i l lb eu s e di nn e x t c h a p t e r 3 1b a s i cd e f i n i t i o n s d e f i n i t i o n9 ( m i n i m a lu n s a t i s f i a b l e o v m u l a ) l e tfb eac n ff o r m u l a fi sc a l l e dm i n i m a lu n s a t i s f i a b l e 矿 ( 1 ) fi su n s a t i s f i a b l ea n d ( 2 ) | o ra n yc l a u s e c f 。f 一、话s a t 诂f i a b l e i no t h e rw o r d s ，m i n i m a lu n s a t i s f i a b l em e a n st h a tt h ef o r m u l ai su n s a t i s f i a b l e a n dd e l e t i n ga na r b i t r a r yc l a u s er e s u l t sas a t i s f i a b l ef o r m u l a t h ep r o b l e mw h e t h e ra p r o p o s i t i o n a lf o r m u l a i nc o n j u n c t i v en o r m a lf o r mi sm i n i m a lu n s a t i s f i a b l ei sk n o w n t ob ed p c o m p l e t e d pi st h ec l a s so fp r o b l e m sw h i c hc a l lb ed e s c r i b e d 明t h e d i f f e r e n c eo ft w on p - p r o b l e m s l e tfb eaf o r m u l aw i t hl i t e r a ll t h e n 丑l ：1 】r e s p e c t i v e l y ( r e s p ) 研l ：0 】i s t h ee m p t yc l a u s eu i ffc o n t a i n st h ec o m p l e m e n t a r yu n i t c l a u s e slr e s p 、l o t h e r w i s e t h ef o r m u l ai st h er e s u l to fd e l e t i n ge a c hc l a u s ew i t hl i t e r a llr e s p ，三 a n dr e m o v i n g “t h eo c c u r r e n c e so f lr e s p l t h a tm e a n sw es e tl=1r e s p l = 0a n ds i m p l i f yt h ef o r m u l af 臼谬m ，m ) d e n o t e st h es e to ff o r m u l a si nc o n j u n c t i v en o r m a lf o r m o v e rnv a r i a b 】e sa n dmc l a u s e s 1 4 3 2 ji m p o r l l a n ts t a t e m e n t so nmuf o r m u l a s 3 2 i m p o r t a n ts t a t e m e n t so nm u f o r m u l a s 1 5 i nt h i ss e c t i o n ，w ew i l lp r e s e n tas e q u e n c eo fs i m p l ef a c t so nm 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 da ni m p o r t a n tl o w e rb o u n do nt h en u m b e ro fc l a u s e sf o rm i n i m a l u u s a t i s f i a b l ef o r m u l a s a tf i r s t ，w el i s ts e v e r a lk i n d so ff o r m u l a st h a tc a nn o tb em i n i m a lu n s a t i s f i a b l e 。 s u p p o s efb eam i n i m a lu n s a t i s f i a b l ef o r m u l aw i t hat a u t o l o g i c a lc l a u s ec ，b y t h ed e f i n i t i o no fm u ，fi su n s a t i s f i a b l ea n df 一 四i ss a t i s f i a b l e ，b u ts i n c eci s at a u t o l o g i c a lc l a u s e ，t h e nf 一 a a n dfi ss a t i s f i a b i l i t y - e q u i v a l e n t ，f 一 g ) i s u n s a t i s f i a b l e ，i ti sac o n t r a d i c t i o n s o ，w ec a ng e t ： f a c t1a 如r m u l a 删耽t a u t o l o g i c a lc l a u s e s 妇n o tm i n i m a lu n s a t i s f i a b l e s i m i l a r l y ，w eh a v e ： f a c t2a o r m u l aw i t hd o u b l eo e c u l t e n c e 8o fc l a u s e si sn o tm i n i m a lu n s a t i s f i a b l e s u p p o s ef b eam i n i m a lu n s a t i s f i a b l ef o r m u l aw i t hav a r i a b l ezo c c u r r i n go n l y p o s i t i v e l y , w i t h o u tl o s so fg e n e r a l i t y , w el e tci st h ec l a u s et h a tc o n t a i n i n gz ，i t i sc l e a rt h a ti na n ya s s i g n m e n tt h ec l a u s et h a ti n d u c e sfb eu u s a t i s f i a b l ec a n tb e g ( 帆j u s ta s s i g n1t o 。) ，t h e nf 一 四i ss t i l lt m s a t i s f i a b l e ，w h i c hc o n t r a d i c t st h e d e f i n i t i o no fm i n i m a lu n s a t i s f i a b l e ，s o ，w eh a v e ： f a c t3l | av a r i a b l eo c c u r 3o n l yp o s i t i v e l yr a s p n e g a t i v e l yt h e nt h ef o r m u l ac a n n o t b em i n i m a lu n s a t f i a b l e t h u se a c hv a r i a b l eo c c u r si nt h ef o r m u l aa tl e a s to n c ep o s i t i v e l ya n da tl e a s t o n c en e g a t i v e l yi nd i s t i n c tc l a u s e s n e x t ，w ec o n s i d e rt h ec a s eo fu n i t - c l a u s e s f a c t4al 。r m u l aft sn o tm i n i m a lu n s a t i s f i a b l e 姑fc o n t a i n sac o m p l e m e n t a r y p a i ro yu n i t - c l a u s e sa n ds o m ea d d i t i o n a lc l a u s e s f a c t5a i o r m u l af i sn o tm i n i m a lu n s a t i s f i a b l e ，fc o n t a i n sau n i t - c l a l l b ela n d a 血r t h e rc l a u s ew i t hl i t e r a ll o rn oc l a u s e 砸晓l i t e r a l l ， i nt e r m so ft h er e d u c t i o nf t l = , 】w eh a v et h ef o l l o w i n gl e m m a l e m m a1 d d k b 9 8 ( u n i t r e s o l u t i o 叫 f o r n 1a n ds o m e ml e t fb ea y o r m u l a 铆c n f ( n ，m ) 玎fc o n t a i n sau n i t c l a u s e l ，n oo t h e rc l a u s ew i t hl i t e r a ll ，n ou n i t c l a u s e 一工，a n da tl e a s to n ec l a u s ew i t h l i t e r a l l t h e nw eh a v e ： fi sm i n i m a lu n s a t i s f i a b l e 玎a n do n l y ，f 【l ；1 1 c n f ( n 1 ，m 一1 ) a n d 目l ：1 1i s m i n i m a lu n s a t i s f i a b l e e h a p t e r3 m i n i m a lu n s a t i s f l a b l ef o r m u l a s i fav a r i a b l eo c c u r so n c ep o s i t i v e l ya n do n c en e g a t i v e l yt h e nb ym e a n so fr e s o - l u t i o nw ec a nr e d u c et h en u m b e ro fv a r i a b l e sa n dt h en u m b e ro fc l a u s e s i ti se a s y t og e tt h ef o l l o w i n gl e m m a l e m m n2 d d k b 9 8 ( r e s o l u t i o nr u l e ) f o rf c n f ( 伸+ 1 ，m + t ) a n dav a r i a b l ezo c c u r r i n ge x a c t l yo n c ep o s i t i v e l ya n d o n c en e g a t i v e l yi nf t o eh a v e ： f = 【扛v ) ，( 、z v ，2 ) ，3 ，一，k + 1 i sm i n i m a lu n s a t i s f i a b l ei ，a n do n l y ，r = ( ，1v 2 ) ，3 ，厶+ 1 c n f ( 礼，m ) i sm i n i m a lu n s a t i i a b l e t h ei n v e r s eo p e r a t i o no ft h er e s o l u t i o nr u l ei st h es p l i t t i n gr u l e w es p l i ta c l a u s ei n t ot w oc l a u s e sb yi n t r o d u c i n g8n e wv a r i a b l e 。a n db u i l d i n go n ec l a u s ew i t h l i t e r a lza n do n ec l a u s ew i t hl i t e r a l - 1 z l e m m a3 d d k b 9 8 ( s p l i t t i n 9r u l e ) l e tf = 【( l 1 v v 饥) ，2 ，一，厶】b eam i n i m a lu n s a t i s f i a b l ef o r m u l ai nc n f ( n ，m ) a n dznn e r ov a r i a b l e t h e n f + = 【( 三 ，v v 厶：v 。) ，( v 岛。v - v 如) ，五，- 一，二】c n f ( n + l ，m + 1 ) 括 m i n i m a lu n s a t i s f i a b l ey o r n ，如，j 1 ， ) = l ，耐 l e m m a4 d d k b 9 8 ( n e wl i t e r a lr u l e ) l e tf = 【，1 ，一，k 】b eam i n i m a lu n s a t i s f i a b l ef o r m u l a 伽c n f ( n ，m ) ，d rs o m en a n dm ，凡ral i t e r a lll e tf + = 【( 1vl ) ，2 ，厶 b eu n s a t i s f i a b l e ，t h e nf 拈 m i n i m a lu n s a t i s f i a b l e t h ef o l l o w i n gt h e o r e ms t a t e sa ni m p o r t a n tl o w e rb o u n do nt h en u m b e ro f c l a u s e s f 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 ： t h e o r e m4 口l 8 6 , d d k b 9 8 可f c n f ( n ，r ) a n dr n ，t h e nf i sn o tm i n i m a lu n s a t i s f i a b l e f o raf o r m u l af c n f ( n ，n + k ) 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 b e c a u s e o ft h e o r e m4 ，w ea l w a y sa s s u m e 女1 w ed e n o t e m u ( k ) = f c n f ( n ，n + ) if i sm i n i m a lu n s a t i s f i a b l e a n d m u = f 1 fi sm i n i m a lu n s a t i s f i a b l e = u k lm u ( k ) t h e o r e m5 d o k b 9 8 l e tfb edf o r m u l a 讥m u ( 1 ) t h e nt h e r e