（基础数学专业论文）关于（ks）sat临界函数上下界的研究.pdf

摘要 僻，s ) 一s a t 是命题满足性问题限制在一类特殊的命题公式上，该命题公式具有每个子句 只有k 个不同的文字且每个变元出现的次数少于s 次的特点。已经验明对于正整数k ，s ， 存在一个指数函数，满足：对任意s s ，作) ，所有的( 女，5 ) 一s a t 例都是可满足的，而 ( 七，) + 1 ) 一s a t 却是一个n p 一完全问题。于是我们称，( ) 为关于仲，s ) 一s a t 的临界函数。 到目前为止，只知道，( 3 ) 和，( 4 ) 的精确值。对于，( ) 是否可计算是一个仍未解决的问题a 因此，对该l 临界函数的上下界研究是具有理论意义的。目前，关于，( ) 的最好上下界分别为 q ( 才k ) 和d ( 矿扩) ，其中a l o g ；一i - - 0 2 6 。 由于每个满足某种条件的数值序列( 阶梯序列) 对应一个h f u ( 1 ) 中的公式，在文献 s s 中，s h o o r y 和s s e z i d e r 通过对数值序列的运算来构造化j ) 一c n f 中的删( 1 ) 公式例， 从而得到了函数，( ) 的可计算上界函数。但该方法是不确定的且不太实用。 本文主要有以下两方面贡献： ( 1 ) 在临界函数的上界方面，基于文献 s s 的思想，本文提出了一个树规则以及基于 该规则的计算上界的确定性算法。该树规则可以显著的减少阶梯数值序列的计算步骤，这使 得新算法比文献 s s 的算法更实用。而得到的界却能接近文献 s s 所得的。此外，运用该算 法，得到了一些n p 一完全问题类。 ( 2 ) 在临界函数的下界方面，本文提出了一个随机算法。对于任意一个( 七，8 ) 一c n f 中 的公式，该算法能随机产生一个赋值。再通过运用概率方法( p r o b a b i l is t i cm e t h o d ) 及局 部引理( l o v d s zl o c a ll e m m a ) ，本文证明了，对任意，+ ) 一c n f 中的公式，如果该公式的子 句数小于。5 8 去2 ，则公式是可满足的。同时还得到了临界函数，( ) 的新下界 q ( j 去批卜 关键词：s a t ，( t ，s ) 一c n f ，极小不可满足公式，概率方法，随机算法 中图分类号0 1 4 2 a b s t r a c t ( k ，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 l ep r o b l e mr e s t r i c t e dt oi n s t a n c e sw h e r ee a c h c l a u s eh a se x a c t l y 七d i s t i n c tl i t e r a l sa n de v e r yv a r i a b l eo c c u r sa tm o s t8t i m e s i ti s k n o w nt h a tt h e r ee x i s t sa ne x p o n e n t i a lf u n c t i o n ，s u c ht h a tf o r8s ，( 七) ，a l l ( 七，s ) 一 s a ti n s t a n c e sa r es a t i s f i a b l e ，b u t ( 七，( 七) + 1 ) 一s a ti sa l r e a d yn p - c o m p l e t e ( k 3 ) w et e r m ，( ) c r i t i c a lf l m c t i o n e x a c tv a l u e so f ，a r eo n l yk n o w nf o rk = 3a n d = 4 ，a n di t so p e nw h e t h e r ，i sc o m p u t a b l e t h u s ，t os t u d yt h eb o u n d so ff ( k ) i s o ft h e o r e t i c a lr e s e a r c hs e n s e s t h eb e s tk n o w nl o w e ra n du p p e rb o u n d so nf ( k ) a r e a ( 2 2 后) a n d0 ( 2 2 k o ) ，w h e r e = l o g j 一1 0 2 6 ，r e s p e c t i v e l y i nf s s ，s h o o r ya n ds s e z i d e ro b t a i nac o m p u t a b l eu p p e rb o u n df u n c t i o nf o r ，( 尼) ( 3 ) t h ea p p r o a c hi st oc r e a t es o m ei n s t a n c ei n ( k ，s ) 一s a tb yc a l c u l a t i n gs t a i r w a y s ，w h i c hc o r r e s p o n dt oc o n s t r u c t i n gs o m ed e s i r e dm 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 t hd e f i c i e n c yo n e h o w e v e r ，t h ec a l c u l a t i o nf o rs t a i r w a y si sn o n d e t e r - m i n i s t i c i ti sd i f f i c u l tt od e t e r m i n et h eu p p e rb o u n d so ff ( k 1f o r 七 i nt h i st h e s i s ，w eh a v ef o l l o w i n gc o n t r i b u t i o n s ： ( 1 ) at r e er u l ei si n t r o d u c e dt or e d u c et h es t e p so fc a l c u l a t i n gs t a i r w a y s ，a n d ad e t e r m i n i s t i cc a l c u l a t i o nf o rs t a i r w a y si sp r e s e n t e dt og e tt h eu p p e rb o u n d sf o r ，( ) ( 3 ) t h ed e t e r m i n i s t i ca l g o r i t h mi sp r a c t i c a l ，a n dt h eu p p e rb o u n d sa r e n e a rt h eb o u n d ss h o o r ya n ds s e z i d e rg o t ( 2 ) ar a n d o m i z ea l g o r i t h mf o ro u t p u t t i n gat r u ea s s i g n m e n tf o rag i v e nf o r m u l a i sp r e s e n t e d b a s e do ni ta n db yp r o b a b i l i s t i cm e t h o d ，w ep r o v et h a t ，f o re v e r y i n t e g e r 2 ，e a c hf o r m u l afi n ( k ， ) 一c n fw i t hl e s st h a n0 5 8 v m k - - l 2 2 i ss a r i s f i a b l e i na d d i t i o n ，b yt h el o v 宣s zl o c a ll e m m a ，w eg e tan e wl o w e rb o u n do ff ( k ) ， q ( 、志2 k ) ，w h i c hi m p r o v e st h er e s u l tn ( 2 。i k ) 一 k e yw o r d s ：s a t ，( 尼，s ) 一e f ，m i n i m a lu n s a t i s f i a b l e 如r m u l a ，t h ep r o b a b i l i s t i cm e t h o d , r a n d o m i z ea l g o r i t h m l l c h a p t e r1 i n t r o d u c t i o n 1 1 b a c k g r o u n d i n1 9 7 1 ，c o o kf o u n dt h ef i r s tn p c o m p l e t ep r o b l e m ，ad e c i s i o np r o b l e mf r o mb o o l e a n l o g i c 【c 0 0 7 1 i ti su s u a l l yr e f e r r e dt ot h es a t i s f i a b i l i t yp r o b l e m ( a b b r e v i a t ef o r s a t ) b e i n go n eo ft h es i m p l e s tn p - c o m p l e t ep r o b l e m s ，s a tp l a y sa ni m p o r t a n t r o l ei nt h es t u d yo fc o m p u t a t i o n a lc o m p l e x i t y m a n yn p c o m p l e t ep r o b l e m se i t h e r c a nb et r a n s f o r m e dt os a to rc o n t a i nc o m p o n e n tp r o b l e m st h a tc a nb et r a n s f o r m e d t o 翻t t h u s ，ag o o ds a ta l g o r i t h mw i l lh a v ew i d eu s a g ep o t e n t i a l l y ( k ，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 l ep r o b l e mr e s t r i c t e dt oi n s t a n c e sw h e r e e a c hc l a u s eh a se x a c t l ykd i s t i n c tl i t e r a l 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 i tw a so b s e r v e db yt o v e y c a 】t h a ta l lf o r m u l a si n ( 3 ，3 ) 一c n fa r es a t i s f i a b l e ，a n d t h es 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 ( 3 ，4 ) 一c n fi sa l r e a d yn p - c o m p l e t e t h i s w a sg e n e r a l i z e di nk r a t o c h v f l sw o r k j p z ，w h e r ei ti ss h o w nt h a tf o re v e r yk 3 ， t h e r ei ss o m ei n t e g e rs = ，( 七) ，s u c ht h a t a l lf o r m u l a si n ( 后，s ) 一c n fa r es a t i s f i a b l e ，a n d ( k ，s + 1 ) 一s a t ，t h es 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 ( 尼，s + 1 ) 一c n f ，i sa l r e a d y n p - c o m p l e t e t h e r e f o r ew et e r mfc r i t i c a lf u n c t i o n i tc a nb ed e f i n e df o r m a l l yb yt h ee q u a t i o n f ( k ) = m a x s ：( 七，s ) 一c n fn u n s a t = d ) f r o m 【c a ，i tf o l l o w st h a tf ( 3 ) = 3a n df ( k ) kf o rk 3 h o w e v e ri ti so p e n w h e t h e rfi sc o m p u t a b l e i t i sk n o w nt h a ta nu n s a t i s f i a b l ef o r m u l ac o n t a i n sam i n i m a lu n s a t i s f i a b l es u b f o r m u l a t h e r e f o r e ， 1 2c h a p t e r1 i n t r o d u c t i o n f ( k ) = m a x $ ：( ，s ) 一6 7 v fn m u = 0 ) t h ef o r m u l a si nm u ( 1 ) h a v eas i m p l es t r u c t u r ea n dc a nb ec o n s t r u c t e di na r e c u r s i v ew a y d d k b 9 8 ，i ti se a s e rt os e a r c hf o rau n s a t i s f i a b l ef o r m u l ai n ( 七，s ) 一 c n fnm u ( 1 ) t h a ni n ( k ，s ) 一c l tnm u i ti st h ei d e ao fs z e i d e r sa p p r o a c h i n s s ，s h o o r ya n ds s z e i d e rd e f i n e dan e wf u n c t i o n ： f l ( k ) = m a x s ：( k ，s ) 一c n fn m u ( 1 ) = 0 e v i d e n t l y , f l ( k ) ，( 七) t oc o n s t r u c t i o nr e q u i r e dm c r ( 1 ) 一f o r m u l a ，t h e yi n t r o - d u c e dac o n c e p to fs t a i r w a y , t ow h i c haf o r m u l ac o r r e s p o n d s ，n a m e l y , af i n i t ei n t e g e r s e q u e n c e 矿= ( a l ，a 2 ，a n ) w i t h0 1 a 22 2a n 1 f o re a c hf ( 七，s ) 一 c n fnm u ( 1 ) ，t h e r ei sac a l c u l a t i o nf o rs t a i r w a y su n d e rs o m er u l e s h o w e v e r ，t h e c a l c u l a t i o ns t a i r w a y sg e n e r a t i n gr e q u i r e dm u ( 1 ) 一f o r m u l ai sn o n d e t e r m i n i s t i c t h e p r o b a b i l i s t i cm e t h o di sn o ta b o u tp r o b a b i l i s t i ca l g o r i t h m s n j ，j h s ，w h i c h g i v et h er i g h ta n s w e rw i t hh i g hp r o b a b i l i t yb u tn o tw i t hc e r t a i n t y , n o ra b o u tm o n t e c a r l om e t h o d s ，w h i c ha x es i m u l a t i o n sr e l y i n go np s e u d o r a n d o m n e s s t h ep r o b a b i l i s t i cm e t h o di san o n c o n s t r u c t i v em e t h o dp r i m a r i l yu s e di nc o m - b i n a t o r i c sa n dp i o n e e r e db yp a u le r d s s ，f o rp r o v i n gt h ee x i s t e n c eo fap r e s c r i b e d k i n do fm a t h e m a t i c a lo b j e c t t h i sm e t h o dh a sn o wb e e na p p l i e dt oo t h e ra r e a so f m a t h e m a t i c ss u c ha sc o m p u t e rs c i e n c e ，n u m b e rt h e o r y , l i n e a ra l g e b r a ，a n dr e a la n a l y s i s c o m m o nt o o l su s e di nt h ep r o b a b i l i s t i cm e t h o di n c l u d em a r k o v si n e q u a l i t y ， t h ec h e r n o f fb o u n d a n dt h el o v d a s zl o c a ll e m m a 1 2m a i nw o r ka n df u t u r ew o r k i nt h et h e s i s ，o u rm a i nw o r k sa r ec o m p o s e do ft w o a s p e c t s ：p r e s e n t i n gad e t e r m i n i s t i c a l g o r i t h mt oc o m p u t i n gt h eu p p e rb o u n d so fc r i t i c a lf u n c t i o n ，( 七) ，a n dg e t t i n ga n e wl o w e rb o u n do f ，( ) f o l l o w i n g ，w ew i l lg i v et h ed e t a i l so ft h e m i nc o m p u t i n gt h eu p p e rb o u n d s a s p e c t ，i n s s ，s h o o r ya n ds s e z i d e ro b t a i n ac o m p u t a b l eu p p e rb o u n df u n c t i o nf o r ，( 自) 三3 ) t h ea p p r o a c hi st oc r e a t e s o m ei n s t a n c ei n ( 七，s ) 一s a tb yc a l c u l a t i n gs t a i r w a y s ，w h i c ha x ec o r r e s p o n dt oc o n s t r u c t l n gs o m 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 sw i t hd e f i c i e n c yo n e h o w e v e r jt h e c a l c u l a t i o nf o rs t a i r w a y si sn o n d e t e r m i n i s t i c i ti sd i 盘c u l tt od e t e r m i n et h eu p p e r b o u n d so ff ( k ) f o rl a r g e rk w ei n t r o d u c eat r e er u l ei nt h ec a l c u l a t i n gs t a i r w a y s ， a n dp r e s e n tad e t e r m i n i s t i cc a l c u l a t i o nf o rs t a i r w a y st og e tt h eu p p e rb o u n d sf o r 厂( ) ( 3 ) t h ed e t e r m i n i s t i ca l g o r i t h mi sp r a c t i c a l ，a n dt h eu p p e rb o u n d sa r e n e a rt h eb o u n d ss h o o r ya n ds s e z i d e rg o t ( s e et a b l e1 ) 1 3 o r g a n i z a t i o no ft h et h e s i s f ( k )s z e s s 】 t h i sp a p e r 3 f ( 3 ) 33 4 f ( 4 ) 44 5 f ( 5 ) 77 7 f ( 6 ) 1 11 l 1 3 f ( 7 ) 1 71 9 2 4 f ( 8 ) 2 93 3 4 1 f ( 9 ) 5 15 8 f ( 1 0 ) n 01 0 1 f ( 1 1 ) n 01 8 9 t h b l e1 3 i nt h eo t h e ra s p e c t ，a n a l o g o u st ot h er a n d o m i z e da l g o r i t h mf o rf i n d i n gt w o c o l o r i n go fk - u n i f o r mh y p e r g r a p h p m a ，c m a ，c m h ，j b o ，j a s ，w ep r e s e n to n e f o ro u t p u t t i n gat r u ea s s i g n m e n tf o rf o r m u l a si n ( 后， ) 一c n f a n dt h e n ，f o re a c h f o r m u l a ，w ec a l lc r e a t eap r o b a b i f i t ys p a c e ，t h es a m p l e so fw h i c ha r et h ea s s i g n m e n t s d e r i v e dr a n d o m l yf r o mt h er a n d o m i z e da l g o r i t h m w es h o w ，i nt h i sk i n do fp r o b - a b i l i t ys p a c e ，f o re a c hf o r m u l a ，t h ep r o b a b i l i t yo ff o r m u l aw i t hat r u ea s s i g n m e n t i sp o s i t i v e ，t h e r e f o r e ，b yt h ep r o b a b i l i s t i cm e t h o d ，t h ef o r m u l ai ss a t i s f i a b l e i n a d d i t i o n ，b a s e d0 nt h er a n d o m i z e da l g o r i t h m ，w ea t t a i n ，b ya p p l y i n gt h el o v 五s z l o c a ll e m m a ，an e wl o w e rb o u n do f ，( ) ，q ( 志2 k ) ，w h i c hi m p r o v e st h er e s u l t a ( 2 2 k ) h o w e v e r ，t h e r ea r es t i l ll o t so fp r o b l e m sr e m a i n i n gu n s o l v e d f o re x a m p l e ，h o w t oi m p r o v ee f f i c i e n t l yt h ee x i t e dd e t e r m i n i s t i ca l g o r i t h mf o rc o m p u t i n gt h eu p p e r b o u n do fc r i t i c a lf u n c t i o n ? h o wt og e tam o r et i g h tl o w e rb o u n db ym o r ec l a s s i c a l m a t h e m a t i c a lm e t h o d s ? m o r ed i f f i c u l t ，h o wt od e t e r m i n et h eq u e s t i o no fw h e t h e r t h ec r i t i c a lf u n c t i o ni sc o m p u t a b l e ? e t c t h e s eq u e s t i o n sa r es t i l lt h en e x tg o m so f o u rr e s e a r c h 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 da sf o l l o w s ：c h a p t e r2g i v e ss o m en o t a t i o n st h a tr e l a t e d t o ( k ，s ) _ s a tp r o b l e m ，i m p o r t a n tc o n c e p t sa n dl e m m a sa b o u tm u ( 1 ) c h a p t e r3 i n t r o d u c e sc a l c u l a t i o nr u l e sa n dp r e s e n t sad e t e r m i n i s t i ca l g o r i t h mc o m p u t i n g ，( ) c h a p t e r4p r e s e n t sar a n d o m i z ea l g o r i t h m ，a n dt h e n ，b a s e d0 i 3i ta n dp r o b a b i l i s t i c m e t h o d ，g i v e ss o m er e s u l t sa b o u ts a tp r o b l e ma n dt h en e wl o w e rb o u n d c h a p t e r 2 p r e l i m i n a r i e s s i n c et h es c o p eo fr e s e a r c hw ef o c u s i n go ni sr e s t r i c t e di np r o p o s i t i o n a ll o g i c ，i nt h i s c h a p t e r ，w ew i l lg i v es o m eb a s i cn o t a t i o n si np r o p o s i t i o n a ll o g i ca n d s o m ei m p o r t a n t s t a t e m e n t so nm u ，e s p e c i a l l ym u ( 1 ) 2 1 p r o p o s i t i o n a ll o g i c p r o p o s i t i o n sa r ej u s ts t a t e m e n t sw i t h o u tv a r i a b l e s p r o p o s i t i o n a ll o g i cd e a l sw i t h t r u t hv a l u e sa n dl o g i c a lc o n n e c t i v e s a n d ，o r ，n o t ，i m p l i e s a n d i fa n do n l yi f a n yl o g i cc o m p r i s e ss y n t a xp a r t ，w h i c hi saf o r m a ln o t a t i o nf o rw r i t i n ga s s e r t i o n s a n ds e m a n t i c sp a r t ，w h i c hg i v e sam e a n i n gt oa s s e r t i o n s t h es y n t a c t i cp a r to f p r o p o s i t i o n a ll o g i cc a nb er e g a r d e da st h ew a yi nw h i c hs t a t e m e n t sa r ec o m b i n e dt o f o r mo t h e rs t a t e m e n t s t h es e m a n t i c sp a r to fi ti sc o n c e r n e dw i t ha s c r i b i n gm e a n i n g t ot h es y m b o l si nv a r i o u sw a y s am a j o rt h e m eo nt h ed e v e l o p m e n to fl o g i ci st h e r e l a t i o n s h i pb e t w e e nt h e s et w oa s p e c t so fl a n g u a g e w et a k ef o rg r a n t e das e to fp r o p o s i t i o n a ls y m b o l sp 1q ，r ，一，i n c l u d i n gt r u t h v a l u e sta n df ( s o m e t i m e sw ed e n o t ea s1a n d0 ，r e s p e c t i v e l y ) af o r m u l ac o n s i s t i n go f o n l yo n ep r o p o s i t r ) n a ls y m b o li sc a l l e da t o m i c w ec a l lt h eo p e r a t o r st h a tc o m b i n e p r o p o s i t i o n a lf o r m u l a st of o r mn e wo n e sc o n n e c t i v e s t h ef o r m a ls y m b o l sf o rt h e s ec o n n e c t i v e sa r ea sf o l l o w s ： vf o r “o r ” ( d i s j u n c t i o 几) af o r“a n d ” ( c o n j u n c t i o n ) 、 f o r“n o t ” ( n e g a t i o n ) df o r “i m p l i e s ” fc o n d i t i o n a l ) hf o r “i fa n do n l yi f ” f b i c o n d i t i o n a l ) 4 2 1 p r o p o s i t i o n a ll o g i c 5 af o r m u l ai sc o n s t r u c t e df r o ma t o m i cf o r m u l a su s i n gl o g i c a lc o n n e c t i v e s1 ，v a da n d h t h ef o r m a ld e f i n i t i o ni sa sf o l l o w s ： d e f i n i t i o n1 ( p r o p o s i t i o n a ly o m 让l a ) n s g s ( i ) p r o p o s i t i o n a ls y m b o l sa r ep r o p o s i t i o n a lf o r m u l a s f 剀可口a n d a r ep r o p o s i t i o n a lf o r m u l a s ，t h e n ( o lap ) ，( av 卢) ，( 、a ) ，( o t 卢) a n d ( o lh 卢) a r ep r o p o s i t i o n a lf o r m u l a s ( 3 1as t r i n go f s y m b o l si s8 p r o p o s i t i o n a lf o r m u l ai f a n do n l yi f i tc a n b eo b t a i n e d b ys t a t i n gw i t hp r o p o s i t i o n a ls y m b o l s ( s ja n dr e p e a t e d l ya p p l y i n g 2 ) f o re x a m p l e ，( a v b ) ，c ，( ( a a b ) _ g ) ，( - 、( a a b ) _ c ) a r ea l lf o r m u l a sw h i l e aa 、，( avb ，( a _ a ) 8 , r en o t t h ei m p o r t a n c eo fc l a u s e ( 3 ) i nt h ea b o v ed e f i n i t i o n i st h a ti tg i v e st h eb a s i sf o ra p p l y i n gi n d u c t i o nd i r e c t l yt of o r m u l a s i nt h ef o l l o w i n g ，f o rs i m p l e n e s s ，w eu s ef o r m u l at od e n o t ep r o p o s i t i o n a lf o r m u l a ， a n dl e t t e rt om e a np r o p o s i t i o n a ll e t t e r ，i fw i t h o u ta b s u r d n e s s d e f i n i t i o n2 ( t 他t ha s s i g n m e n t ) i n s 9 3 aa s s i g n m e n t7 - i sof u n c t i o nw h i c ha s s i g n st oe a c hl e t t e rp 。u n i q u ev a l u e 7 _ ( p ) o ，1 ) d e f i n i t i o n3 n s 9 3 av a l u a t i o n7 - i saf u n c t i o nw h i c ha s s i g n st oe a c hf o r m u l af au n i q u ev a l u e 7 - ( f ) o ，1 s ot h a ti t sv a l u eo nnc o m p o u n df o r m u l a i sd e t e r m i n e di na c c o r d a n c e w i t ht h ea p p r o p r i a t et r u t ht a b l e s t h u s ，f o re x a m p l e ，r ( - 1 f ) = 0i f a n do n l yi f 7 _ ( f ) = 1a n d7 _ ( f vg ) = 1 矿a n do n l yi ft ( f ) = 1o r 下( g ) = 1 a na s s i g n m e n t 丁s a t i s f i e saf o r m u l afi f7 - ( f ) = l ；o t h e r w i s e ，t h ea s s i g n m e n t f a l s a t i s f i e st h ef o r m u l a d e f i n i t i o n4 n s 9 3 a f o r m u l af i ss a i dt ob ev a l i di f f o ra n ya s s i g n m e n t7 - ，7 _ ( f ) = 1 s u c hf o r m u l a i sa l s oc a l l e dat a u t o l o g y d e f i n i t i o n5 ( u n s a t i s f i a b l ef o r m u l a ) n s 9 3 a f o r m u l af i ss a i dt ob eu n s a t i s f i a b l ei fo n l yi f f o ra n ya s s i g n m e n t7 _ ，7 _ ( f ) = 0 6c h a p t e r2 p r e l i m i n a r i e s 2 2b a s i cd e f i n i t i o n sa n dn o t a t i o n s al i t e r a li 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 ec i sad i s j u n c t i o no fl i t e r a l s ，c = ( l 1v 一vl m ) ，a n ds o m e t i m e sw ew r i t ec a sas e t o fl i t e r a l s ，c = l 1 ，l m ) t h ei n t e g e rm ，t h en u m b e ro fl i t e r a l so c c u r r i n gi n t h ec l a u s ec ，i sc a l l e dt h el e n g t ho ft h ec l a u s ec ，d e n o t e db y # 1 i t ( c ) o r1 c i au n i t c l a u s ei sac l a u s ec o n t a i n i n go n l yo n el i t e r a l ac o n j u n c t i o nn o r m a lf o r m ( c n f ) f o r m u l afi sac o n j u n c t i o no fc l a u s e s ，f = ( c 1a ag ) ，a