（应用数学专业论文）可满足公式到mu（1）公式的扩张.pdf

摘要 经典逻辑中的s a t 问题是指布尔表达式的可满足性问题它是计算机科学中 的核心问题。s a t 问题是n p 完全问题，从理论上说，s a t 问题不能在多项式时间 内解决，它超出了现代计算机的能力。所以，s a t 问题是计算机科学发展中的“瓶 颈”问题，计算机科学家们一直都在寻求各种快速策略和方法试图改进s a t 问题 的求解。 极小不可满足公式的研究是近年来兴起的关于s a t 问题的一个热点方向。一 个c n f 公式( c n f 公式是有限个子句的合取) f 称为极小不可满足的( m u ) ，如果 f 是不可满足，并且在f 中删去任意一个子句后所得到的公式是可满足的。删( k ) 表示子句数与变元数的差为k 的极小不可满足公式的类。k l e i n eb u n i n g h 等人 的研究结果表明：如果k 0 ，则公式不是极小不可满足的，也就是说，所有极小 不可满足公式其子句数必定大于公式中的变量个数。 在本文中，我们将给出一个在多项式时间内判定可满足公式到删( 1 ) 公式 扩张问题的算法。关于公式扩张问题，k l e i n eb u n i n gh 和z h a oxs 已经做出 了若干结果，他们得出：h o r n 公式到椰( 1 ) 公式的扩张问题可在多项式时间内判 定，问题删一e x t e x t = t 为d 9 一难，问题删一e x t e x t = 1 在p n e o 1 之中，问题 姗一e x t e x t = t ，d e f i = k 可在多项式时间内判定，这里记删一e x t e x t = t ， d e l l = k = f e c n f lj g ：f + g e 删( k ) ，v a r ( g ) v a r ( f ) ，i g l = t 。在本论文中， 我们考虑对一个给定可满足c n f 公式f ，是否存在公式g 使得f + g e m u ( 1 ) ( v a r ( g ) v a r ( f ) ) 并给出这个问题的多项式时间判定算法。 关键词：s a t ；k c n f ；极小不可满足公式；公式归约；算法 中图分类号：0 1 4 2文献标识码：a a b s tr 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 n u l l a s i ti sa l le s s c 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 7 1p 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 i 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 r 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 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 l l r e c e n ty e a r saf o r m u l afi nc 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 i u n c t i o no ff i n i t ec l a u s e s ，af o r m u l afi sm i n i m a lu n s a t i s f i a b l e ( m u ) i ff i su n s a t i s f i a b l ea n df 一 c ) 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 e f t 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 r 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 o r m u l a sw i t hd e f i c i e n c y 1 i ti sw e l tk n o w nt h a tfi sn o tm i n i m a l u n s a t i s f i a b l ei fk _ im u ( k ) r o 叫，_ e p r e s 肌t i n gv a r i a b l ea n dc o l u m nr e p r e s e n t i n gc l a u s e ，b y t h 拈w ec n 1 。5 8 ”m 7 1 zt o ，p r s e n tnc n ff o r m u l a t h ef o r m a ld e f i n i t i o ni sa sf o u o w i n 9 d e f i n i t i o n7 ( r e p r e s e n t a t i o nm a t r i xo fnc n ff o r m u l a ) l e f ：i v l ，c k 】b eo f o r m u l aw i t hn a r i a b l e sz l ，z n i nc n f ( n ，m ) t h e n mm n t r i j ：( n ) i sc a l l e dt h er e p r e s e n t a t i o nm a t r i xo ff ，d e n o t e db ym r ，w h 8 ” 旷 三x 篡ie 鬟c jq s o m e t i m e sw ew r i t eb l a n kf o r7 0 7 五拓口m p l e1f ：( z 1 v x 2 ) a ( 一z 1 v x 4 ) a ( 、x 2 v x 3 v x 4 ) a ( ，x 2 v ，x 3 v x 4 ) a ( 1 x 4 v z 5 v z 6 ) a ( 1 。4 v _ 1 $ 5 v 。6 )a ( 一。4 v ，z 6 ) h a s 玑e m 、a t r i x 上 +一一一 +一 h ，0 c t t h ef o r m u f nfn b o ei s 。m i n i m n l “n s a t i s f i 。b i e ，0 m m i a i ni r a 8 6 , ? 上肌“5 k l e i n eb i i n i n 9 s h o w e de v e r wf o r m u l ai nm u c o r r e s p o n dt oaf o r m a lm a t r i x w h i c h i sc o l l e db a s i cm a t r i x ，i t sd e f i n i t i o ni sa sf o l l o w i n 9 d e f i n i t i o n8 ( b a s i cm a t 俐 t h ef o l l o w i n gm a t r i xw i t hnr o w sa n d ( 礼+ 1 ) c o l u m n sd e f i n e di n d u c t i v e l yi s t e r m e dab a s i cm a t r i x ： r j ，( + 一) i sab a s i cm a t r i x ( 2 1u b ki s 口b a s i cm a t r i x , t h e nt h ef o l l o w i n gm a t r i x 证b a s i c ( 言一0 ) w h e r eb li s v e c t o rw i t h ( b 1 ) j o ，+ ) a n da tl e a s to n e + s i g n i 3 ) 对b 2i s nb a s i cm a t r i x , t h e nt h ef o l l o w i n gm a t r i xi sb a s i c 一 ( 言笔) 2j1 1 e e r e s o l u l y o np r 0 0 f w h e r eb 2i sov e c t o rw i t h ( b 2 ) s 0 ，一) a n da tl e a s to n e s i g n 睢) w h e r eb li sav e c t o rw i t h ( 6 1 ) j 0 ，+ ) a n da tl e a s to n e + s i g n ，a n dw h e r eb 2i sn i n r a 8 6 , d d x 8 9 8 ，h a n sk l e i n eb i i n i n gh a sp r o v e dt h ef o l l o u i n gt h e o r e m t h e o r e m2f a f u ( 1 ) 玑a n do n l yi ft h er e p r e s e n t a t i o nm a t r i x 吖fi sab a s i c m a t r i xu pt oap e r m u t a t i o no lr o w sa n dc o l u m n s ? 2 4t r e e r e s o l u t i o np r o o f b a s e d 口nt h es t r u c t u r eo f m u ( 1 ) ，w ei n t r o d u c et r e e r e s o l u t i o np r o o fi nt h i ss e c t i o n i ti sau s e u la p p r o a c hi np r o v i n gt h e o r i e sr e l a t e dt om u ( 1 ) f o r m u l a d e f i n i t i o n9 “l ， ) 一r e s o l u t i o 州 l e tf = 【( l v f ) ，( 一l v 9 1 ) ，( ，l v g p ) ，日】b eac n f f o r m u l a ，w h e r eb c o n t a i n sn e i t h e rln o r l t h ef o r m u l af 7 = 【( ，v9 1 ) ，( fv g p ) ，f r e s di sc a l l e d ( 1 ， ) 一r e s o l v e n to yf f o r p = 1 ，t h e f o r m u l a f 7 = ( ，v 9 1 ) b 】i sc a l l e d ( 1 ，1 ) 一r e s o l v e n t f t h ef o l l o w i n gl e m m as h o w st h a tf o r 1m u ( k ) i sc l o s e du n d e r ( 1 ) 一r e s o l u t i o n l e m m a1l e tf = 【( lv ，) ，( _ 1 lv9 1 ) ，一，( 一lv9 p ) ，日。a t b eam u y o r m u l a ， w h e r eb e “c o n t a i n sn e i t h e rl n o r - l t h e n ，f m u ( k ) ，o rk2 1t ，a n do n l y 矿 f = 【( ，v g a ) ，( ，v 9 p ) ，耳。t 】m u ( k ) p r o o f w i t h o u tl o s so fg e n e r a l i t y f 0 g ，w ea s s u m ef = 【( zv 门，( 、zv 9 1 ) ，_ ，( 1 zv 卯) ，f r e s t 】，w h e r eb e 武c o n t a i n sn e i t h e rzn o r z ，a n df 7 = 【( ，v 9 1 ) ，( ，v 郎) ，b 。“ ( 辛) s u p p o s ef m u ( k ) a n d # v a r ( f ) = n t h e n ，# c l ( f ) = n + k ，# v a r ( f ) = n 一1 ，a n d 弗c f ( f ) = n + k 1 t h u s ，d ( f ) ；k w ew i l ls h o wf m u ( k ) f i r s t l y , f 1i su n s a t i s f i a b l e 聪o t h e r u r i s e 。t h e r ee x i s t sat r u t hn s 甄口n m e n tv3 u c ht h 8 t ( f 7 ) = ：1 i ti m p l i e s ( ，v 9 1 ) 一= ( ，v g v ) = ( f r 。) ：= 1 w ee x t e n d i n t o at r u t ha s s i g n m e n t s u c ht h a t ( f ) = 1a sf o l l o w ： 8c h a p t e r2p r e l i i 1 i n a r i e s ip ( ) i ，y v a r ( f ) z ) ( ) = 0q y = za n dp ( ，) = 1 i 1 i f y = 。a n d ( ，) = 0 c l e a r l y ，7 ( f ) = 1 i ti sc o n t r a d i c tw i t ht h eu n s a t i 币a b i l i t yo ff s e c o n d l y ，f fi sm i n i m a lu n s a t i s f i a b l el jo t h e r w i s e ，t h e r ee x i s t sac l a u s eh f ls u c h t h a tf ) i su n s a t i s f i a b l e w ec o n s i d e rt h ef o u o w i n gc a s e s ： c a s e h = ( fv9 1 ) f o rs o m el isp w 1 0g ，w ea s s u m eh = ( f v a l ) p l e a s en o t et h a tf 1 = 【( x v ，) ，( 、x v 9 2 ) ，( 一。v 如) ，一“】i ss a t i s t i a b l e t h u s w e 。t eat r u t ha s s i g n m e n t s u c ht h a t ( f 1 ) = 1 i ti m p l i e s ( 。v ，) = p ( z v9 2 ) 一= ( _ 1 zvg p ) = p ( b 。) = 1 盯( z ) = 1 t h e nv ( 9 2 ) 一= p ( 卯) = ( f k n ) = 1 可( z ) = 0 ，t h e nv ( ，) = ( f r e s t ) = 1 t h e r e f o r e ，w ea l w a y sh a v e ( f h ) ) = 1 i ti sac o n t r a d i c t i o n c a s e 2 h f r 。m s i n c efi sm i n i m a lu n s a t i s f i a b l e ，f l = ( zv ，) ，( ，zv9 1 ) ，( 一。vg p ) ，群。】i s s a t i s f i a b l e ，w h e r e 只e “= f r e “ ) t h u s ，w eh a v eat r u t ha s s i g n m e n tps u c ht h a t ( f 1 ) = 1 i ti m p l i e s ( z v ，) = ( ，z v9 1 ) 一= ( ，z v9 - ) = p ( 群。“) = 1 巧( z ) = 1 ，t h e nu ( 9 1 ) = = ( 9 p ) = l ，( c 。n ) = 1 i f ( z ) = 0 ，t h e n ( ，) = ( 群。雠) = 1 t h e r e f o r e ，w ea l w a y sh a v e ( f h ) ) = 1 i ti sac o n t r a d i c t i o n ( 乍) s u p p o s ef 7 = 【( f v 9 1 ) ，( f v g , ) ，b 。t m u ( k ) w ew i l ls h o wf m u ( k ) f i r s t l y ，fi su n s a t i s f i a b l ei fo t h e r w i s e ，t h e r ee x i s t sat r u t ha s s i g n m e n t s u c ht h a t ( f ) = 1 i f p ( 茁) = l ，t h e np ( 9 1 ) = ( 卯) = p ( b 。t ) = 1 ，y ( z ) = 0 ，t h e n ( ，) = v ( 耳e s t ) = 1t h e r e f o r e ，w ea l w a y sh a v e ( f ) = 1 i ti sac o n t r a d i c t i o n s e c o n d l y ，fi sm i n i m a lu n s a t i s f i a b l e t fo t h e r w i s e ，t h e r ee x i s t sac l a u s eh fs u c h t h a tf 九) i su n s a t i s f i a b l e w ec o n s i d e rt h e 如l l o w i n gc a s e s ： c a s e2 j h = v ，) p l e a s en o t et h a tb e “i ss a t i s f i a b l e t h u s ，w eh a v eat r u t ha s s i g n m e n t s u c ht h a t ( b e “) = 1 w ec a ne x t e n dvi n t oat r u t ha s s i g n m e n t s u c ht h a tr ( f ) ) = 1 6 8 | o l l o w ： 州沪篆，叮 c a s e2 2 h = ( 一z v 9 1 ) i o rs o m e l i p w 1 0 g ，w ea s s u m eh = ( - 、x v 9 1 ) p l e a s en o t et h a tf l = 【( f v 9 2 ) ，( y v g p ) ，b “】 i ss a t i s f i a b l e t h u s ，w eh a v eat r u t ha s s i 9 r n m e n t s u c ht h a tp ( f 1 ) = 1 w ec a n e x t e n d i n t oat r u t ha s s i g n m e n t s u c ht h a tt ( f 耐) = 1a s 如f l o w ： iv ( f ) 矿g v a r ( f ) z ) 7 ( ) = 0i f y = za n d ( ，) = 1 【1 i f y = za n d ( ，) = 0 24t r e e - r e s o l u l y o np r ( ) ( ) f c a s e2 3 h f r 。m s i n c ef 7i sm i n i m a lu n s a t i s f i n 6 f ef l = ( ，v9 1 ) ，一，( fvg p ) ，f 】i ss a t i s f i a b l c ， w h e r e 只e “= b e 。 ) t h u s ，w eh a v eat r u t ha s s i g n m e n t s u c ht h a tu ( f x ) = 1 w ec a ne x t e n d i n t ot h et r u t ha s s i g n m e n t 7i nc a s e2 2 w eh a v e ( f h ) ) = l d e f i n i t i o n1 0 i n t r e ea n dr e g u l a rb i n a r yi n t r e e 3 ( i 3ad i r e c t e dg r a p ht 话a nm t r e e 寸 f1 1 ) t h eu n d i r e c t e dg r a p ht h a tu n d e r l i e sti sat r e e ； r 到t h e r ei se x a c t l yo n ev e r t e xt o v ( t ) w i t hd e g i ( v o ) ， w es a yt h a tv o i st h er o o t o | t ： r 圳d e g i nv ) = 1 ，d ra l lu v ( t ) e x c e p tt h er o o to f t f o r y ( t ) ，vi sc a l l e dal e 4o f t 矿d e g o 。t ( v ) = 0 w ed e n o t el e a f ( t ) = v ( t ) l d e g 。# v ) = o ) a n d ( 丁) = v ( t ) l e o f ( t ) ，a n d u k ni sc a l l e di n v e r t e x f 剀a ni 竹一t r e et i sar e g u l a rb i n a r yi 竹- t r e e 妒d e g o u t ( v ) = 2f o ra l lu v n ( t ) d e f i n i t i o n1 1 ( r e s o l v e n tc l a u s e ) l e tc 1a n dqb et w oc l a u s e s ，i ft h e r ei se x a c t l yo n el i t e r a lls u c ht h a t 工c 1a n d 、l c 2 ，t h e nz o ec a l lt h ec l a u s ec = ( c 1 一 l ) ) u ( c 2 一 、l ) ) t h er e s o f 7 e n to fc 1 a n d go n la n dd e n o t elb yr ( c ) d e f i n i t i o n1 2 ( t r e e r e s o l u t i o np r o o f ) l e tfb eai o r m u l a ，tar e g u l a rb i n a r yi n - t r e e ，a n daav e r t e x - l a b e l l i n gw h i c h a s s i g nt de v e r yv e r t e xv v ( t ) ac l a u s e t h et r i p l et = ( t ，a ，f ) i sat r e er e s o l u t i o n p r o o l 矿 “，入( ”o ) = f o r t h er o o tv oo y t j r 纠a ( u ) fy o rv l e a f ( t ) ； f 圳f o rv k n 口) a n dt h e8 t t c c e s s o r su 1 ，坼0 ， 一印一c h i l da n dr i g h t - c h i l do f 口，i f a ( ) i sar e s o l v e n to fa ( u 1 ) a n da ( t - ) b o t ht h er e p r e s e n t a t i o nm a t r i xa n dt r e e r e s o l u t i o np r o o fa r ei m p o r t a n tt o o lt os t u d y t h es t r u c t u r eo st h ef o r m u l ai nm u i nn e x ts e c t i o nw ew i l lu s eb o t ho it h e m c h a p t e r3 b a s i cr e s u l to nm u ( 1 ) i nt 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 ma n d p r e s e n tt h r e ei m p o r t a n tt h e o r i e st h a tw i l lb eu s e di nn e x tc h a p t e r 3 1 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 i nt h i ss e c t i o nw ew i l lp r e s e n tas e q u e n c eo ls i m p l ef a c t so nm i n i m a lu n s a t i s i a b l e f o r m u l a s f i r s t l y ，w eh a v et h ef o l l o w i n gs i m p l er e s u l t s 1 ) ai o r m u l aw i t ht a u t o l o g i c a lc l a u s e so rd o u b l eo c c u r r e n c e so fc l a u s e si sn o t m i n i m a lu n s a t i s f i a b l e f 2 1 i i av a r i a b l eo c c u r so n l y p o s i t i v e l yr e s p jn e g a t i v e l yt h e nt h e f o r m u l ac a n n o tb em i n i m a lu n s a t i s f i a b l e t h u se a c hv a r i a b l eo c c u r s 讥t h ef o r m u l a a tl e a s to n c ep o s i t i v e l ya n da tl e a s to 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 f 3 ) af o r m u l a fi 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 yp a i ro fu n i t c l a u s e s a n ds o m ea d d i t i o n a lc l a u s e s 4 ) i nc a s eo fau n i t c l a u s e sa n daf a r t h e rc l a u s ew i t h l i t e r a llo rn oc l a u s ew i t hl i t e r a l - , lt h ei o r m u l ai sn o tm i n i m a lu n s a t i s f i a b l e i nt h i sp a p e rw ei n t r o d u c ean o t i o nc it od e s c r i b et h ec h a r a c t e ro f m u f o r m u l a t h es o r m a ld e f i n i t i o ni sa sy o u o w i n g ： d e f i n i t i o n13l e tfb eacnff o r m u l a 时fs a t i s f i e st h ei o l l o w i n gc o n d i t i o n ： v ，f ：f 一 ，) f t h e nw es a yfi sc l a u s e i n d e p e n d e n t d e n o t et h ec l a s so fc l a u s e i n d e p e n d e n tl o r m u f a sa s ： c i = f c n f v f f ：f 一 ，) ，) i ti se a s yt oc h e c kt h a ti faf o r m u l ai su n s a t i s f i a b l ea n d 伽c it h e n 琥ef o r m u l ai s m i n i m a lu n s a t i 妒a b l e ，ie u n s a tnc i m u 3 21 1 w ob a s i cr e s u u l lo n ，f 1 1 3 2t w ob a s i cr e s u l to nm u ( 1 ) t h e o r e m3l e tfb ea | o r m u l ai nm u ( 1 ) ， f ，ie v f ，g f ，w eh a v e # h i t ( f g ) s1 、l 9 ) 1 w h e r eb o t hfa n dga r ec l a u s e s ) l l t h e n | o fa n yt w od i s t i n c tc l a u s es ，g 停h i t ( f ，g ) = j v a r ( l ) ：l ，a n d p r o o f ：b a s eo nt h eb a s i cm a t r i x ，w ep r o v et h i sp r o p o s i t i o ni n d u c t i v e l y e a s e l t h ef o r m u l ah a v et h ei o t t nf = f + 一) | 1 lt h i sc a s e fh a v eo n l yt w oc l a u s e sta n d z o b v i o u s l yw eh a v et h a t # h i t ( x ，、z ) sl e 。：吼e 如m u 托胁e 舭如伽肚b t 一0 1 w h e r eb li s 。v e c t o rw i t h ( b o j o ，+ ) a n da tl e a s to n e + s i g n s i n c eb l 0 ，+ ，t h en u m b e r h i tv a r i a b l e sc a n n o tb ei n c r e a s e d ( ：?) ，s 。”es 缸“n n ”e t n n t 群日t t c ，s n e ”，( ：? m 疏ed 蛐s m 盯( b 。，1 0 ) ，琥e 一匆，”瓤w e 琥耐把以幻轨e 饥c 他i 哪0 ，觚t n “m s e r 。c c “r 打。琥er o ”( b l , - ) , b u ti nt h ec o l u m n ( ：) b e s i d e - a n o t h e rs i g n i s0 ，s oi t 0i m p o s s i b l et h a tt h en u m b e ro fh i tv a r i a b l e si n c r e a s i n gb e t w e e nt h ec l a u s e s 盯( 嚣) 删舭妇e ( ：) 砌c e w eh a v et h a t # h i t c 川q 翰”舅托加r m u l a h a v e t h e f o m 尸= ( 言岛b 2 ) w h e r e b 2i sav ”如r 研加( 6 2 ) ， 0 ，一) a n da tl e a s to n e s i 9 n i nf a c t ，t h i sc a s es i m u l a t et h ee a s e i t se a s yt og i v et h ep r o o fo ft h i sc a s eb ys i m u - l a t i n ge a s e2 h e r ew ew o n tg i v et h ep r 0 0 1 c a s e 。：孤。，。地。t h ef o r mf = ( b 。1 1 。他。i 。鲥。，。溉 0b 2 ( b t ) j o ，+ ) a n da tl e a s to n e + s i g n ，a n dw h e r e5 2 i sav e c t o rw i t h ( b 2 ) j o ，一) a n da tl e a s to n e s i g n w ec l a i mt h a t 存, h i t 郎一o ，( ：) 。r ( 言) r e s p e c t i v e l y s i n c ei nt h ec l a u s e ( ) n 竹a ( b 。1 ) b e s i d et h ev e c t o rb t , 。， 淞0de玩 m、 321 1 u7 0b a s i cr e s u l to nm u ( 1 )1 3 c a s e 2 l = 1 i nt h i sc a s e ，t h et r e e r e s o l u t i o np r o o f th a v eo n l yt w ol e a v e s 。a n d ，z ，l e tl e a f ( t ) = ft h e nf=za ，zi sam i n i m a lu n s a t i s f i a b l ef o r m u l a n o ww ec a na s s l t m et h e c o n c l u s i o ni ss a t i s f i e d 讥c a s eo f l e = n 一1 ，i e ，矿l e = n lt h e n t h e o m l u l a f 7 = l e a f ( t ) i sam i n i m a lu n s a t i s f i a b l e 如r m u l a c a s e 22m l = n f i r s t l y ，w ep i c kal e a fuw h o s ep a t ht ot h er o o tui sl e n g t hn ，i e ，l e ( u ，u ) = n ， b yd e f t n i t i o no | t r e e r e s o l u t i o np r o o f , w eh a v et h a tt h e r ee x i s tal e a fuw h o s e | t h e r i ss o r a et ot h el e n ，“，a n dt h e r ee x a c t l yi so n el i t e r a lls u c ht h a tl a ( u ) a n d l a ( 2 f7 ) b yl e m m aja n dt h ea s s u m i n g 伽c a s e 2 ，w eh a v et h a tf = ( f 7 一 a ( 1 f ) a ( 1 l ) ) ) u ( 工，a ( u ) ) ，( l ，a ( “) ) ) i sm i n i m a lu n s a t i s i a b l e e x a m p l e2 一6 ) ( 3 v 9 7 ) 0 叫2 扎“j c o n s i d e rt h ef o r m u l af = 【( y 4 v y l ) ，( 一玑v 一2 ) ，( y 2 v y l ) ，( y 6 v y s ) ，( 一l v ，( 一5 v ，7 ) ，( 、1 v ，9 3 ) i n m u ( 1 ) ，i 如t r e e r e s o l u t i o np r o o f i sa s ，d f - f i g u r e1 c h a p t e r4 t h ee x t e n s i o no fc n f i nt h i sc h a p t e r , w eb e g i nt os o l v et h ep r o b l e mo fe z t e n d i n 9nc n ff o r m u l as t e pb y s t e p 4 1c a s e la n dc a s e 2 f i r s t l yw eb e g i nw i t hn o t t n a lf o r m u l a t h es t r u c t u r eo ft h ef o r m u l ai sd e s c r i b e d a s t h e o l l o w i n ge a s e c a s e lf o r y x v a r ( f ) ，o c c ( x ，f ) ( 1 1 ) 2 ep o s ( x ，f ) lo r n e g ( x ，f ) 1 t h e ，0 l l o w i n gp r o p o s i t i o nc a ng i v eu st h e a n s w e r t h e o r e m6l e tfb eas a t i s f i a b l ec n ff o r m u l aa n dg nf o r m u l as u c ht h a tf + g m u ( 1 ) w i t hv a t ( g ) v a r ( f ) n e n t h e r ee x i s tov a r i a b l ezi nfs u c ht h a t o c c ( x ，f ) s