（计算机应用技术专业论文）max（2）公式改名的复杂性.pdf

原创眭声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究所取得的成果。除文中已经注明引用的内容外，本 论文不包含任何其他个人或集体已经发表或撰写过的科研成果。 对本文的研究在做出重要贡献的个人和集体，均已在文中以明确 方式标明。本人完全意识到本声明的法律责任由本人承担。 论文作者签名：型量鱼擅日期呈q q 盈皇旦 关于学位论文使用授权的声明 本人完全了解贵州大学有关保留、使用学位论文的规定，同 意学校保留或向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅舜口借阅；本人授权贵州大学可以将本学位论 文的全部或部分内容编入有关数据库进行检索，- j - 以采用影印、 缩印或其他复制手段保存论文和汇编本学位论文。 ( 保密论文在解密后应遵守此规定) 论文作者签名：巡鲎擅导师签名： 泌 ，q 摘要 一个c n f 公式，称为极小不可满足的( 彤) ，如果f 是不可满足，并且在， 中删去任意一个子句后所得到的公式是可满足的一个m u 中的公式f 称为最大 的，如果对于任意一个子旬f e f 且对于任意一个文字l ，正，工仨，将l 添加 到子句f 中，公式f 变为可满足的最大的极小不可满足公式类记作m a x ， m a x ( k ) = m u ( k ) c 、m a x 公式f 的一个改名是一个定义在v a t ( f ) 上的函数妒，使 得对每个变元x ，认x ) x ，x ；公式f 的一个变元改名是v a k f ) 上的一个置换； 公式，的一个文字改名是一个变元改名和一个改名的组合。以上这三种改名不改 变公式的可满足性。 改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重 要作用。许道云教授已经证明：m u ( k ) 中的变元和文字改名都等价于图同构的判 定问题，而图同构的判定问题是n p 问题。最近，许道云教授找到了一个极小不 可满足公式的子类m a x + 公式，该类公式的变元和文字改名的判定问题可 以在多项式时间内完成，并指出m a x + o ) 公式的改名判定时间是o ( n 2 ) 本文基于上述结论，利用h a n s k l e i n eb r i n i n g 教授提出的分裂技术，先对一 些满足特殊条件的m a x + 公式的结构进行了分析，发现了一些规律。之后，利用 这些规律，再对m a x + ( 2 ) 公式的结构进行了分析，发现任何一个m a x + ( 2 ) 公式 的结构必然具有如下情况之一： ( 1 ) 有两个全出现变元，且每个变元在公式f 的正负出现次数至少为2 ： ( 2 ) 有唯一的全出现变元； ( 3 ) 没有全出现变元，但有1 到3 个准全出现变元，且每个变元在公式f 的 正负出现次数至少为2 ： ( 4 ) 没有全出现变元和准全出现变元，但有唯一的一对匹配变元对，并且在 这对变元中至少有一个变元在公式f 中的正负出现次数至少为2 。 这些结构特点保证了两个m a x + ( 2 ) 公式是否有改名函数的问题可以在 o ( n 2 ) 时间内完成。本文给出了相应的算法，并进行了证明。 关键词：m a x + ( 2 ) 公式、改名，复杂性 中图分类号：0 1 4 1 1 文献标识码：a a b s t r a c t ac n ff 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 v ) ，i ft h e f o r m u l afi s u n s a t i s f i a b l ea n dd e l e t i n ga l la 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 e f o r m u l a af o r m u l afi n 删i sc a l l e dm a x i m a l 。i ff o ra n yc l a u s e f e f ， a n yl i t e r a la n d 也，上t f ， a d d i n glt ofy i e l d sas a t i s f i a b l e f o r m u l a t h es e to fm a x i m a lm i n i m a lu n s a t i s f i a b l ei sd e n o t e da sm a x a r e n a m i n go ff o r m u l afi sam a p p i n g 妒o v e rw 们s u c ht h a t 氟对e “q f o re v e r yv a r i a b l e x av a r i a b l er e n a m i n gi sap e r m u t a t i o no fv a r i a b l e s al i t e r a lr e n a m i n gi sac o m b i n a t i o no fav a r i a b l er e n a m i n ga n dar e n a m i n g t h er e n a m i n g so ff o r m u l a sd o n tc h a n g et h es a t i s f i a b i l i t yo ff o r m u l a s t h er e n a m i n g sh a sp l a y e das i g n i f i c a n tr o l ei ns i m p l i f y i n gr e s o l u t i o n p r o o f s o f s o m eh a r df o r m u l a sa n d c o n s t r u c t i n g t h ee f f i c i e n t s a t i s f i a b i l i t ya l g o r i t h m s p r o f e s s o rd a n y u n x uh a sp r o v e dt h a t t h e v a r i a b l ea n d l i t e r a lr e n a m i n gp r o b l e m so ft h ef o r m u l a si nm u ( k ) a r e e q u i v a l e n tt ot h eg r a p hi s o m o r p h i s mp r o b l e ma sw ek n o w n ，t h eg r a p h i s o m o r p h i s mp r o b l e mi ss t i l li n ，r e s e n t l y 。p r o f e s s o rd a o y u n x ua n dh i s s t u d e n to i n g y a n c h e nf o u n dan e ws u b c l a s si nm uf o r m u l a s ，w h i c hi s c a l l e dm a x + f o r m u l a s 。a n di nw h i c ht h ev a r i 曲l ea n dl i t e r a lr e n a m i n g p r o b l e m so ff o r m u l a si sp o l y n o m i a l a n dt h e yp o i n tt h a tt h er e n a m i n g p r o b l e m si nb z 4 x + 0 ) f o r m u l a si ss q u a r e b a s e do na b o r ec o n c l u t i o n s w es h o ws o m er u l e sa b o u t 劓r a z + f o r m u l a s u s i n gt h es p l i t t i n gt e c h n i q u eb r o u g h tb yp r o f e s s o rh k l e i n eb r i n i n g w i t h t h eh e l po ft h e s er u l e s ，w es h o wap r o p e r t ya b o u t 脚+ ( 2 ) t h ep r o p e r t y t e l l su st h a te v e r yf o r m u l afi n 脚+ ( 2 ) h a v eo n eo ft h ef o l l o w i n g s t r u c t u r e s ： ( 1 ) t h e r ea r et w o 伽1a p p e a r a n c ev a r i a b l e si n f ，a n de v e r yv a r i a b l e a p p e a r si nfa tl e a s tt w ot i m e s “+ ” a n dt w ot i m e s搿一”： ( 2 ) t h e r ei so n l yo n e 向j 1a p p e a r a n c ev a r i a b l ei nf ： ( 3 ) t h e r ea r eo n l yo n et ot h r e en e a r l y 删1a p p e a r a n c ev a r i a b l e s , a n d e v e r yv a r i a b l ea p p e a r si nfa tl e a s tt w ot i m e s “+ ” a n dt w ot i m e s“一”： ( 4 ) t h e r ei so n l yap a i ro fm a t c h i n gv a r i a b l e s , a n da tl e a s to n eo f t h e ma p p e a r si nfa tl e a s tt w ot i m e s“+ ”a n dt w ot i m e s。一” a c c o r d i n gt ot h i sp r o p e r t y ，w ep r o v e dt h a tt h ev a r i a b l ea n dl i t e r a l r e n a m i n gp r o b l e m si nm a x + ( 2 ) f o r m u l a si ss q u a r et o o w es h o wa n dp r o v et h e a l g o r i h ma b o u tt h i sq u e s t i o ni nt h i st h e s i s k e yw o r d s ：m a x + ( 2 ) ，r e n a m i n g , f o r m u l a s , c o m p l e x i t y 2 第一章绪论 一个文字是一个命题变元或命题变元的否定一个子句c 是文字的析取范式 ( c = 也v v k d ，有时将子旬c 表示成一个文字集合( c ；瓴，l ) 。一个合取范式( c s f ) f 是子句的合取扩= ( c l 一c * ，有时将，表示成一个子句集合护z 虹，g ) 或一个子句序 列护= i c , c d 。设自然数啊r 2 i ，记c 肝o ，) 为含有n 个变元和，个子旬的c n f 公式的集 合通常，记公式类f “) = u 。c n f ( ，l ，n + k ) ，整数k 被称为公式差。 对于一个c n f 公式，给定了该公式中的所有命题变元的真假赋值后。就可以判断这个 公式在该赋值上是否满足若存在一个赋值使该公式满足，则称该公式可满足；若不存在赋 值使该公式满足，则称该公式不可满足。对于，( t ) 中的公式，可满足性问题是p 一完全的。 如果一个c n f 公式，是不可满足。并且在f 中删去任意一个子旬后所得到的公式是可满足 的，则称f 为极小不可满足的( m u ) 【l l 】。判断一个c n f 公式是否为一个极小不可满足公式 问题是d p 一完全的。其中是被描述成两个n p 问题的差的一些问题的集合【l l 】。记m u ( k ) 为含有一个变元n + k 个子句的极小不可满足公式的集合。 一个h o r n 子旬是最多含有一个正文字的子旬。一个h o r n 公式是一些h o m 子句的析取。 在文献【6 】中，g d a v y d o v ，1 d a v y d o v a 和h k l e i n eb o n i n g 证明了在公式集，( o ) 中没有极小不 可满足公式。一个极小不可满足的h o m 公式属于f ( 1 ) 【6 】。另外，对，( 1 ) 中的极小不可满足 公式，至少存在一个变元在公式中的两个不同子句中的出现为一正一负【6 】。对于一些公式 子类，例如h o m 公式、2 - c n f 公式，极小不可满足问题都可以在平方时间内解决【6 】。在 文献【1 2 】中，o k u l l m a n n 证明了，对于公式集，( t ) ，极小不可满足判定问题在多项式内可解 决。 i i 引言 在文献【l l 】中，c h p a p a d i m i t r i o u 和d w o l f e 证明了对任意一个公式，可以在多项式 时间内构造出另一个公式，( ，) 满足： f 可满足，当且仅当厂( f ) 可满足； f 不可满足，当且仅当，( ，) 极小不可满足 也就是说，一个不可满足公式在多项式时间内可以转化为一个极小不可满足公式。所以 通过极小不可满足公式来研究不可满足公式就显得非常有意义 分裂技术是研究极小不可满足公式结构的有效工具。在一个公式，中，取出一个变元， 我们对他进行真假赋值，= 0 和，= i ，从而来考察赋值后得到的新的公式对极小不可满足 公式的一个变元赋值后，得到的公式仍是极小不可满足公式。也就是说，极小不可满足公式 通过分裂得到的公式保持了极小不可满足性。特别地，建立在分裂技术上的归纳证明是可行 的并且容易得到一些公式类的性质。因此我们对那些在分裂下保持封闭的公式类感兴趣。 改名技术是研究两个c n f 公式是否相同的一种技术，包括变元改名、改名和文字改名， 其中文字政名是改名和变元改名的组合。 改名技术在简化一些难例公式的消解证明和构造高效的可满足算法方面有重要意义。 首先，改名技术可以改进可满足性算法。众所周知，对称规则允许如f 推演：如果一个 子句厂已经从子句集f 中推导出，而且9 是出现在f 内的变元集合上的一个置换，则下一步 证明可以引入子句“，) 在文献【1 3 】中，k r i s h n a m u r t h y 举例说明了命题证明系统中对称规 则的作_ h j i 。他将对称规则应用到消解子句中，给出了一些难例公式更短的证明。众所周知， 一些难例公式有很好的对称结构。例如，鸽巢公式就是因此而有一个多项式大小的证明。在 文献【1 4 冲可以找剑更多相关内容。 另外，改名技术对改进一些算法也有很大帮助。例如，在文献【1 5 1 中。作者将改名技术 应用在了d p l l 算法中假设在d p l l 算法中根据变元分裂产生的二叉树中，有两个节点上 的公式之问存在改名函数，那么就可以把其中一个节点用空公式来代替，从而降低该公式的 二叉树的节点规模，算法中与这个公式有关的证明也可以相应简化 可见，改名技术在可满足性问题的研究上有重要意义，特别是对极小不可满足公式的研 究 1 2 研究动机 对于不可满足公式，中的个子句，如果在，中添加一个其正负都不在，中出现的文 字后，就得到一个可满足的公式，则称该子句，在，中是最大的( m 靠i m d 如果个极小 不可满足公式中的任何一个子旬都是最大的，则该公式是一个最大的( m a x i m a l ) 极小不可满 足公式记这类公式为j 椴。记j 缎( d - 脚w d n j “r 在文献1 1 0 中介绍了一种把极小不 可满足公式构造成一个最大的极小不可满足公式的方法 对于不可满足公式，中的一个子句，如果删除，中任意个文字工后，就得到一个可 满足的公式，则称该子旬，在f 中是边缘的m 瞰g i n 嘶如果一个极小不可满足公式中的任 何一个子旬都是边缘的，划该公式是一个边缘的( m 椰口n 哟极小不可满足公式记这类公式 为脚，记j “日g ( 的- m y o ) n 肛t 舳在文献 1 0 1 中介绍了一种把极小不可满足公式构造 成一个边缘的极小不可满足公式的方法 在文献【4 】中，作者对极小不可满足公式及其诸多子类的改名问题进行了研究，发现大 多数问题都是n p 一完全的或者等价于图同构问题，而图同构问题的判定是肿的只有子类 尬o ) 和m a r c ( t ) 的改名问题是多项式的此后，文献【4 1 的作者在极小不可满足公式的改名 问题上又做了进一步研究，在f 9 】中构造出了一个新的极小不可满足公式子类一勉“+ 公 式，该子类的改名问题在多项式内可解，指出了该子类中的 螂+ o ) 公式的改名问题在平方 时闯内解决 肛戗+ 公式类是通过一种递归方法构造出的一个极小不可满足公式的子类该子类的定 义为脚+ - 扩e 似i 玉e w ( ，) 。v 分裂对以，l ) ：厶l e 脚+ u 臼 ) j 砌+ 一j 棚砸) n x 1 3 研究的问题 本文基于上述结论，利用h a n s k l e i n eb a m i n g 教授提出的分裂技术，先对m a x 公式的 结构进行了分析，发现两个m a x + 公式如果若干个子旬相同时，它们的结构满足下面几个特 点： ( 1 ) 两个肥饼+ 公式g 和片，若有如下形式，g z b 色c ，窖) ，日一“白c ， ) ， 则有g = ，即g 日 ( 2 ) 两个肥t r 公式g 和h ，若有g = “屯g ) ，圩= g 龟c r 也) ，则 公式g 和h 的结构有如下情况： g = ( c c ，c ，：) ，日= ( c 。c ，c ，：】 ( 3 ) 两个胁货+ 公式g 和h ，若有g = 如晚矗9 2 ) 。h 生g 岛q 毛) ， 则有公式g = h 或者公式g 和h 的结构有如下情况： 若# v 嘶g ) 玮( 田3 ，则g 和仃的结构必是下列情况之一l 若# 旧群( j j f ) - 2 ，则g 和h 的结构必是下列情况之一； 舢、g = c ： b ) g ，f + +。 p o 、g 七： 日t c + 0 i ( + ： h z c 4 + - 若# v 缸6 3 # ；i ，则g 和的结构必是该情况：g - h t “_ ) 根据这些结构特点，通过分裂验证的方法再对肛“+ 公式的结构进行了分析，发现任 何一个m a x + ( 2 ) 公式的结构必然具有如下情况之一# ( 1 ) 有两个全出现变元，且每个变元在公式f 的正负出现次数至少为2 ； ( 2 洧唯一的全出现变元； ( 3 ) 没有全出现变元，但有l 到3 个准全出现变元，且每个变元在公式f 的正负出现次 数至少为2 ： ( 4 ) 没有全出现变元和准全出现变元，但有唯一的一对匹配变元对，并且在这对变元中 至少有一个变元在公式f 中的正负出现次数至少为2 脚+ ( 2 ) 公式的这种结构特点，保证了两个肛( 2 ) 公式是否有改名函数的问题可以在 以t ) 时间内完成。本文给出了该改名算法，并对其复杂性进行了理论证明 5 吣习n习们习们习 o + c o + c 一 + f + + c 略 q 0 吩 气 岛 怕 、 h ， h 、， h 、 厅 日 日 0为0习0纠0圳 + o c + o c + 一 c + o c q 弓 o q 一 一 一 岛 岛 h 、 旧 ， h ， h 、 g g g g 从 队 趴 卧 争 j 习j 第二章m u 公式和删矿公式 在本章中，将介绍有关命题逻辑和a 盯公式、极小不可满足似u ) 公式和最大的极小不 可满足( m t _ r + ) 公式的一些概念，定义及相关结论 2 1 命题逻辑和c 伊公式 命题逻辑( p r o p o s i t i o n a li o g i c ) 是最简单的逻辑系统，但计算机科学和数学优化中的许多 重要研究分支和著名问题却源于命题逻辑命题逻辑的研究对象为只考虑取“真”、。假”值 的命题通常用 “，这些符号代表任意的命题，称为命题变元【l 】常用1 , 0 或1 ，表示 命题变元的真假值由命题变元出发，经过使用逻辑联结词“与”( 又称“合取”，记作，、) 、 。或”( 又称。析取”，记作v ) 、。非”( 又称。否定”，记作，) ，“蕴涵”( i r 作- + ) 、。等价” ( 记作 ) 可以构成命题逻辑公式，其定义如下 定义1 1 ( 命题逻辑公式) 【2 】 ( 1 ) 命题变元是公式( 称为原子公式) c 2 ) 若口和卢是公式，那么o 办和v 几卜口x 似_ 觑( 口”力也都是命题公式 ( 3 ) 一串符号是命题公式当且仅当它可以由( 1 ) 和c 2 ) 得到 倒如：设，b , c 是命题公式，则( v 毋c 似 毋_ c ) “彳毋_ c ) 都是命题公式，而 一一、( v 丘“_ 一) 都不是命题公式定义i 中的( 3 ) 很重要，它告诉我们怎样以原子公式 作为基，使用连接符号归纳得到命题公式 命题逻辑是公式的语言每个公式都有一定的意义，也就是真假值t 或者f ，它的值是 由命题符号所包含的内容决定的。命题公式的值可以通过真值表计算得到 定义2 ( 真假赋值) 【2 】 真值赋值是一个从命题变元集合到真假值集合 o l l 拘函数，简称赋值，又叫解释 定义3 ( 公式的真假值) 【2 】 真假赋值r 给公式指派的真假值递归地定义如下： ( i ) “田e l o ； ( i j ) ；托如黜一； ( i i i ) 酗nb ) = 七如果7 等卿1 ： 舭v b ) 。以如果7 峰孑删； ( v ) 啦一b ) = ：髁喘孑件1 ； 啦”b ) = ：螈省一 定理1 对一个真假赋值4 有唯一的真假值，使得v ( 口) = a 口) 其中口为命题公式中的任一文 字 一个可满足公式是指有真假赋值后，得到的结果是t 定义4 ( 永真公式或重言式) 【2 】 一个命题公式矿称作是有效的，如果对于任何真假赋值r 都有r 细) ；1 满足这样性质的命 题公式称作永真公式，也叫重言式。 6 例如：公式( p v 呻) 是重言式，因为对任意赋值r ，无论r ( 。l 还是f ( p ) - l ，都有r ( p v - - p ) - i 定义5 ( 永假公式或不可满足公式) 【2 】 命题公式矿是不可满足的。如果对于任意真假赋值r 。都有r 西- o 例如：公式o 呻) 是不可满足公式，因为对任意赋值f 无论r ( ：) f f i l 还是t ( 力。i ，都有 定义6 ( 可满足性公式) 【2 】 命题公式妒是可满足的，如果存在某个真假赋值t ，有f = h 原子公式或其否定为文字( i i 懈砷原子公式本身称为正文字，而原子公式的否定称为负文 字若干个文字的析取构成子句( c i 跚s e ) 。其长度是指所古文字的个数只有一个文字的字 句称为单子句( m l i t c l 踟s e ) 没有文字的子旬称为空子旬( m p t y c l a u s e ) ，记为口 定义3 ( 合取范式和析取范式) f 1 】 若干个子句的合取是一种特殊形式的公式，称为合取范式( c o n j t m c t i v cn o r m a lf o r m ) ，简写 为c n f ，其一般形式为( 。v - * - v k ) ( k v v 五) 这里的每个与是文字一个公式 被称为析取范式( d i s j u n c t i v en o r l l l s lf o r m ) ，简写为d n f ，如果他的形式为nv - - 。伟这里每 定理2 【1 1 对任意公式，都有与之等值的合取范式和析取范式 一个文字是一个命题变元或命题变元的否定一个子旬c 是文字的析取范式 缸t “v v k ) ) ，有时将子句c 表示成一个文字集合( c z 他。，工_ ) 一个合取范式( c f ) f 是子句的合取( ，= ( c j 一一g ) ) ，有时将f 表示成一个子旬集合( ，一b 。，c ) 或一个子旬序 列( ，= b 一g d ”护) 表示出现在公式f 中的变元集合，酬一表示变元集合妒) 上的 文字集合妒) 、d ( ，) 分别表示出现在公式f 中的变元个数和子旬个数，舯如，) 、 懈仗，) 分别表示变元，在公式f 中出现的正、负次数记k ，) = ( 础，l 嗍如，) ) 对 一r l ，记伽“r ) 为舍有一个交元和r 个子旬的c n f 公式的集合通常，记公式类 ，证) ；l k a 矿“一+ i ) ，整数k 被称为公式差 设，是一个舍有文字的公式，则公式巧。，有如下定义 如果，包含单子句越，则铀，= 口( 空公式) ；否则压删是由下面方法得到的公式： ( 1 ) 对任意个子句，e f 。若有l e ，则从f 中删除厂； t 2 ) 对任意一个子旬，e f ，若有屯e ，。则从f 中删除 公式石。们有类似定义 定义9 ( 公式的表示矩阵) 3 1 设，；b ，。c 是带有一个变元却，i ，m 个子句的公式。如下定义的一m 矩阵坼t “。) = ；曩 ( 有时用空白表示o ) 2 2 改名 定义1 0 ( 改名，变元改名，文字改名) 【3 】 ( 1 ) ( 改名) 设h 和f 都是c n f 公式，则一个映射尹：州册_ 衙( n 被称为一个从j j r 到f 的 改名，当且仅当对所有l e l i t ( h ) ，有“) e 厶埘和* 吐) - ，烈d ，其中符号一表示逻辑等 7 价 c 2 ) ( 变元改名) 设和，都是c n f 公式。且有( 研- 州乃，则一个映射9 ：州哪_ i ，) 被称为一个从日到f 的变元改名，当且仅当一是一个满足“田- f 的置换 ( 3 ) ( 文字改名) 设日和f 都是( 3 v f 公式，则一个映射，：似册_ 坝n 被称为一个从h 到f 的文字改名，当且仅当p 是一个坝研上的置换，且对所有e m ( 哪，有氟卅- ，烈d ，其 中符号- 表示逻辑等价 注意：一个文字改名是变元改名和改名的复合 2 3 朋可公式 在这部分，我们将给出一些关于极小不可满足公式的简单事实：另外，还会给出几个 重要的定理和引理，包括它们的证明最后。我们还将给出关于极小不可满足公式的子旬个 数的一个下界，印一个含有一个变元的极小不可满足公式至少要包含n + 1 个子旬 定义n ( 极小不可满足公式) 【4 】 一个c n f 公式，是极小不可满足公式( m i n i 啪iu x k s a t i s f m b l ef o r m u l a ) ，简记为m u 公式，如 果：( 1 ) f 是不可满足的；( 2 ) 对于任一予旬f e f ，都有公式，一t 介是可满足的 也就是说，一个c n f 公式f 是极小不可满足的，当且仅当这个公式是不可满足的，且 删去任意一个子句后产生的公式是可满足的。判断一个c n f 公式是否为一个极小不可满足 公式的问题是d p 完全的，其中d p 是所有可以描述成两个n p 问题的差的问题的类 下面的定理说明了关于极小不可满足公式的子句个数的一个下界 定理3 【5 ，6 】 如果公式f e c n f ( n , r ) 。且r 一，则公式f 不可能是一个极小不可满足公式。 因此，假设有k 2 1 ，我们记： m u ( k ) = f e c n f “ + d i f f u ； 删z ，i f e m u = u _ m u ( k ) 下面介绍一些有关极小不可满足公式的一些事实； 事实1 【9 1 含有永真子旬的公式不是极小不可满足公式； 含有重复出现的子句的公式不是极小不可满足公式； 如果一个变元在公式中只有正或负的出现，则该公式不是极小不可满足公式； 如果一个公式包含一对互补的单子句和其它子旬，则该公式不是极小不可满足的： 如果一个公式包含一个单子句l ，并且另外有一个子旬包含文字或没有子句包含文字 也，则该公式不是极小不可满足公式 下面介绍i - l k l e i n eb o n i n g 教授提出的分裂定理，该定理可以降低极小不可满足公式的 公式差首先，先说明几个记号 设，是一个极小不可满足公式，且有f = v 石卜。( x v f , ) , ( - a v 9 0 , ，( - - a v g , ) ，1 ，其中 变元，不在中出现则记，扣m 。正】，l z k ，岛1 ，f e = 融v m ，o v 工以及 f i ：；【( 吐v 霸x ，吖v 岛 通常，若记公式，t 【，e ，巨，c 噩。，朗，【f k ，以，c 】和【，l ，丑。，q 都是极小不可满足公式， 分别记e = 扩l ，且，c 】、f - 【f l i ，罡。，c 】，则称公式对( 昂f 0 ) 为公式，在变元，上的分裂对 下面介绍分裂定理 定理4 ( 分裂定理) 【7 】 设公式f e j 4 - u ( t ) ，其中k i 对f 中的任意变元j 有c “一( z 2 ) 不妨设f 有形式： f = v f a ，o v x 且，c 疋，窖i 卜vg ，其中以，c 昱。是f 中的不含文字j 和q 的 8 子旬的合取，对特定的和t 。有五i m 。，e ，q e 删以) ，l = 喃，& ，罡。，q e 删( k ) 则有i t 。l _ i 如果c = 口，即c 是空公式，则该分裂被称为析取分裂( d i 萄珊c t i 强s p l i t t i n g ) ，变元，被称 为析取分裂( d 蠲1 m c t i v ev m a b l e ) 引理1 ( 消解规则) 【6 】 设公式，e c n f ( n + l , t + i ) ，变元，的正、负文字，和一在公式f 中的出现都只有1 次，即 公式有形式；f 。融v 石) 似v 五x 磊, - - - , f , 。1 ，劓f 是极小不可满足的当且仅当 e m v 五x 再，z 。1 e c r ，o 是极小不可满足的 引理2 ( 单子句消解) e 6 】 设公式f e c n f ( n , ，) 。其中一1 如果公式f 包含一个单子句l ，其它子旬不包含文字， 也没有单子旬也，且，中至少有一个包含文字。的子句则：公式，是极小不可满足公式， 当且仅当j i 1 c n f ( n l , r 1 ) ，且五卅是极小不可满足的 定义1 2 ( 仉) 一消解) f 6 】 设公式，一睢v n ( 正霸卜，也。“x l 是一个c w f 公式，其中e 。不包含和山则 公式n 【( 厂v 譬l n ，u v g k 】称为公式，关于文字的一个0 ) 一泊解 引理3 f 6 】 设公式f ；【( 工v 力( 1 工v 暑t 卜，h l 。g j 1 是一个c j v f 公式。其中不包含和山则 公式f e 删( t ) 。其中i i ，当且仅当公式f i o r v 白卜。o r 。暑，x ，一e 枷( t ) 通过引理3 可知，对于一个极小不可满足公式f e m i y ( k ) ，o ) 一消解保持公式的极小不 可满足性，且公式差不变 引理4 1 6 x q t - t l e 数一和m ，设公式f = 瞒。，l 1 是a 暇 辨) 中的极小不可满足公式若对某个文字 ，若有，一= 【( v x 五，厶】是不可满足的，则，是极小不可满足的 f 是c n f 公式，是一个不在f 中出现的文字，定义l v d f z ( v 力i ，e 毋 引理5 【6 】 设公式ee 觚，盹) 和五e 觚，( 毛) ，对于公式6 和五，是一个新文字则公式( l v a f , ) + “v d 五) e 埘，其中t = 毛+ 屯+ i 州e ) n 埘i 五) l - l 定理5 【6 】 设公式f e 觚，o ) ，则f 中存在一个变元，其正负文字在f 中都只出现1 次。即有 o “乃= 0 , d 定理6 嘲 设公式f 是一个极小不可满足的h o r n 公式，则f e m u 0 ) 定义1 3 ( 基础矩阵) 【6 】 由下列方法递归构造的具有一行n + l 列的矩阵是基础矩阵： ( 1 ) “- ) 是基础矩阵； ( 2 ) 如果马是基础矩阵，则下面的矩阵也是基础矩阵： 暖匀 其中， 是一个取值于 o + 的向量，且至少有一个。+ ”出现； o ) 如果置是基础矩阵。则下面的矩阵也是基础矩阵： ( + 劫 其中，击2 是一个取值于 o - 的 句_ 量。且至少有一个。一。出现： 9 ( 4 ) 如果丑和马是基础矩阵，则下面的矩阵也是基础矩阵： 一0 1 l 屯l l o 岛j 其中， 是一个取值于 ” 的向量，且至少有一个。+ ”出现；屯是一个取值于 o ，- 的 向量，且至少有一个。”出现 在文献【6 】中，作者已经说明了觚，( 1 ) 公式的矩阵表示经过行列置换后，是基础矩阵这 意味着，u u 0 ) 公式可以通过递归来构造 定理7 【6 1 公式fej a - u 0 ) ，当且仅当f 的矩阵表示通过行列置换后，是基础矩阵 定理8 【刀 设，e 肿1 2 ) ，对，中的任一变元，有“n 仁2 ) ，则对任一变元，有“n z ( 五2 ) 定理9 【7 】 设f e 删( 2 ) 。对，中的任一变元j 有“乃( 2 ，2 ) ，剐，可被写成： f l 【( 呻v 毛卜。1 丐一v 而l 吨v 而x “v v 而) ，( 1 畸v v 吨) 】，或者下面矩阵的形式： 一 + ： ： + + +一一 4 - 一一 本部分，我们先介绍最大的( m a x a 越1 ) 极小不可满足公式，简记为m a x 公式接着介绍 m a x 公式的子集一脚+ 公式。最后，再介绍一种递归构造肛“+ 公式的方法 设f 是一个极小不可满足公式，且有，。眙v 五卜，o v ，= k u v 卜，。v9 1 ) 1 ，其中 变元j 不在中出现则记，l l m ，朋，f l 一嘶，盾l ，弘眙v 石卜- ，( x v , ) 1 以及 ，c t 【( 叫v 窖l 、- i * 9 ( 蟒v & ) 】 通常，若记公式f = i f c 。易c ：丑。f 明，旷l ，疋，q 和【，l ，丑。，q 都是极小不可满足公式， 分别记c ；【，i 。，c l 、f = i f l ，罡。，c 】，则称公式对( e 。l ) 为公式f 在变元，上的分裂对 定义1 4 ( 最大的( 邛日i 啪1 ) 极小不可满足公式) 【4 】 一个极小不可满足( 埘) 公式f 是最大的( m a x i m a l ) , 如果增加任意一个文字弛e 州聊到 f 的任子句c 中后( 请注意：t c ) ，产生的公式是一个可满足公式 记肛“为最大自q ( m a 虹m a i ) 觚，公式的集合，j 执y o ) = 觚，( ”n 膨 也就是说，如果公式f 中的子旬，是最大的( m a 】i m a l ) ，则向，中任意添加一个不在，中 出现的文字后得到的公式是可满足的。公式，e 删是最大的极小不可满足公式，即脱仃公 式，当且仅当f 中的任何子句都是最大的( m 戤i m a i ) 。在【8 】中，作者已经说明判定脚公式 的问题是d ，一完全的 下面介绍一些眦讲公式的特殊性质 引理6 【6 】 设公式，e 埘让) j e 们，( c ，f 。) 是公式f 在变元，上的分裂对，其中e t i ，k ，以，c 】， l z 旷b 罡。，c 1 如果e ，则公式，= f 一乓4 - x v 。也是极小不可满足公式 证明：见文献【6 】。 1 0 推论1 设公式f e 似，e 仰。( 只。l ) 是公式在变元，上的分裂对，其中e ；i ，k ，疋，c 】， l = w i - ，丑。，6 1 则有或= 丑= ， 推论2 设公式f e m c x ( k ) ，变元j e 妒) 则公式，的分裂对【e ，e 。) 是唯一的 推论3 设公式f e m o c o ) ，变元，t 妒) tf 有形式，一钕v 石卜，讧v 五) ，。暑l 卜。爵x o t 【，e ，f c ，k 】 。 事实2 设公式f 是极小不可满足公式，是们上的文字，且l c f 则，是不是最大的( m 旺衄a d 当且仅当f t 力+ 工v n 是极小不可满足的 定理如 设公式f e m a x ( k ) ，变元，e 州f ) ，有p = f c ，c , f 1 则： ( 1 ) 对任一子句，e f i 。和g e f l 。，在旷l 。c l 中是最大的窖在i ，l ，c 】中是最大的； c 2 ) 对任一子旬 e c 和变元集驴) 一协上的文字，如果对于文字h 在【，b ，c l 中不是 最大的，则旷l ，f 】是可满足的；相应地，如果对于文字，h 在【，l ，c 】中不是最大的，则 旷k ，1 是可满足的其中，c t n + 拉v 力 证明：见文献【6 】。 下面介绍m a x 公式的一个子集一j 似+ 公式 定义1 5 ( 肛+ 公式) m a x + = p e m a x l h e w 驴) ，v 分裂对( t ，l ) ：c ，le m a x + u 口) ) 记脚+ 0 ) - m i x + n m x ( k ) 显然，肛t r 公式集是m a x 公式集在分裂上的闭包 众所周知， 似公式有如下性质： ( 1 ) 对任一公式f a 船皤o ) ，存在唯一鼢变元，满足肿慨，) + 譬嘛d 爿c j ( 乃； ( 2 ) 对于公式，在变元j 上的分裂对以，l j ，有 ( c ) n 口但 - ， 显然有她瞰d = j 鲋+ ( 1 ) 肛研+ 定理n 设公式五，e e 脱“u 口 ，是相对于公式e 和e 的新变元对任何子旬集c c 五n 五， 有焉一c 和五一c 非空。则有，t x v d t 焉一c ) + c + - - 口v d 幔一o m a x 证明：见文献网 在定理l l 中，有以下几种特殊情况：( 记v 。= l bl w d ，z ，) ( 1 ) 如果ee m a x ，b = 四，c ；，则f ；，h 巧+ l 叫e 肌“； ( 2 ) 如果e l 丘e 删，c 霉，则，l j 均e + 哺h 五e 脚； ( 3 ) 如果五t f 2 e m 4 x ，c z 厩一 力。，是五中的任一子句，则f = ( x v ) + c + ( - - a v , o e m 4 x ； ( 4 ) 如果五，ee m a x 且v a r ( f o n v a r ( f 0 = # ，c = ，则f = x v # e + q h 五e 肛饼； ( 5 ) 如果月，ee 脚且州点) n 坩( 五) 一，c = 一，则，= j h 耳+ 叫h 五e 脚 下面从构造m a x + 公式的角度给出m a x + 公式的另一个定义 定义1 6 通过下列方法可递归构造出m a x + 公式集中的所有公式 首先，递归构造公式集合r - 如下： ( 1 ) 空公式属于r 二t ( 2 ) 公式o 卅e r ，其中，是一个变元； ( 3 ) 如果公式五，五er o + ，是一个对于e ，e 的新变元，c 是五n e 的子集，且使e c 和 五一c 不为空，则公式l v d ( f , - c ) + c + - 也v d 幔一c ) e r ( 4 ) 如果公式，e r _ + 且f 不是空公式，是对于，的新文字，则公式h ，+ 叱e r 二1 ； ( 5 ) 如果公式昂五t r ，且巧一五，z 是一个新文字，则公式f - h 五+ 正五q f m 。o j 似+ 公式集由右式得到：m a x + = r - - 一 口 此定义给出了一个构造m a x + 公式的方法 在【9 】中，作者已经证明了这种构造m a x + 公式的方法具有可靠性和完备性 在下一章中。将给出关于m a x + ( 2 ) 公式的一个性质根据该性质可将删) r ( 2 ) 公式的改 名目恿在o ( n ： 内完成 1 2 第三章删矿仞公式的一个结构特点 本章将给出关于删( 2 ) 公式的一个结构特点根据该性质可将膨“+ ( 2 ) 公式的改名问 题在o ) 内完成 在说明肋“+ f 习公式的这个特点时，要用到一些关于j “r 公式的结构的一些结论本 章分为两部分第一部分以引理的形式给出了这些结论及其证明。在第二部