（计算机应用技术专业论文）基于st方法的命题公式不可满足性的判定系统.pdf

基于s t 方法的命题公式不可满足性的判定系统 摘要逻辑公式的满足性问题是理论计算机科学和人工智能中的著名问题命题逻辑公 式的满足| 瞄朔定方法和一阶逻辑公式有限模型构造技术在离散数学研究、电路辅助设计、软 件工程和人工智能领域都有一些应用 很多算法可以用来进行重言式验证，比如表算法、王浩算法以及二叉判定图b d d 二又 判定图b d d 和它们的变体在其它应用方面做得也比较好，比如说模型检测等 s t h m r e k 的重言式验证方法在一些应用上可以与二又判定图b d i ) 媲美，但是这个方法 相对来诫在硬件检测方面并不为人所知g r o o t e 发现s t a i m r c k 方法与基于b d d 的方法和 o t t e r 证明器比较而畜，在一个特定的荷兰火车站的安全保证系统验证中是非常高效的 然而，我们说s t i m r c k 方法是不完善的虽然许多工业检测问题的难度是o 或者1 ， 对于难度为o 的问题不需要使用二难规则就可以解决，但对于难度为i 的问题就需要使用一 级二难规刖而在此前的任何资料中都未曾提到关于s t i m r c k 方法中，二难规则中集合 r 1 和r 2 的交集为空集的情况然而这种情况是j 晡可能存在的本文利用三元组形式给出 了s t i m a r c k 算法的一套推理规剧及相应的s t a i m a r c k 算法，井就r 1 和r 2 的交桌为空集的 情况给出实例以及处理这种情况的办法并用程序( 即不可满足公式的反驳证明系统) 实现了 这种方法使得s t i m a r c k 方法更加完善 进一步，我们用四元组形式给出了一套适用于不同联结词的推理规则，用四元组粜合表 示公式，并对三元组形式表示规则的程序张加修改，从而可以形成s t i m a r c k 算法的一般规 则判定系统 下一步，我们将实现基于文本的推理规则的s t a i m r c k 证明器，以及探索更好的解决二 难规刖中的漏洞的方法 关键词不可满足公式：s t l l m a r c k 方法；二难规刷 中图分类号0 1 4 1 1 a c h e c k i n gs y s t e mo fu n s a t i s f i a b i l i t yb a s e d o ns t a l g o r i t h mf o rp r o p o s i t i o n a lf o r m u l a s a b s t r a c t s a to f1 0 s i cf o r m u l a si saf a m o u sp r o b l e mo ft h e o r e t i cc o m p u t e rs c i e n c ea n d a r t i f i c i a li n t e l l i g e n c e c h e c k i n gm e t h o do fs a t i s f i a b l l i t yf o rp r o p o s i t i o n a ll o g i cf o r m u l a sa n df i n i t e m o d e lc o n s t r u c t e dt e c h n o l o g yf o rf i r s t - o r d e rl o g i cc a nb es p p u e di ns o m ef i e l d s ，s u c ha sd i s c r e t e m a t h e m a f i r e s e a r c h ，t h ec o m p u t e ra i d e dd e s i g no fe l e c t r o n i cc i r c u i t s ，s o f t w a r ee n g i n e e r i n ga n d a r t i f i c i a li n t e l l i g e n c e m a n ya l g o r i t h m sa r ea p p l i c a b l ef o rt a u t o l o g yc h e c k i n g , s u c ha st a b l e a up r o o fs y s t e m 、 w a n g h a oa l g o r i t h ma n db i n a r yd e c i s i o nd l a g r a m ( b v d s ) b d da n dt h e i rv a r i a t i o n sw o r kw e l l f o ro t h e ra p p l i c a t i o n s ，s u c ha sm o d e lc h o k i n g s t a i m a r e k sm e t h o do ft a u t o l o g yc h e c k i n gm a yw e l lr i v a lb d d s 1 8 】i ns o m ea p p l i c a t i o n s ， b u tt h a ti sr e l a t i v e l yu n l m d w ni nt h eh a r d w a r ev e r i f i c a t i o nc o m m u n i t y 1 0 1 n d sp a t e n t e dm e t h o d i si m p l e m e n t e di nac o l l n l e r c i a it o o l t h a th a sb e e nu s e di nm a n yi n d m 仃i a ls v s t e mv e r i f i c a t i o n p r o j e c t s 1 o f t e n t h ev e r i f i c a t i o np r o b l e mc a nb ee x p r e s s e d a ni n d u c t i v ep r o o f , a n dt h eb a s e c a s ea n dt h es t e pc h e c k e du s i n gs t a i m a r c k sm e t h o d m a n yo ft h e s er e a l - w o r l dv e r i f i c a t i o n sg i v e r i s et o 印o r m o u sf o r m u l a st h a tc o u l dn o tb eh a n d l e db ya 肛r 锄tb d dp a c k a g e s c r r e o t eh a sf o u n d s t a l m a r c k sm e t h o dt ob ev e r ye f f i c i e n tc o m p a 托dt ob d d - b a s e dm e t h o d sa n dt h eo t t e rd o ，e li n t h ev e r i f i c a t i o no f t h es a f e t yg u a r a n t e e i n gs y s t e ma tap a r t i c u l a rd u t c hm f l w a ys t a t i o n 1 2 h o w e v e r , s t 墨i m a r c k sm e t h o di sn o tp e r f e c t m a n yi n d u s t r i a lv e r i f i c a t i o np r o b l e m sg i v er i s e t of o n n u l a sw h o s eh a i d n e s si s0w 1 ，f o rt h ef o r m u l a sw h o s eh a r d n e s si s0 ，o d ec a nf i n dap r o o fi n l i n e a rt i m ew i t h o u tt h ed i l e m m ar o l e ，b u tf o rt h ef o r m u l a sw h o s eh a r d n e s si s1 。o n em u s tmt h e d i l e m m ar u l e i ti sn o tc o n s i d e r i n gt h ec a s et h a tt h ei n t e r s e c t i o no fr 1a n dr 2i se m p t yi nt h e 、b r a n c ha n dm e r g er u l e ”，b u ti ti sp o s s i b l et h a tt h ec a s ee x i s t s i no u ra r t i c l e ，w eg a v ea ne x a m p l e w i t ht h a tc a s ea n dm a d eas y s t e mc o n t a i n i n gt h ec a s e o u rm e t h o dh a v ei m p r o v e dt h e 、d i l e m m a r u l e “，a n dg a v eap e r f e c tp r o v e r k e yw o r d s ：u n s a f i s 矗a b l ef o r m u l a , s t a l m a r c km e t h o d ，d i l e m m ar u l e c h a p t e r1 i n t r o d u c t i o n s a t o f l o g i cf o r m u l a si saf a m o u sp r o b l e mo f t h e o r e t i cc o m p u t e rs c i e n c ea n da r t 进c i a l i n t e l l i g e n c e c h e c k i n gm e t h o do fs a t i s f i a b i l i t yf o rp r o p o s i t i o n a ll o g i cf o r m u l a sa n d f i n i t em o d e lc o n s t r u c t e dt e c h n o l o g yf o rf i r s t o r d e rl o g i cc a nb ea p p l i e di ns o m e f i e l d s ，s u c ha sd i s c r e t em a t h e m a t i c sr e s e a r c h ，t h ec o m p u t e ra i d e dd e s i g no fe l e c t r o n i c c k c u r s ，s o f t w a r ee n g i n e e r i n ga n da r t i f i c i a li n t e l l i g e n c e t h e r ea r et w om a i nt y p eo f a l g o r i t h m sf o rs o l v i n gs a t 【d h r v 0 1 ，n a m e l ys p l i t t i n ga l g o r i t h m s ( s e e d p 6 0 ，d l l 6 2 ， k u l 9 9 ，k l 9 7 ，k u l 9 8 ，k u l 0 0 ，p p s z 9 8 ，p p z 9 7 ) a n dl o c a ls e e r c h ( f o rr e f e r e n c e ss e e ， f o re x a m p l e ，【g p f w 0 0 ，k p 9 2 ，s l m 9 2 ，p a p 9 1 ，s c h 9 9 ，h 0 0 ) a l g o r i t h m s t h e s e m e t h o d sa l ed e s i g n e df o rb e t t e rw o r s t - c a s eu p p e rb o u n d s m a n yo t h e ra l g o r i t h m s a r ea p p l i c a b l ef o rt a u t o l o g yc h e c k i n g ，s u c ha st a b l e a up r o o fs y s t e m ，w a n g h a o a l g o r i t h ma n db i n a r yd e c i s i o nd i a g r a m ( b d d s ) s t t d m a r c k sm e t h o do ft a u t o l o g y c h e c k i n gm a yw e l lr i v a lb d d s 【b 8 6 】i ns o m e8 p p l i e a t i o u s ，b u ti ti sn o tp e r f e c t b y i m p r o v i n gi t s d i l e m m ar u l e ，w eg e tam o r ep e r f e c tp r o v e r 1 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 a ll o g i cd e a l sw i t ht 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 ， e t c i th a sn ov a r i a b l e sa n dc a l lo n l ye x p r e s ss i m p l e s tm a t h e m a t i c a ls t a t e m e n t s p r o p o s i t i o n a ll o g i cc o m p r i s e sas y n t a x ，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 e r - t i o u sa n das e m a n t i c s ，w h i c hg i v 髑am 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 l 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 of o r mo t h e r s t a t e m e n t s t h es e m a n t i c sp a r ti sa s c r i b i n gm e a n m gt ot h es y m b o l si nv a r i o u sw a y s t h ef o r m 8 1n o t a t i o no faf o r m u l ai 8a 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 l o n u t a ) ( 1 ) p r o p o s i t i o n a ls y m b o l s 眦p r o p o s i t i o n a lf o r m u l a s l 2 封i f 2a n dpa 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 tap ) ，( ov 口) ，( 、口) ，( d p ) a n d 陋hp ) a r ep r o p o s i t i o n a lf o r m u l a s 俐as 加i n go y s y m b o l s i sap r o p o s i t i o n a lf o r m u l ai f a n do n l ui y i t nb 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 l3 舯6 0 b 以，a n dr e r a t e d l ya p p l y i n y ( $ ) p r o p o s i t i o n a ll o g i ci saf o r m a ll a n g u a g e e a c hf o r m u l ah a sam e a n i n g ( o rt r u t h v a l u e ) - - e i t h e rto rf - r e l a t i v et ot h em e a n i n go fp r o p o s i t i o n a ls y m b o l si t c o n t a i n s - t h em e a n i n gc a l lb ec a l c u l a t e du s i n gt h es t a n d a r dt r u t ht a b l e s d e f i n i t i o n2 ，m i t a s s i g n m e n t ) at r u t ha s s i g n m e n t 诂af u n c t i o nw h i c ha s s i g n st oe a c hp r o p o s i t i o n a ll e t t e r aau n i q u et r u t hv a l u e - 4 ( a ) t ，f ) d e f i n i t i o n3 ( r 他t hv a l u a t i o n ) at r u t hv a l u a t i o nv saf u n c t i o nw h i c ha s s i g n st oe a c hp r o p o s i t i o n a lf o r m u l a qau n i q u et r u t hv a l u ev ( a ) s ot h a ti t sv a l u eo nac o m p o u n d ，0 r m u l ai sd e t e r m i n e d 讥a c c o r d a n c ew 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 ，i o re x a m p l e ，y ( 一0 。= f 够 y ( 口) = ta n d y 幢v 国= t 谚v ( n ) = to rv ( 所= t t h e o r e m1g i v e nat r u t ha s s i g n m e n tat h e r e 妇au n i q u et r u t hv a l u a t i o nvs u c h t h a tv ( a ) = a ( a ) f o re v e r yp r o p o s i t i o n a ll e t t e ra av a l u a t i o ns a t i s f i e saf o r m u l ai ft h ef o r m u l ae v a l u a t e st otu n d e rt h ev a l u a t i o n d e f i n i t i o n4ap r o p o s i t i o n 口o fp r o p o s i t i o n a l 蛔i ci ss a i dt ob ev a l i d 铲i o ra n y v a c a t i o ny ，v ( 口) = t s u c hap r o p o s i t i o ni 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 ) a p r o p o s i t i o n 盯o fp r o p o s i t i o n a lt o a i ci ss a i dt ob eu n s a t i s f i a h l e 玎f o ra n yv a l u - o 缸d n v ，y ( 盯) = f s o u n d n e s sa n dc o m p l e t e n e s sa r er e l a t i v et op r o o fs y s t e m s f o rs o m ep r o o f s y s t e m ，t h ep r o o fo fi t ss o u n d n e s sa n dc o m p l e t e n e s si st op r o v et h ee q u i v a l e n c e o ft h es e m a n t i cn o t i o no fv a l i d i t ya n dt h e s y n t a c t i cn o t i o no fp r o v a b i l i t y f o re x - a m p l e ，w h e t h e ra l lt a b l e a up r o v a b l ep r o p o s i t i o n a lf o r m u l a sa r ev a l i d ( s o a n d n e s so f t h ep r o o fm e t h o d ) a n dw h e t h e ra l lv a l i dp r o p o s i t i o n a lf o r m u l a sa r et a b l e a up r o v - a b l e ( c o m p l e t e n e s so ft h em e t h o d ) 1 2 p r o o fs y s t e m so fs a t i s f i a b l l r r y 1 2p r o o fs y s t e m so fs a t i s f i a b i l i t y 3 t h e r ea r em a n yp r o o fs y s t e m so fs a t i 正a b i l i t yf o rp r o p o s i t i o n a lf o r m u l a s s u c h8 8 t a b l e a up r o o fs y s t e m w a n g h a oa l g o r i t h m b i n a r yd e c i s i o nd i a g r a m ( b d d s ) a n d d p l la l g o r i t h m al o to fe f f o r th a sb e e ni n v e s t e di np r o v i n g l e s s - t h a n - 2 一u p p e r b o u n d sf o rm u c ho fs u c ha l g o r i t h m s c t l t a b l e a u p r o o f s y s t e m i s t o s t a r t w i t hs o m e e n t r y , i e ，s o m e s i g n e d p r o p o s k i o n a l f o r m u l a ，s u c ha sf a ( f 1 a ) ，a n da n a l y z ei ti n t oi t sc o m p o n e n t si ns u c haw a y 鹪t o s e et h a ta n ya n a l y s i sl e a d st oac o n t r a d i c t i o n w j 耐i it h e nc o n e h i d et h a tw eh a v e r e f u t e dt h eo r i c i n a la s s u m p t i o nt h a ta ( - 1 a ) i sf a l s ea n ds oh a v eap r o o fo fa ( 1 口) t h ed a v i s - p u t n a mm e t h o di sav e r ye f f e c t i v em e t h o df o rt e s t i n ge a t i 曲a b i l i t y o faf i n i t es e to fp r o p o s i t i o n a ls t a n d a r dc l a u s e s t h em e t h o dc o n s i s t si nac o m b i n a - t i o no fe a g e r l yp e r f o r m e ds i m p l i f i c a t i o ns t e l m ( u n i tr e d u c t i o n ，p u r el i t e r a ld e t e c t i o n ) t o g e t h e rw i t hc a 的s p l i t so i lp r o p o s i t i o n a lv a r i a b l e s 1 3s t a l m a r c k sm e t h o d s t a i m a r c k sm e t h o dd a t e di n1 9 8 0 sa n di tm a yw e l lr i v a lb d d s b 8 6 i ns o m ea p p l i c a - t i o n s ，b u tt h a ti sr e l a t i v e l yu n k n o w ni nt h eh a r d w a r ev e r i f c a t i o nc o m m u n i t y 【h 9 6 】 t h i sp a t e n t e dm e t h o di si m p l e m e n t e di nac o m m e r c i a lt o o lt h a th a sb e e nu s e di n m a n yi n d u s t r i a ls y s t e mv e r i f i c a t i o np r o j e c t s 【b 9 7 t h em a i ni d e ao fs t a i m a r c ka l g o r i t h mi s f o l l o w s ： ( 1 ) i n t r o d u c eas e r i e so fs i m p l ei n f e r r i n gm i c ea n dab r a n c ha n dm e r g er u l e ( 2 ) f o rt h eg i v e nu n s a t i s f i a b l ef o r m u l af ，s u b s t i t u t ee a c hs u b f o r m u l af o ra d e wv a r i a b l e t h u s t h eo r i g i n a lf o r m u l ac a nb er e p r e s e n t e da 8as e to ff o r m u l a s i nt h ef o r mo fe 三。奉掣0 ，v ，呻，+ 呻) ) o re 三1 z an e wv a r i a b l ee oc a n r e p r e s e n tf f o re x a i n p l e ：f o r m u l af = ( oa1 b ) _ cc a nb er e p r e s e n t e d 蝇 e o i ( e l c ) ，e l 三( a ae 2 ) ，e 2 e ，6 ) ( 3 ) l e te 0i1 ，w ea c h i e v ea no r i g i n a le q u i v a l e n c ec l a s sr ( 4 ) 0 - s a t u r a t i o n 岛i sd o n eb ya p p l y i n gs i m p l er u l e st of o r m u l a sw h i c ha r ei nr t od e d u c en e we q u i v a l e n c e s ac o n t r a d i c t i o ni so b t a i n e d w ea r ed d n e ( 5 ) o t h e r w i s e ，1 - s a t u r a t i o ni sp e r f o r m e d ：f o re a c hv a r i a b l e ，t h ei m p r o v e dd i l e m m a r u l ei su s e dt od e d u c en e w e q u i v a l e n c e s i fac o n t r a d i c t i o ni so b t a i n e di nc u r r e n t b r a n c h ，w ea r ed o n e ( 6 ) e l s e ，c o n t i n u ep e r f o r r a i n ga d d i t i o n a ll e v e l so fs a t u r a t i o nu n t i lac o n t r a d i c t i o n i so b t a i n e d ( 7 ) t h ea b o v ep r o c e s sh a sf o r m e dat r e es t r u c t u r e i fe a c hl e a fn o d ei nt h e 4 c h a p t e r1 i n t r o d u c t l o n i n f e r r i n gt r e ec o r r e s p o n d st oac o n t r a d i c t i o nc l a s s t h a tm e a n sw eh a v eo b t a i n e da r e f u t a t i o np r o o f t h ea l g o r i t h mp r o v i d e sa ne f f i c i e n tw a yt od ot a u t o l o g y ( u n s a t i s f i a b i l i t y ) c h e c k - i n go nl a r g ef o r m u l a s i ti sab r e a d t h - f i r s ta p p r o a c ha n dh a sb e e nu s e dt op e r f o r m i n d u s t r i a l - s t r e n g t hf o r m a lv e r i f i c a t i o no f m a n yh a r d w a r e - l i k es y s t e m s g k v 9 4 b u t i ti sn o tp e r f e c t ，b yi m p r o v i n gi t s “d i l e m m am l e ”，w eg e tam o r e p e r f e c tp r o v e r 1 4f u r t h e rw o r k a tp r e s e n t ，o u rw o r kh a si m p r o v e ds t a i m a r c ka l g o r i t h ma n di tb e c o m e s m o r ep e r - f e c t t h eq u e s t i o no fw h e t h e ro rn o tt h es t a i m a r c ka l g o r i t h mc a nb ea p p l i e di n p r a c t i c ei nc a dr e m a i n st ob ea n s w e r e d t h ef u r t h e rw o r ki st h a tw ew i l lc o m p l e t et h es t a l m a r c kp r o v e rw h i c hi sb a s e d o nt h er u l e st h a td e p e n do nt e x t it h i n kt h a ti st h ec o m b i n a t i o no f t h e o r ya n d p r a c t i c e c h a p t e r2 s e v e r a lp r o o fs y s t e m s i nt h i sc h a p t e r ，w ew i l lo v e r v i e ws e v e r a lp r o o fs y s t e m so fu n s a t i s f i a b i l i t y ( v a l i d i t y ) f o r p r o p o s i t i o n a ll o g i cf o r m u l a s t h e ya r et a b l e a up r o o fs y s t e m ，w a n g h a oa l g o r i t h m a n di t si m p l e m e n t a t i o n ，a n ds oo n 2 1t a b l e a up r o o fs y s t e m t a b l e a up r o o fs y s t e mi sac l a s s i cp r o o fm e t h o d s m u n y a n ss y s t e mo f a n a l y t i c t a b l e a u x s 6 9 ，s 0 4 ，s i r e 0 4 】i sa9 0 0 de x a m p l e s e m a n t i ct a b l e a u xs y s t e m s v e r e f i r s ti n t r o d u c e dd u r i n gt h ef i f t i e s ，b yb e t h ，k a n g e r ，h i n t i k k aa n ds h z t t ea l r a o s t s i m u l t a n e o u s l y b 5 5 ，k 5 7 ，$ 7 7 ，h 9 5 t a b l e a up r o o fi sas y s t e mf o rb u i l d i n gp r o o f so fp r o p o s i t i o n a lf o r m u l a sa n dt h e p r o o f sw i l lb el a b e l l e db i n a r yt r e e sc a l l e dt a b l e a u x 【n s 9 3 ( h e r ew ec o n s i d e ro n l yt h e e a s ef o rp r o p o s i t i o n a ll o g i c ) t h el a b e l so nt h et r e e sw i l lb es i g n e dp r o p o s i t i o n a l f o r m u l a s ，t h a ti sap r o p o s i t i o n a lf o r m u l ap r e c e d e db ye i t h e rato ra nf ( w h i c hw e c a l lt h i n ko f 醐i n d i c a t i n ga na s s u m e dt r u t hv a l u ef o rt h ep r o p o s i t i o n a lf o r m u l a ) t h et a b e l so ft h en o d e sc a nb ec a k e de n t r i e so ft h et a b l e a ut h et a b l e a u xc e g l b eb u i l d e di n d u c t i v e l yb yf i r s ts p e e i l y i n gc e r t a i nt r e e sa st a b l e a u x ( t h es o - c a l l e d a t o m i ct a b l e a u x ) a n dt h e ng i v i n gad e v e l o p m e n tr u l ed e f i n i n gt a b l e a u xf o rc o m p o u n d p r o p o s i t i o n a lf o r m u l a sf r o mt a b l e a u xf o rs i m p l ep r o p o s i t i o n a lf o r m u l a s t h ei n d u c t i v ed e f i n i t i o no ft a b l e a u xi sb a s e do nt h ef o l l o w i n g1 a b e l l e db i n a r y t r e e sa st h ea t o m i ct a b l e a u xf o ra n yp r o p o s i t i o n a lf o r m u l a sqa n d 口a n dp r o p o s i t i o n a l l e t t e ra ( a st a b l e1 ) t h ep l a no ft h ep r o c e d u r ei st os t a r tw i t hs o m ee n t r y , i e ，s o m es i g n e dp r o p o - s r i o n a lf o r m u l a ，s u c ha sf a ( f _ 1 a ) ，a n da n a l y z ei ti n t oi t sc o m p o n e n t si ns u c ha w a ya st os e et h a ta n ya n a l y s i s1 c a d st oac o n t r a d i c t i o n w ew i l lt h e nc o n c l u d et h a t w eh a v er e f u t e dt h eo r i g i n a la s s u m p t i o nt h a ta ( - 1 a ) i sf a l s ea n ds oh a v eap r o o fo f 5 6c h a p t e r2 s e v e r a lp r o o fs y s t e m s q ( 1 口) d e f i n i t i o n6 ( t a b l e a u x ) ：af i n i t et a b l e a ui sab i n a r yt r e e ，l a b e l l e dw i t hs i g n e d p r o p o s i t i o n a li o r m u l a sc a l l e de n t r i e s ，w h i c hs 删s f i ut h e o l l o w i n 9i n d u c t i v ed e f i n i - l i o n ： ( 1 ) a l la t o m i ct a b l e a u xa r ef i n i t et a b l e a u x ( 2 ) i | ti sa 舢i t et a b l e a u , pap a t ho rt ea ne n t r yo f to c c u r r i n 9o npa n d 丁i so b t a i n e d 加m 丁的a d j o i n