（基础数学专业论文）线性公式可满足性判定问题的复杂性.pdf

摘要 可满足性问题( s a t i s f i a b i l i t yp r o b l e m ，简称s a t ) 是计算机科学的中心问题 之一，也是第一个被证明的胛一完全问题，并且是一大类n p 一完全问题的核心。 s a t 问题是指可满足布尔表达式的集合，它在数理逻辑、人工智能、约束可满足 性问题、v i s i 集成电路设计与检测、计算机科学理论、计算机视觉、机器定理 证明、机器人规划、机器学习等领域具有广阔的应用背景。 一个c n f 公式f 称为线性的，如果f 中任意两个不同的子句中至多包含一 个相同的变元。一个c n f 公式f 称为严格线性的，如果f 中任两个不同的子句 恰好包含一个相同的变元。所有严格线性公式是可满足的( 3 3 s p o r s c h e ne t c 2 0 0 6 ) 。对于线性公式类l c n f ，判定问题l s a t 是n p 一完全的。对于l c n f 的 子类l c n f 吐( 其公式中每个子句的长度至少为k ) ，如果在l c n f 出公式中存在 一个不可满足公式，则判定问题三甜l 是p 一完全的( 3 1 ，3 2 s p o r s c h e n ，e s p e c k e n m e y e r , 2 0 0 6 ) 。因此，对于l c n f 出( k 苫3 ) 公式，判定问题l s a 疋t 的尸_ 完全性取决于在l c n f 蔽公式中是否存在不可满足公式。在( 3 1 ，3 2 s p o r s c h e n e s p e c k e n m e y e r , 2 0 0 6 ) 中，通过构造超图和拉丁方阵，已经证明了l c n f 必和 l c n f ：。都包含不可满足公式，并提出了一个公开问题：当k 之5 时，在l c n f d , 公 式中是否存在不可满足公式。 本文基于线性公式的结构与特点，提出了线性化算法，使用该算法可以在i f i 多项式时间内把任一公式f 转化为线性公式f 砌，且两者有相同的可满足性。另 外，本文通过研究极小不可满足公式在公式归约中的应用，给出了在k l c n f ( 其公式中每个子旬的长度都为k ，k 乏3 ) 公式中构造不可满足公式的一般方法。 证明了：对每个k 苫3 ，k l c n f 公式中存在极小不可满足公式，并且证明了下 面更强的结果：对每个k 苫3 ，k l s a t 是n p 一完全的。 关键词：线性公式满足性尸一完全性极小不可满足公式归约算法 中图分类号：t p 3 0 1 5 3 文献标识码：a a b s t r a c t t h es a t i s f i a b i l i t yp r o b l e m ( s a tf o rs h o r t ) ，am a j o rp r o b l e mi nc o m p u t e r s c i e n c e ，w h i c hi st h ef i r s tn p - c o m p l e t ep r o b l e ma n dt h en u c l e u so ft h ec a t e g o r yo f n p c o m p l e t ep r o b l e m s a tp r o b l e mi st h es e to fs a t i s f i a b l eb o o l e a nf o r m u l a s ，w h i c h c a nb ew i d e l yu s e di ns u c hf i e l d s 弱s y m b o l i cl o g i c ，a r t i f i c i a li n t e l l i g e n c e ，c o n s t r a i n t s a t i s f a c t i o n p r o b l e m ，d e s i g na n dd e t e c t i o no fv l s ii n t e g r a t ec i r c u i t ，t h e o r i e s o f c o m p u t e rs c i e n c e ，c o m p u t e rv i s i o n ，p r o o f o fm a c h i n e t h e o r y , r o b o tp r o g r a m ，a n d m a c h i n el e a r n i n g ac n ff o r m u l afi sl i n e a ri fa n yd i s t i n c tc l a u s e si nfc o n t a i na tm o s to n e c o m m o nv a r i a b l e ac n ff o r m u l afi se x a c tl i n e a ri fa n yd i s t i n c tc l a u s e si nf c o n t a i ne x a c t l yo n ec o m m o nv a r i a b l e 甜le x a c tl i n e a rf o r m u l a sa r es a t i s f i a b l e ( 3 3 s p o r s c h e ne t c ，2 0 0 6 ) ，a n df o rt h ec l a s so fl i n e a rf o r m u l a s l c n f ，t h ed e c i s i o n p r o b l e ml s a tr e m a i n sn p c o m p l e t e f o rt h es u b c l a s s e sl c n f 出o fl c n f ，i n w h i c hf o r m u l a sh a v eo n l yc l a u s e so fl e n g t ha tl e a s tk ，t h ed e c i s i o np r o b l e m l s a 疋ir e m a i n sn p c o m p l e t ei ft h e r ee x i s t sa nu n s a t i s f i a b l ef o r m u l ai nl c n f 一, ( 【3 1 ，3 2 s p o r s c h e n ，e s p e c k e n m e y e r , 2 0 0 6 ) t h e r e f o r e ，t h en p c o m p l e t e n e s so f s a tf o r l c n f 缺( 七3 ) i st h eq u e s t i o nw h e t h e rt h e r e e x i s t sa nu n s a t i s f i a b l e f o r m u l ai n l c n f , k i n ( 【3 1 ，3 2 s p o r s c h e n ，e s p e c k e n m e y e r ，2 0 0 6 ) ，i ti ss h o w nt h a t b o t hl c n f 3a n dl c n f , 4c o n t a i nu n s a t i s f i a b l ef o r m u l a sb yt h ec o n s t r u c t i o n so f h y p e r g r a p h sa n dl a t i ns p u a r e s i t l e a v e st h eo p e nq u e s t i o nw h e t h e rf o re a c hk 芝5 t h e r ei sa nu n s a t i s f i a b l ef o r m u l ai nl c n f 出 b a s e do nt h es t r u c t u r ea n dp r o p e r t yo fl i n e a rf o r m u l a s ，w ep r e s e n taa l g o r i t h m w h i c hr e d u c eaf o r m u l aft oal i n e a rf o r m u l af 抽i np o l y n o m i a lt i m eo fl f i f i ss a t i s f i a b l ei fa n do n l yi ff 砌i ss a t i s f i a b l e f u r t h e r ，w ep r e s e n tas i m p l ea n d g e n e r a lm e t h o dt oc o n s t r u c tu n s a t i s f i a b l ef o r m u l a si nk - l c n f ，w h i c hf o r m u l a s h a v ee v e r yc l a u s e so fl e n g t hk ，f o re a c hk 苫3b yt h ea p p l i c a t i o no 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 st or e d u c t i o n sf o rf o r m u l a s w es h o wf o re a c hk 乏3t h a tt h e r e e x i s t sa l lm i n i m a lu n s a t i s f i a b l ef o r m u l ai nk - l c n f t h e r e f o r e ，t h es t r o n g e rr e s u l ti s s h o w n ，w h i c hk - l s a ti sn p - c o m p l e t ef o rk 乏3 k e y w o r d s ：l i n e a rf o r m u l a s a t i s f i a b i l i t yn p c o m p l e t e n e s s m i n i m a lu n s a t i s f i a b l ef o r m u l ar e d u c t i o n a l g o r i t h m 4 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究所取得的成果。除文中已经注明引用的内容外，本 论文不包含任何其他个人或集体已经发表或撰写过的科研成果。 对本文的研究在做出重要贡献的个人和集体，均已在文中以明确 方式标明。本人完全意识到本声明的法律责任由本人承担。 论文作者签名：蕉盛搓 日 期： 2 qq g 生垒月 关于学位论文使用授权的声明 本人完全了解贵州大学有关保留、使用学位论文的规定，同 意学校保留或向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅；本人授权贵州大学可以将本学位论 文的全部或部分内容编入有关数据库进行检索，可以采用影印、 缩印或其他复制手段保存论文和汇编本学位论文。 ( 保密论文在解密后应遵守此规定) 论文作者签名：耋篮蓝导师签名：日期：至q q g生f l 旦 第一章前言 1 1 研究背景 可满足性问题( s a t i s f i a b i l i t yp r o b l e m ，简称s a t ) 是计算机科学的中心问题 之一，也是第一个被证明的脚一完全问题，并且是一大类卿一完全问题的核心。 s a t 问题是指可满足布尔表达式的集合，它在数理逻辑、人工智能、约束可满足 性问题、v l s i 集成电路设计与检测、计算机科学理论、计算机视觉、机器定理 证明、机器人规划、机器学习等领域具有广阔的应用背景。 对于一个c n f 公式。给定该公式中的所有命题变元的真假赋值后，就可以 判断这个公式在该赋值上是否满足。1 若存在一个赋值使该公式满足，则称该公式 可满足；若不存在赋值使该公式满足，则称该公式不可满足。 若一个a 防公式f 是不可满足，并且在f 中删去任意一个子句后所得到的 公式是可满足的，则称f 为极小不可满足的( m u ) ( 9 c h p a p a d i m i t r i o u ，d w o l f e ，1 9 8 8 ) 。已经证明：如果d 仃) s0 则f 不是极小不可满足的( 1 3 ，2 8 g d a v y d o ve t c ，1 9 9 8 ；r a h a r o n i ，1 9 9 6 ) 。因此，我们可以记m u ( k ) 为公式差为 k ( k 苫1 ) 的极小不可满足公式集。一个公式是否属于m u ) 能在多项式时间内判 定( 1 4 h f l e i s c h n e re t c ，2 0 0 2 ) 。若语言b 属于艘，且n p 中的每个a 都多项式 时间可归约到丑，则称语言b 为p 一完全的( 2 5 m s i p s e r , 2 0 0 5 ) 。判断一个c n f 公式是否为一个极小不可满足公式问题是d p 一完全的，其中d p 是被描述成两个 p 问题的差的一些问题的集合( 9 c h p a p a d i m i t r i o u ，d w o l f e ，1 9 8 8 ) 。 在文献( 9 c h p a p a d i m i t r i o u ，d w b l f e ，1 9 8 8 ) 中，c h p a p a d i m i t r i o u 和 d w o l f e 证明了对任意一个公式f ，可以在多项式时间内构造出另一个公式厂( f ) 满足： f 可满足，当且仅当，泸) 可满足； f 不可满足，当且仅当，( f ) 极小不可满足。 也就是说，一个不可满足公式在多项式时间内可以转化为一个极小不可满足 公式。所以通过极小不可满足公式来研究不可满足公式就显得非常有意义。极小 不可满足公式的研究是近年来兴起的问题的一个热点方向。德国学者h k l e i n e 5 b r i n i n g ，0 k u l l m a n n 等人在这方面做了许多重要的工作。极小不可满足公式的一 些结构和性质将有助于判定s a t 算法的研究。我们对极小不可满足公式集感兴趣 主要基于两方面的原因：一是大多数的消解难例公式都是极小不可满足的：二是 对于极小不可满足公式的深入理解，有助于我们构造新的难例公式以及新的满足 性算法。在我们所知道的消解难例中几乎都是极小不可满足公式( 2 ，3 ，5 ，2 2 a a t s e r i a s ，2 0 0 0 ；a h a k e n ，1 9 8 5 ：au r q u h a r t ，1 9 8 7 ：k r i s h n a m u r t h y , 1 9 8 5 ) 。 极小不可满足公式的一些结构和性质将有助于判定s a t 算法的研究。一个 s a t 算法是指能在有限的时间内，判定任意给定的c n f 形式的命题公式是否是 可满足的。对c n f 公式的深入研究，能够使很多公式得到简化，从而节约计算 机计算时间。 1 2 研究意义 本文给出了线性化算法和线性公式的判定算法，线性化算法可以在多项式时 间内把任一公式转化为线性公式，且两者有相同的可满足性。线性公式的判定算 法可以在多项式时间内判定一个公式是否为线性公式。使用算法的思想有助于构 造其它的线性公式。 由m u 公式在公式归约中的应用以及归纳法，我们得到在k l c n f ( k 苫3 ) 公 式中构造线性m u 公式的一般化的方法，从而证明了对每一个正整数k 3 ， 七一l c n f 包含m u 公式。这个结论强于开问题“在l c n f ：a 公式中是否存在不可 满足公式( 3 1 ，3 2 s p o r s c h e n ，e s p e c k e n m e y e r , 2 0 0 6 ) 。由k l c n f ( k 芑3 ) 公式 中存在m u 公式这一事实，我们证明了判定问题k l s a 丁( k 3 ) 是p 一完全的。 1 3 研究的主要内容 在本文中，我们主要从两个方面进行研究，一是对线性公式的结构与特点进 行研究，二是对线性公式的可满足性判定问题进行研究。 如果一个c n f 公式f 中的任意两个不同子句最多包含一个公共变元，则称 公式f 为线性的。如果一个c n f 公式f 的任意两个不同子句恰好包含一个公共 6 变元，则称公式f 为严格线性的。记l c n f 和x l c n f 分别表示线性公式类和严 格线性公式类。定义七一c n f ：= fe c n fiv c f ，i c i = 七) ，l c n f ：_ 妒a 盯if 是线性的) ，x l c n f ：= f e c n fif 是严格线性的) ，l c n f 吐妒l a 盯iv c e f ，l c l 七) ，k - l c n f ：= f l c n fi v c f ，i c l - - k 。对应地，各子类的可满足 性判定问题分别记为k s a t ，l 阴丁，x l s a t ，l 翻i 和k l 阴r 。 对线性公式的研究，我主要从线性化算法和线性公式的判定复杂性两个方面 进行研究。在文中给出了线性化算法和线性公式的判定算法，线性化算法可以在 多项式时间内把任一公式转化为线性公式，且两者有相同的可满足性。线性公式 的判定算法可以在多项式时间内判定一个公式是否为线性公式。 已经证明每个严格线性公式是可满足的( 3 3 s p o r s c h e ne t c ，2 0 0 6 ) ，l s a t 问题是p 一完全的( 3 l ，3 2 ，3 3 s p o r s c h e n ，e s p e c k e n m e y e r , 2 0 0 6 ：s p o r s c h e n e t c ，2 0 0 6 ) 。对于l c n f 的子类l c n f ：t ，如果在l c n f ：t 中存在不可满足公式，则 l s a l t 仍然是p 一完全的( 3 1 ，3 2 ，3 3 3s p o r s c h e n ，e s p e c k e n m e y e r ，2 0 0 6 ：s p o r s c h e ne t c 。，2 0 0 6 ) 。所以，当k 3 时，鲥毛是否是艘一完全问题归结为在 l c n f , 中是否存在不可满足公式。在( 3 1 ，3 2 3s p o r s c h e n ，e s p e c k e n m e y e r , 2 0 0 6 ) 中，通过构造超图和拉丁方阵，分别构造出了l c n f ：，和l c n f ：。中的不可满 足公式。然而，这种方法过于复杂并且不具一般性。在( 3 2 s p o r s c h e n ，e s p e c k e n m e y e r ，2 0 0 6 ) 中，提出了一个公开问题：当k 苫5 时，在l c n f t 中是否存 在不可满足公式。 对线性公式的可满足性判定问题的研究，我主要从以下两个方面进行研究， 一是对不可满足公式存在性的研究，二是对线性公式可满足性问题的判定复杂性 的研究。 在将c n f 转变成3 一c n f 方法中，我们发现了一个与极小不可满足公式相联 系的基本规律，对一个子句c = ( 厶v vl ，) 3 ) ，转换方法是首先引入。一3 ) 个新变量y ，y ：，y p 一，然后将c 分裂成块缇，l ：】，地 ，以：】， 0 二，0 】，进而 7 构造 一2 ) 个子句( v 厶vy 。) ，心v mvy ：) ，心一：v - , y ，一。vy p - a ) ，口p 一。v v 叫p 一。) 。在这里，公式跌，( 强vy 2 ) ，( 叫州vy p - 3 ) ，- , y p - 3 】实际上是删( 1 ) 公式，而且c 的分割化，l ：】，他】- ，但p - 2 ) ， 己p _ 1 ，三p 对应于一个a 伊公式【( v 上：) ，如，l p 掣( v 0 ) 】。因此3 一c n f 公式【心v 厶vm ) ，( 匕v 啊vy ：) ，心一：v y 尹一vy p - 3 ) ，( 0 。v y - y v 。) 】可看成是【( vl 2 ) ，厶，0 巾4 p d vl p ) 】与【m ，( 叫，vy 2 ) ，( 一y 口一。vy l , - 3 ) ，一y p - 3 】分别在对应位置上的子旬析取。另外，单元子 句对应于公式【vy vz ) ，vy v ，2 ) ，犯v - ，) ，vz ) ，犯v - - , yv ，z ) 】，这里 【( yvz ) ，( yv ，z ) ，( ，yv z ) ，( ，yv z ) 】为m u ( 2 ) 公式，子句( 厶v 厶) 对应公式 【( 厶vl ：vy ) ，( 厶vl 2v - , y ) 】，这里【y ，一，y 卜ya ，y 为m u ( 1 ) 公式。基于这一基本 规律的发现以及极小不可满足公式的特点，我们通过构造适当的极小不可满足公 式，可将任一个c n f 公式转化为其它类型的公式。实际上我们已经将这一方法 应用于公式的归约上。在( 2 1 j w a n g ，d x u ，2 0 0 5 ) 中，我们给出了解决( 3 0 r i m p a g i l a z z o ，r p a t u r i ，1 9 9 9 ) 中一个公开问题的算法：对固定的k 和t ( 3st ； 州，。 三如酱； 似忡$ 如果“导“跏l ； ( i v h 舢叫三 ( v ) f ( a - - * b ) 咋 ( v i h ( a 删埠 定理2 1 1 如果f ( a i ) 一域f ( b ) - 1 否则 如果r ( a ) = 0 或r ( b ) 一1 否则 对一个真假赋值4 有唯一的真假值，使得v ( a ) = 4 ( 口) ，其中口为命题公式 中的任一文字。 一个可满足公式是指有真假赋值后，得到的结果是t 。 定义2 1 - 4 ( 永真公式或重言式) 一个命题公式驴称作是有效的，如果对于任何真假赋值r 都有z 如) = 1 。满 足这样性质的命题公式称作永真公式，也叫重言式。 例如：公式( pv 叩) 是重言式，因为对任意赋值f ，无论可( p ) = 1 还是 z p ) 一0 ，都有f 0v - , p ) 一1 。 定义2 1 5 ( 永假公式或不可满足公式) 命题公式9 是不可满足的，如果对于任意真假赋值f ，都有z ) - 0 。 例如：公式0a - p ) 是不可满足公式，因为对任意赋值f ，无论f o ) ；1 还是 z o ) = 0 ，都有f oa - , p ) 一0 。 br l u矾 r 果 定义2 1 6 ( 可满足性公式) 命题公式驴是可满足的，如果存在某个真假赋值f ，有z ( 驴) 一1 。 定义2 1 7 ( 文字和子句) 原子公式或其否定称为文字o i t e r a l ) 。原子公式本身称为正文字，原子公式的 否定称为负文字。若干个文字的析取构成子句( c l a u s e ) ，其长度是指所含文字的 个数。只有个文字的子旬称为单子句( u n i tc l a u s e ) 。没有文字的子句称为空子句 ( e m p t yc l a u s e ) ，记为口。 一般说来，子句中的文字越多，该子句就越容易被满足。举一个简单的例子， 单子句p 只有在p 为真时才被满足，而对于子句pvq ，不仅在p 为真时被满足， 而且在口为真时也被满足。所以，文字越少的子旬越难满足。一个极端的情形是， 空子旬不可满足。 注：空公式( 中) 可满足。 定义2 1 8 ( 合取范式和析取范式) 若干个子句的合取是一种特殊形式的公式，称为合取范式( c o n j u n c t i v en o r m a l f o r m ) ，简写为c n f ，其一般形式为心，v vk 。) ( k ，v vk 。) 。这里 的每个是文字。一个公式被称为析取范式( d i s j u n c t i v en o r m a lf o r m ) ，简写为 d n f ，如果他的形式为v v 。这里每个仍是若干个文字的合取。 在本文中，所有的公式都是指c n f 公式。 定理2 1 2 对任意公式，都有与之等值的合取范式和析取范式。 一个文字是一个命题变元或命题变元的否定。一个子句c 是文字的析取范式 ( c = ( 厶v v 厶) ) ，有时将子旬c 表示成一个文字集合仁一忆，”。一个合 取范式( c n f ) f 是子句的合取( f = ( c 1a e ) ) ，有时将f 表示成一个子旬 集合p 一 c 1 ，e ”或一个子旬序列= c 1 e d 。p a ，忙) 表示出现在公式 f 中的变元集合，所仁) 表示变元集合阳，忙) 上的文字集合。孝阳，陋) 、j 5 6 c z p ) 分 别表示出现在公式f 中的变元个数和子句个数，p o s ( x ，f ) 、，l 昭g ，f ) 分别表示 1 变元x 在公式f 中正出现、负出现的次数。- 记o c c ( x ，f ) 一0 b ，f ) ，l 昭g ，) ) 和 o c c s ( x ，f ) = p o s ( x ，f ) + n e g ( x ，f ) 。对刀，1 ，c n p ( n ，r ) 表示含有以个变元和 r 个子句的c 脬公式的集合。通常，记公式类f ) = u 柑c n f ( n ，以+ 七) ，整数七称 为公式差。定义f 的尺寸为i f i = 埘。l e i ，其中i e i 表示子句c 中包含的文字个 f 是a 旧公式，l 是一个不在f 中出现的文字，定义lv df 一 犯v 厂) i 设f 是一个含有文字l 的公式，则公式冗叫有如下定义。 如果f 包含单子句，则气。】2 中( 空公式) ；否则气i l 】是由下面方法得到 的公式： 公式q 工- o 】有类似定义。 设，一 c 1 ，c 。) 是带有想个变元而，毛，m 个子句的公式。如下定义的 n x m 矩阵m ，= ( q ，j ) 称为f 的表示矩阵，其中 f + 鼍c ， 口u 。 _ ，鼍c ， ( 有时用空白表示o ) 。 l o 0 葺，一t 岳c j ( 1 ) ( 改名) 设日和f 都是c n f 公式，则一个映射妒：t i t ( h ) _ t i t ( f ) 被称为 一个从h 到f 的改名，当且仅当对所有l l i t ( h ) ，有伊( 乙) 仁，l 】- 和 映射妒：v a r ( h ) 一v a r ( f ) 被称为一个从到f 的变元改名，当且仅当垆是一个满 足驴( 日) = f 的置换。 ( 3 ) ( 文字改名) 设日和f 都 c n f 公式，则一个映射伊：l i t ( h ) 一l i t ( f ) 被 称为一个从日到f 的文字改名，当且仅当伊是一个l i t ( h ) 上的置换，且对所有 l l i t ( h ) ，有垆( 一，工) 一一驴仁) ，其中符号一表示逻辑等价。 注意：一个文字改名是变元改名和改名的复合。 子句( - , p 1v v - , p 。vq 1v vq m ) 等价于( p 1a ap 。) 一( q 1v vq 。) 。 采用这种形式表示子旬c 时，若万一0 ，则称c 为正子句；若m = 0 ，则称c 为 负子句；若m 和，z 都是正整数，则称c 为混合子旬。当ms 1 时，称c 为h o r n 子句，否则称为非h o r n 子句。例如：( pv - , qv ，) 和( 叩v ，g ) 都是h o r n 子旬。 2 2d p l l ，异法 d p l l 算法是d a v i s 和p u t n a m 提出的方法，l o g e m a n n 和l o v e l a n d 对它作 了进一步的描述。d p l l 算法是求解可满足性( s a t ) 问题的一个重要算法，有关 d p l l 算法的详细描述，请参阅文献( 1 ，1 0 ，1 1 张健，2 0 0 0 ；d a v i sm e t c ，1 9 6 2 ； d a v i sm ，p u t n a mh ，1 9 6 0 ) 。 如果一个子句含有一对互补文字，称该子句为重言子句。在一个公式中删去 重言子旬后，不影响公式的可满足性。一个变元x 在一个公式f 中的正( 或负) 出现，指文字石( 或文字一x ) 在f 中出现。 下面我们叙述一下d p l l 算法： 设f 是一个公式，在d p l i ，算法中，应用了如下的4 条规则对问题进行简化 或分解： 1 重言式规则 删去当前公式f 中的重言子句。 2 单子旬规则 假设当前公式，含有一个单子句仁】( 子句中只包含一个文字) ，对于变量x ， 1 4 如果 x ) 和 一x ) 均出现，则公式f 不可满足；否则删去所有包含文字l 的子句( 不 仅仅删去单子句 l 】) ，然后从剩下的含有文字一l 的子句中删去文字，l 。 3 纯文字规则 如果一个文字l 出现在当前公式f 的某些子句中，并且文字，l 不出现在f 的其它任何子句中，则将所有包含文字l 的子旬删去。 4 分裂规则 如果当前公式f 具有形式：f 一【 v 五) ， v 厶) ，( - xv9 1 ) ，( 一xvg 。) ， 啊，啊】，其中子句五，厶，9 1 一，g 。，1 1 1 ，鸭不含x ，x 。则将验证f 的可满足 性问题分裂为两个子问题：验证五枷1 暑【 ，厶，啊，】和f t 柚】- g l ，一，g 。，嚏， ，】的可满足性。如果其中之一可满足，则f 可满足；否则f 不可满足。 假设公式f 应用上述4 条规则中的任意规则后所得到的公式为f ，则公式 f 和f 。有相同的可满足性。一 下面的例子能够帮助读者更好地理解d p l l 算法。 例2 2 1 设公式f ； 扛，z ，缸，y ，z ，w 】，缸，y ，z 】，缸，一y ，z ，缸，- , y ，一z ，w ， 一z ，y 】， 一工 ， o ，z 】i ， ，y ，z 】，我们使用d p l l 算法验证公式f 的可满足性。由纯文字规则， ：丈- t w 出现在公式f 的某些子句中，并且文字一w 不出现在f 的其它任何子句 中，将所有包含文字w 的子句删去，我们得到公式f ； 缸，y ，一z ) ，缸，一y ，z ) ， 一x ， y 】- ， x 】- ，z ) ， ，y ，一z 】- 。由单子句规则，公式f 中含有单子句一x ，删去一x 和 包含，x 的子旬，并在其它含有文字x 的子旬中删去x ，我们得到公式 f 。= “y ，一z ) ， 一y ，z ) ，o ，z ) ， 一y ，一z 】) 。由分裂规则，我们得到曩；叫= z 】- ， 一z 】 和 墨：，- 0 】- l ，z ) ，仁) ) ，易知，瓦_ 1 l 和墨；，- 0 】均不可满足，所以公式f 不可满足。 容易证明：在使用d p l l 算法对一个公式的可满足性验证中，如果只使用到 重言式规则、单位子句规则、纯文字规则，则这类公式的可满足性验证可以在多 项式时间内完成。然而，一般情况下，在使用d p l l 算法的过程中，不可避免地 1 5 要使用到分裂规则。因此，分裂规则是d p l l 算法的核心部分。分裂规则的使用， 产生了两个分支问题，而其它规则的使用只产生一个简化问题。这样，我们可以 用一棵二叉树直观地表示d p l l 算法的规则使用过程。这样的树称为d p l l 算法 的分裂树，简称分裂树。分裂树的根结点用初始公式f 标记，一次规则的使用产 生一个或两个子结点，新的予结点用相应的新公式进行标记。分裂树的叶结点用 空公式或空子句标记。如果所有叶结点均被空子旬( 口) 所标记，则原始公式f 不可满足；否则，f 可满足。 在应用d p l l 算法的过程中，分裂树的结点数是验证过程的计算复杂性的一 种度量形式。d p l l 算法的各种改进策略就是引入新的规则( 或规则组合) 降低 分裂树的结点数。在文( 1 张健，2 0 0 0 ) 中，作者对d p l l 算法的一些著名的改进 策略作了一个很好的总结。 下面介绍一种改进的d p l l 算法，称为r s l m s 算法( r e s o l u t i o n s u b f o r m u l a l i t e r a lr e n a m i n g - m u l t i p l e - s p l i t t i n g ) ，此算法是基于h k l e i n eb r i n i n g 和赵希顺在 文( 3 0 r 1 m p a g i l a z z o ，r p a t u r i ，1 9 9 9 ) 的思想设计的。r s l m s 算法仅限于使用在 不可满足公式的反驳证明中。在此算法中，消解规则指n 球) 一消解、子公式规则 指在一个不可满足公式中取一个不可满足的子公式、对称规则为文字改名规则、 重复规则指相同公式取其中之一、分裂规则为d p l l 算法中的分裂规则。与 d p l l 算法类似，仍然用树的形式描述规则的使用过程，所产生的树仍然称为分 裂树。在分裂树上，仍然用一个公式标记一个结点。在树的叶结点上，允许用空 子句( 口) 作标记。 在r s l m s 算法中，使用下列规则： 1 初始化规则( i n i t i a t i n g ) 分裂树的树根用初始公式瓦标记。 2 g 半) 一消解规则( g 术) 一r e s o l u t i o n ) 假设v 为当前分裂树上的一个叶结点，所带标记公式为 f 一【v 厂) ，( 一三vg 。) ，( ，lvg p ) ，】，其中，蹦不包含文字l 和，l 。则由v 产 生一个孩子结点心，并用公式【( 厂vg 。) ，( 厂vg e ) ，】标记屹。( 请注意：单子 句消解规则是q 木) 一消解规则的特殊情形。) 1 6 3 子公式规则( s u b f o r m u l a ) 假设y 为当前分裂树上的一个叶结点，所带标记公式为f 。如果e 是f 的一 个子公式，则由，产4 ：- - 个孩子结点k ，并用公式只标记k 。( 请注意：使用该 规则时，只是不可满足公式。) 4 文字改名规则( l i t e r a lr e n a m i n g ) 假设v 为当前分裂树上的一个叶结点，所带标记公式为f 。设妒是公式f 的 一个文字改名，使得妒( f ) = 只，则由，产生一个孩子结点心，并用公式c 标记屹。 5 重复规则( m u l t i p l e ) 假设y 为当前分裂树上的一个叶结点，所带标记公式为f 。如果在当前分裂 树上有另一个结点，被f 所标记，则由v 产生一个孩子结点e ，并用空子句口标 记k 。 6 分裂规则( s p l i t t i n g ) 假设v 为当前分裂树上的一个叶结点，所带标记公式为f 。如果文字在f 中既有正出现、又有负出现，则由v 产生两个孩子结点屹、匕，并分别用公式 下犯一1 ) 标- i 已v , 、用公式f 仁一0 ) 标记咋，其中，仁；1 ) ( f 犯= o ) ) 是在公式f 中 令一1 犯= 0 ) 代入公式化简后所得到的公式。 7 结束规则 如果当前分裂树的所有叶结点已经被空子句口所标记，则结束计算，并返回 “秀盾 o 一个公式f 不可满足，。当且仅当存在一个基于r s l m s 算法的返回“矛盾 的反驳证明。在r s l m s 算法中，子公式规则涵盖了d p l l 算法中的重言式规则。 2 3 消解 在这部分，我们将给出一些关于消解原理的基本知识、极小不可满足公式的 简单事实以及几个重要的定理和引理。 1 7 目前影响最大、应用最广的推导规则是j a r o b i n s o n ( 2 9 r a h a r o n i ，n l i n i a l ，1 9 8 6 ) 提出的“消解”( r e s o l u t i o n ，也被译成“归结”) 及其改进。命题逻 辑中的消解方法，可以说是d p l l 算法中单子旬规则的推广。其消解原理 ( r e s o l u t i o np r i n c i p l e ) 如下： 假设有两个子旬c ，和c ：，其中分别含文字工。和：，并且这两个文字互补。 分别将工，和l ：从c 。和c ：中删掉，再将两个子句中的其余文字合并，所得到的新 子旬c 称为c l 和c 2 的消解式( r e s o l v e n t ) 。c 1 和c 2 是c 的父子旬。对任意两个 子句，它们的消解式必是其逻辑推论。 例如：子句pvq 和- - , pv ，vs 的消解式为qvrvs 。子句pvq 和pv 一，没 有消解式，因为它们中没有互补的文字。 定义2 3 1 ( q 宰) 一消解) ( 1 3 g d a v y d o ve t c ，1 9 9 8 ) 设公式f - 【犯v 厂) ，( ，工v9 1 ) ，( ，上vg p ) ，如，】是一个c n f 公式，其中 不包含l 和，l 。则公式f = 【( ，v9 1 ) ，( 厂vg p ) ，】称为公式f 关于文字的 一个仉木) 一消解。 特别地，当p - 1 时，称公式f 一【( 厂v9 1 ) ，】为f 关于文字l 的一个q 1 ) 一 消解。我们知道：每个不可满足公式f ，均可以通过有限次消解产生一个空子句。 请注意：消解产生空子句的过程中，可能只用到f 中的部分子句，也可能f 中 的部分子句被重复使用。有关图论的术语和记号请参阅文献( 7 b o n d yj 八 m u r t yu s r ，1 9 9 6 ) 。一棵规则二叉树t 一( v ，e ) 是指树中每个枝结点恰好有两个孩 子结点。由于每次消解只取两个子句，所以消解产生空子句的过程可以联系到一 棵规则二叉树。在此二叉树上，叶结点用f 中的子句标记，每个枝结点用其两个 孩子结点所标记的子句的消解子句进行标记。对应的两条边上用相应的消解变元 所对应的一对互补文字分别标记。最后，根结点用空子句标记。由此产生的标记 树称为公式f 的一棵消解树。请注意：一个不可满足公式的消解树不一定唯一。 由消解树形成公式的一个形式化证明称为树消解证明。消解树的结点数是消解复 杂性的一种度量形式。 定义2 3 2 ( 树消解证明) ( 3 6 x ud a o y u n ，2 0 0 5 ) 假设f 是一个不可满足公式，丁是一棵规则二叉树，结点标记函数丸，将每 1 8 个结点v v ( r ) 映射到一个子句，边标记函数丸将每条边e e e 仃) 映射到一个文 字。我们称四元组r = 仃，砧，九，f ) 为公式f 的树消解证明，其中： ( 1 ) 九( v o ) = 口( 空子句) “是丁的根结点) ； ( 2 ) 九o ) f p 是z 的叶结点) ； ( 3 ) 对于丁的枝结点y 及其左孩子和右孩子u ，九( y ) 是九( b ) 和九，o ，) 关 于某个变元x 的消解子句。而且，如果x 砧“) ，则气，v 1 ) 1 ez 且k ，1 ，) 一，x ； 如果- - , x 九“) ，则k ，) 一一工且九，y ，) = x 。 例2 3 1 公式f t r y 。vy 1 ) ，( 一，y 4v - , y ：) ，( y ：vy a ) ，( y 。vy s ) ( 一) ，。v - , y 。) ( ) ，。vy 7 ) ，( ，y 5 v y ，) ，( 一y ，v - , y ，) 】删( 1 ) 。公式f 的表示矩阵为： ) ，4 y 2 y l y 3 y 6 y 5 y 7 下面是公式f 树消解证明： y 图( 1 ) 1 9 g y 7 2 4m u 公式 定义2 4 1 ( 极小不可满足公式) ( 3 7 x ud a o y u n , 2 0 0 2 ) 一个c n f 公式f 是极小不可满足公式( 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 ) ，简记 为m u 公式，如果：( 1 ) f 是不可满足的；( 2 ) 对于任一子句，e f ，都有公式 f 一 厂) 是可满足的。 也就是说，一个c n f 公式f 是极小不可满足的，当且仅当这个公式是不可 满足的，且删去任意一个子句后产生的公式是可满足的。 定义2 4 2 ( p 一完全) 如果语言8 属于p ，且艘中的每个a 都多项式时间可归约到口，则称语 言艿为n p 一完全的。 判断一个c n f 公式是否为一个极小不可满足公式的问题是d l 完全的，其中 d p 是所有可以描述成两个p 问题的差的问题类，即d p - ai 存在b e n p 及c c o n p 使得a = bn c 。 下面的定理说明了关于极小不可满足公式的子句个数