（计算机应用技术专业论文）nthit公式的存在性.pdf

摘要 可满足性问题( s a t 问题) 在数理逻辑，人工智能、机器学习、约束满足问题、脚 集成电路设计与检测以及计算机科学理论等领域具有广阔的应用背景。可满足性问题是第一 个p 一完全问题，并且是一大类n p 一完全问题的核心大量的实践表明，许多p 一完 全向题无论对于计算机科学理论还是工程应用都有着至关重要得意义。 极小不可满足公式的研究是近年来兴起的关于可满足性问题的一个热点方向。一个 c n f 公式f 称为极小不可满足的( 删) ，如果f 是不可满足，并且在f 中删去任意一个 子句后所得到的公式是可满足的。分裂技术是研究极小不可满足公式的很好工具。取出一变 元z ，我们对他进行真假赋值x 一0 和善- 1 ，从而来考察赋值后得到的新的公式对极小 不可满足公式的一个变元赋值后，得到的公式仍是极小不可满足公式。特别地，可以使用分 裂技术对公式归纳证明并对公式进行分类。 一对子句c 1 和c 2h i t t i n g 的，如果c 1 和c 2 中存在一对互补文字，即存在文字三使 得l c l 且一c j 一个c n f 公式f 中的任意两个不同的子旬中恰有一对互补文字，我 们称，为非重言h i t t i n g 公式( n o n - t a u t o l o g i c a lh i t t i n g ) 我们用r h t 表示非重言的 h i t t i n g 公式类。 在【1 3 】中，h a n sk l e i n eb o n i n g 和赵希顺利用分裂技术研究了m u 予类k 的核k ，得 出了k ：在分裂下是封闭的结论。他们证明了胛一日玎一肘u ) 一0 毒2 ) 和 m a x 一h i t m u 。同时，留下两个公开问题： ( 1 ) 对于任意f r h t ( 1 ) 是否存在一个文字，l 在f 中仅出现一次? ( 2 ) 对于后七2 ，r - 本文根据r h t 所满足的条件，以公式的变元数栉和子句数m 为参数，构造了命 题公式以。证明了： ( 1 ) 日。可满足当且仅当存在一个含有n 个变元和1 1 1 个子句的r 一只玎公式 ( 2 ) 对于n t 一尼盯( 1 ) 中的任意一个公式f ，存在文字己，在f 中仅出现一次 ( 3 ) 对于七2 ，公式峨。“是一个不可满足公式 ( 4 ) 对- t - k 2 ，r 一月盯 ) 是一个空集 r 一册z 是一类重要的命题公式只公式的构造不仅解决了长期困扰理论计算界 的两个公开问题，而且从一个全新的角度、直观地诠释了n t h i t 公式类的结构与性质并 完成了对其分类。， 关键词：s a t ：不可满足公式；n p 一完全问题 中图分类号： l a b s t r a c t n es a t i s f i a b l e ( s a t ) p r o b l e m p l a y s a l l i m p o r t a n t r o l ei na r t i f i c i a l i n t e l l i g e n c e , m a c h i n el e a r n i n g , m a t h e m a t i c a ll o g i c , v l s id e s i g na n dd e t e c t i o no t h e r a r e a s i tl i e sa tt h ee v e r yh e a r to faf a m i l yo fn p - c o m p l e t ep r o b l e m s ，a n di s i m p o r t a n tt ob o t hc o m p u t e rs c i e n c ea n dp r a c t i c a la p p l i c a t i o n s r e s e a r c ho nt h em 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 c0 1 1s a tp r o b l e m t h a tb e g i n st os u r f a c ei nr e c e n ty e a r s a f 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 f fi 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 a p o w e r f u lf o ri n v e s t i g a t i n gt h e s t r u c t u r eo fm i n i m a lu n s a t i s f i a b l ef o r m u l a si s s p l i t t i n g w et a k ea v a r i a b l ex 。a s s i g nt r u t hx - 0a n d 并- 1 ，a n dc o n s i d e rt h e r e s u l t i n gf o r m u l a s f o ram i n i m a l u n s a f i s f i a b l et h er e s u l tf o r m u l a sc o n t a i nm 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 s i np a r t i c u l a r , b a s e do ns u c has p l i t t i n gi n d u c t i o np r o o f sc a i l b ep e r f o r m e da n dc h a r a c t e r i z a t i o nf o rs o m es o m ec l a s s e so ff o r m u l a sc a nb e e s t a b l i s h e d h 1 【1 3 】，h a n s k l e i n eb u n i n go b t a i n st h er e s u l tt h a tk i sc l o s e du n d e r s p l i t t i n g , a n dl e a v e st w oo p e np r o b l e m s ：( 1 ) f o ra n yf o r m u l afe n t h i t ( 1 ) ，i f t h e r ee x i s t sal i t e r a l 工o c c u r r i n ge x a c t l yo n c ei nf ( 2 ) f o ra n yk 苫2 ，i ft h es e t n t h i t ( 0i sa l le m p t ys c l b a s e do nt h ec o n d i t i o n so fn t m tf o r m u l a , w ec o f l s t m c tf o r m u l ah h 矗s u c ht h a t h i i ss a t i s f i a b l ei fa n do n l yi ft h e r ee x i s t san t h l tf o r m u l aw i t hn v a r i a b l e sa n d mc l a u s e s b yt h ep r o p e r t i e so fh m ，w ep r o v et h a tf o ra n yf e n t h r i qt h e r e e x i s t sal i t e r a l 工o c c u r r i n ge x a c t l yo n c ei nf ，a n ds h o wt h a tf 7 一解 ) i sa l l e m p t ys e tf o rk 2 t h u sw es o l v ep o s i t i v e l yt w oo p e np r o b l e m s n t h 珏i sa l li m p o r t a n tc l a s so fp r o p o s i t i o n a lf o r m u l a t h ec o n s t r u c t i o no fh t m f o r m u l an o to n l ys o l v ep o s i t i v e l yt w oo p e np r o b l e m st h a th a v eb e e np u z z l e dt h ec o m p u t e r s c i e n t i s t sf o r 钮l o n gt i m e , b u ta l s oe s t a b l i s ht h ec h a r a c t e r i z a t i o na n ds t r u c t u r eo fn t h i t c o m p l e t e l y k e yw o r d s ：s a t ；u n s a t i s f i a b l ep r o b l e m ；c o m p l e t e - p r o b l e m 2 第一章引言 命题逻辑是最简单的逻辑系统，其研究对象为只考虑取“真”、“假”值的命题。由简单 命题出发，经过使用逻辑联结词以构成复合命题。尽管命题逻辑是最简单的逻辑系统。然而， 计算机科学和数学优化中的许多重要研究分支和著名问题却源于命题逻辑。 命题公式的有关定义如下： 定义1 ( 命题公式) 【1 】 ( 1 ) 命题符号是命题公式 。 ( 2 ) 如果口和卢是命题公式，那么( 口 声) ，( 口v 卢) ，( 一口) ，( 口一卢) 和 一) 也是命题公式。 ( 3 ) 一串符号是命题公式当且仅当它可以由( 1 ) 和( 2 ) 得到 例如，0 v 曰) ，c ，( 似a 功一c ) ，( 一以一b ) 一c ) 都是命题公式，而 a 一，0 v b ，( - - - , a ) 却不是命题公式定义1 中的( 3 ) 很重要，它告诉我们怎样依原 子公式作为基使用连接符号归纳得到命题公式i 命题逻辑是公式的语言。每个公式都有它一定的意义( 也就是真值) 一f 或者，它的值 是由命题符号所包含的内容决定的。命题公式的值可以通过真值表计算得到。 定义2 ( 真假赋值) 【1 】 真值指派a 是一个函数，它给命题中的字母a 赋以唯一的一个值，a ( a ) f ， 。 定义3 ( 公式的真假值) 【1 】真假赋值 ，给公式指派的真假值递归地定义如下： ( i ) ，( 口) f ，) ( i i ) 小咖侈嚣认彩可 。讧，y c 口 卢，一f 罢暑y a = 且，芦= ( m ) 0 等琦或者“印哥 ( v ) ， 叫一再骗认彩棚轧印k 。 c 帅似_ 胁b 骗讹k “p 可 定理l 对一个真假赋值a 有唯一的真假值1 ，使得以a ) 一a ( 口) ，其中口为命题公式中的任一字 母。 一个值满足公式是指真假赋值后，得到的结果是t 定义4 一个命题公式称作是有效的，如果对于任何真假赋值，都有，( 盯) - t 。满足这样性质的 命题公式称作重言式 例如： ，0v 一口) m t 无论， ) - t 还是，( 口) _ ，。 定义s ( 不可满足性公试) 命题盯是不可满足的，如果对于任意真假赋值v ，( 盯) - f 例如： ， a 一口) - f ，无论 ， ) - t 还是 ，( 口) = ， 。 定义6 ， 命题a 是可满足的，如果存在真假赋值 ，使得。，- t 可满足性问题就是判定一个布尔公式是否是可满足的它可以形式化地表示为 s f 4 丁= i 由是可满足的布尔公式l 一命题公式( 合取范式( c 伊) ) 是极小不可满足的当且仅当它是不可满足的且删去其 中的任一子旬可以得到一个可满足的公式。极小不可满足问题是d l 完全的，其中d p 是所有可 以描述成两个p 问题差的问题类。 现在p 一p 是否成立的问题是计算学科和当代数学研究中最大的悬而未决的问题之 一如果p 一p ，则所有在多项式时间内可验证的问题都将是在多项式时间内可求解或可 判定的问题。大多数人不相信尸一n p ，因为人们已经投入了大量的精力为n p 中的某些问 题寻找多项式时间算法但没有成功然而，要证明p ，n p 目前还无法做到这一点 2 5 。在p 是否等于p 问题上库克等人于2 0 世纪7 0 年代初取得了重大的进展。他们认为p 类中的某 些问题的复杂性与整个类的复杂性有关当这些问题中的任何一个存在多项式时间算法时，则 所有这些n p 问题都是多项式时间可解的这些问题被称为n p 完全性问题 7 ，8 p 完全性问 题在理论和实践两方面都具有重要的研究意义。历史上第一个p 完全性问题是库克于1 9 7 1 年提出的可满足性问题。 关于可满足性问题和n p 问题的联系，库克给出并证明了这样的定理： 5 w 丁p 当且仅当p n p 1 1 动机 有些极小不可满足公式，我们从他的某个子句中删去或添加一个文字并不破坏它的极小 4 不可满足性例如： f - ( ，4v c ) a ( 6 v av c ) a ( 一6 v 口) a - ，c 我们很容易看到，从第一个字句中删除c 或添加c 到第三个子句中得到的字句，仍是极 小不可满足公式。这就激发我们去研究极小不可满足公式的两个子类第一个是由膨【厂一公 式构成的子类- m a r g ，我们称它为边缘的。一个m u 一公式称为边缘的，如果去掉任意 文字得到的是一个非极小不可满足公式那就意味着边缘公式里没有冗余文字第二个 m u 一公式的子类是脚，我们称它为极大的。个肘u 一公式是极大的，如果增加一 个文字到任何一个子句中得到的不再是一个极小不可满足公式 分裂技术是研究极小不可满足公式的有效工具。取出一变元x ，我们对他进行真假赋值 x - 0 和x - 1 ，从而来考察赋值后得到的新的公式对极小不可满足公式的一个变元赋值 后，得到的仍是极小不可满足公式特别地，我们可以采用分裂技术进行归纳证明并且对子 类进行分类【8 】。基于上述原因，我们对在分裂下是闭的子类感兴趣。 给一个肘【厂一公式的子类k ，我们定义k k + 的任一公式都在k 中，它的任意一个 文字的分裂产生的公式都在k 中。并且，k 在分裂下是闭的。我们称k 是k 的分裂核( 简 称核) 我们将看到，边缘公式的核恰好是极小不可满足公式子类d 的核，它的任一变元称 作裂解式的分裂。这里的裂解式的分裂是指通过真假赋值得到两个独立的极小不可满足公 式我们可以根据真值赋值的组数对此公式进行另外一种描述。有这样一类肘，一公式， 从中删除任一子句后得到的可满足行性赋值是唯一的。也就是说，得到的公式是 u n i q u e 一明r 。由这些极小不可满足公式构成的集合称作u n i q u e m u 并且 u n i q u e m u 的核与边缘公式的核是相匹配的。 极大的m u 一公式是m u 一公式的一个子类，它的核具有h i t t i n g 性质。也就是说任何 两个不同的字句都包含一对互补文字大家都熟悉的一个事实是，使用h i t t i n g 公式来解决 不可满足性问题是非常有效的。我们感兴趣的是含有打个变元、n + 1 个子句，并且每一对 子句仅含有一对互补文字的非重言式h i t t i n g 公式。在这一领域有两个公开的问题：( 1 ) 对 于任意f e a r 一脚r ( 1 ) 是否存在一个文字l ，在f 中仅出现一次? ( 2 ) 对于 k 七2 ，n t 一脚r ( 七) 是否为空集? 1 2 主要工作 。 针对上述两个公开问题，我们构造了公式以得到了如下的结果： 1 日。是可满足的，当且仅当存在万个变元肌个子旬的，满足如下条件： ( 1 ) p o s ，f ) o , n e g ，) ) - 0v x e v a r ( f ) ( 2 ) f 中没有重言式子旬 5 ( 3 ) f n t h f 2 2 上么是不可满足的 3 如果f r 一且盯，则存在文字，l 在f 中出现且仅出现次。 4 对于任意露 0 ，珥。+ 2 是不可满足的 5 对于任意n ，m 0 m 一万22 ，风。是不可满足的 6 m a x q n t h i t m u q n t h i t m u a r t h i t 是一类重要的命题公式峨。公式的构造不仅解决了长期困扰理论计算界 的两个公开问题，而且从一个全新的角度、直观地诠释了r 一日盯公式类的结构与性质并 完成了对其分类 1 3 进一步的工作 极小不可满足问题m u 0 ) * am u ( 2 ) 在多项式时问内可判定在其证明中，简化过程起着 很重要的作用。简化过程是连续使用一种消解方法。我们下一步的工作就是用消解的方法来 证明峨。公式的一些结果，从而简化证明过程。 6 第二章可满足性问题 本章介绍了可满足性问题的基本定义、几种常见的可满足性问题以及可满足问题的复杂性。 2 1 基本定义 一个文字是一个命题变元或命题变元的否定一个子旬c 是文字的析取范式 ( c ( v v l ) ) ，有时将子旬c 表示成一个文字集合( c - 厶，厶) ) 一个合取范 式( c n f ) f 是子旬的合取( f - ( c la e ) ) ，有时将f 表示成- - 4 子句集合 ( f - c i ，e ) 或一个子句序列( fi 【c l ，e 】) v a r ( f ) 表示出现在公式f 中的变元 集合， f f f 旷) 表示变元集合l ，口，伊) 上的文字集合。# v a r ( f ) 、# c l ( f ) 分别表示出现在公 式f 中的变元个数和子句个数，p o s o ，f ) ，n e g ，f ) 分别表示变元x 在公式f 中出现的 正、负次数。 定义l( 公式的表示矩阵) 4 1 设f - 【c 1 ，c i 】是带有一个变元气，毛，脚个子句的公式如下定义的辟m 矩阵 m y - ，j ) 称为f 的表示矩阵，其中 例如： ( 有时用空白表示0 ) a i ，。 + x f cj 一 一x t c i 0 x i ，一x i 圣c i f 一【( 墨v 屯) ，瓴v 一工2 ) ，( 一乇v x o ，( ，一v _ ，而) 】，表示矩阵为： 五 f + + 一一1 而i + 一+ 一 g 一【( 五v 一屯v 矗) ，( 屯v 一) ，( 鼍v 一毛) ，而】 五 而 黾 x 4 +o 一+ o o +一 +o 0 o 一 + 0 o 五 或x 2 而 i + 、 一 + i 一 + i i +一j 定义2 ( 子句的析取) 墨。【五，卅】和e - 9 1 ，“，g 卅】是a ，f 公式我们称： ev 。e 一【 v9 1 ，厶v 】为互和e 的析取 定义3 ( 可满足的等价性) 【刎 公式f 和g 是可满足等价的，如果f 和g 是同时可满足的或同时不可满足的。 7 2 2 可满足性问题 k c m f 表示字句长度不大于k 的a 7 ：f 公式类可满足性问题( 简称s a t ) 就是判 定一个布尔表达式是否存在满足性赋值。命题逻辑的可满足性问题是理论计算机科学中的重 要问题。一般情况，我们考虑任意的公式，但是我们特别注意c 7 f 公式，它的每个子句都 是合取的，而字句是由正、负文字的析取构成的。对任意公式，都有与之等值的合取范式和 析取范式。通常我们假定公式已被转换为合取范式一个翩r 算法能在有限时间内，判定 任意给定的c 伊形式的命题逻辑公式是否可满足而且在可满足的情形，算法往往会给出 使字句满足的一个赋值。 判断命题公式可满足性的一个直接办法是穷举发，或者说构造出它的真值表。因为变量 的个数是有限的，而每个变量只有两种可能取值，所以这种办法从理论上讲是可行的但在 实际使用时，他显然难以应付变量比较多的公式 常见的几种鲥r 问题：、 ( 1 ) 2 翻r 问题。他要求每个子旬最多只有两个文字 ( 2 ) h o r n 子旬的可满足性问题。 、 ， ( 3 ) 任意形式的布尔表达式是否可满足? 他们不一定是合取范式或析取范式。 ( 4 ) 带量诃布尔表达式的正确性。给定一组布耳变元 岛，p 2 ，见) 以及他们构成的 布尔表达式e ，判断( q , p 3 ( q ：p ：) ( q 见) e 是否成立这里的每个q 是j ( 存在) 或者 v ( 任意) 。 ( 5 ) 唯一可满足性问题( u n i q u e s a t ) ：是否存在唯一的赋值，使得给定的子句集 合得到满足? ( 6 ) 最大可满足性问题( m a x 一翻r ) ：找出一个赋值，使得被满足的子句数达到最 大。 2 3 可满足性问题的复杂性 s a t 问题被称为难的，因为我们没有“有效的”方法来解决它。我们借助于复杂性理 论来刻划翻r 问题。 算法是解决问题的程序因此，对于可满足性问题，给了一个s a t 的例子，算法应能 判定出它是可满足的还是不可满足的。最坏情况算法复杂性就是算法在解决某一类问题操作 所需要的最大步骤数，通常用函数，和变量s 表示。我们说算法的复杂度为0 ( ，0 ) ) 在 s a t 中5 表示为出现在公式中的字句个数或变元数一个算法被认为是好的，它能在多项 时间内运行完【1 7 1 8 p 类定义为存在多项式时间算法的问题类 6 】。例如，1 - c n f 公式属于尸1 ，p 是多 项是时问可验证的问题类，也就是说，对于一个问题和它的一个特解能在多项式时间内验证 这个特解满足原问题。显然，p p 容易看出，& i r e n p 因为，给一个跗r 为题 和它的满足性赋值，很容易在多项式时间内验证出它满足每一个字句现在仍然不知道是否 s a t e p p - n p 是否成立? 这是一个具有挑战性的公开问题2 大多数科学家猜测 n p ，但缺乏根据研。 再没有介绍p 一完全性之前，先看多项式归约。p 。多项式时间可归约到p ( p 和p 表 示问题类) ，如果存在多项式时间可计算函数，：使得，对每一个有 p 尊，( 叻e p 记作p p 注意，p 至少是和一样难的，p 可看成p 的特例于是有：7 如果p s ：p 且p p ，则p 。e p p 是p 完全的，如果p p 且p 中的每个a 都多项是时间可归约到p c o o k 【2 8 】已经证明任何p 问题都可多项式时间归约到可满足性问题。因此t 跗r 是p 一 完全的。 从算法复杂度上讲，s a t 是n p 难的问题。根据计算机界的研究成果，人们通常认为， 不太可能有多项式时间的算法。但是人们后来发现，大多数随机生成的问题实例并不是那么 难解决。 9 第三章极小不可满足公式 在这章我们概括性的介绍极小不可满足公式的性质及一种重要的方法分裂技术。 3 1 基本定义 定义1 ( 极小不可满足公式) ，是c n f 公式，f 是极小不可满足的。如果： ( 1 ) f 是不可满足的 ( 2 ) 对于任一厂f ，f 一 ， 是可满足盼 简单地说，一命题公式( 厶取范式( c n 功是极小不可满足的当且仅当它是不可满足的且 删去其中的任一子旬可以得到一个可满足公式极小不可满足问题是d 完全的，其中d 是所有可以描述成两个n p 问题的差的问题的类。 我们通常用公式差d ( f ) 对m u 进行公类，在文【9 ，z 3 “e ，已证明了一个结果：如果 d 但) 墨0 ，则f 不可能是极小不可满足公式于是，我们只对d ( f ) ) 0 进行分类对于 k 0 ，定义m u ( 豇) 一f f e m u l d ( f ) - 七 我们称一个m u 公式f 是最大的( m a x i m a l ) , 如果增加任意一个文字犯e l i t ( ，) ) 到 f 的任一子句c 中后( 请注意：工圣c ) ，产生的公式不再是极小不可满足公式( 此时，新 公式是一个可满足公式) 。m a x 表示最大的m u 公式集，m a x ) 一m u ) n 脱4 x 对应地，一个m u 公式f 是边缘的( m a r g i n a l ) ，如果从f 中删去任意一个文字后，得到 一个非极小不可满足公式，m a r g 表示边缘的m u 公式集且 肥根g ) - m u ) f 1 m a r g 。 一对子句c 1 和c 2h i t t i n g 的，如果c l 和c 2 中存在一对互补文字，即存在文字l 使 得c 1 且，c ：如果一对j 矗玎嘲子句c l 和c 2 中恰有一对互补文字，则c 1 和g 的 消解不会产生重言式子句一个c 伊公式，中的任意两个不同的子句中恰有一对互补文 字，我们称f 为非重言h i t t i n g 公式( n o n t a u t o l o g i c a l h i t t i n g ) 。我们用r - h 盯表示非重 言的h i t t i n g 公式类。类似地，可以用公式差对胛h i t 进行分类，并记 n t h i t ( 七) - f n t 一盯丁j d ( f ) 一七) 不失一般性，我们假定r 一脚r 中的公式f 满足如下条件： ( 1 ) f 中的每一个变元x 正、负文字都出现，b p p o s o ，f ) 1 r n e g g ，f ) 1 ( 2 ) f 中无重言式子句即不会出现一个子句同时包含一对互补文字x 、一x 我们记：脚r 一 f c ： r f i v ，g ，f g ，存在文字l ：工，且，l 曲 胛一尼盯妒c f i v ，g f ，f g ，存在唯一的文字：工f 且- l g 1 0 h i t m u h i t n m u 。 n t h r r m u - n t h l t n m u n t h r r ( k ) - f l f r - h i t ，d ( f ) 一后) ， h i t 一肘u ) 一m u ) n h r r ， n t h h - m v ( k ) - n t h 玎n m u 3 2 极小不可满足公式的若干性质 性质1 ( 分裂定理) 1 0 1 设 f - 盼v 矗) ，0 v ) ，口，( 吖v & ) ，( - x vg f ) 】 为一公式，其中b 不含有x 和，x 令 r x 】- 【 ，曰】，f - x 】。【岛，g ，b 】 则f m u 当且仅当下面的( 1 ) ( 3 ) 成立： ( 1 ) 存在极小不可满足的公式只c _ f p , 】和l f - 司，使得 【 ，正】只【g l ，g ，】l ( 2 ) 对任意极小不可满足的公式e ，扛】及匕f 卜叫， 【 ，l 】e 【，& 】j ；二 ( 3 ) 对任意极小不可满足的公式e ，扛】及t 。研一x 】， ( e n b ) u ( l n 口) b 性质2 设 f 置【 v ) ，ov 正) ，b ，( ，工vg 。) ，( - xvg f ) 】 为m ( k ) 中的一公式。x 和一x 不出现在b 中设，中的每一文字至少出现两次， 则f m u ( k ) 当且仅当 ( i ) f 的每个真子集是可满足的； i i ) 存在集合巨，b 。及c ，使得【吃，c ，b 。卜b 且 e - 【五，丘，e ，c 】m u g k 一1 ) ，f 。【g l ，岛，b 。，c 】m u 仁k 一1 ) 性质3 设为一文字，且设 f 一陋v ，- lv ，】，f - 【f ，k 】 则f m u 当且仅当f 的每一真子集可满足且f e m u 定理3 ( 坍塌定理) 设l 为一文字，且设 f 叫王v ，工v ，2 ，】，f 一陋v ，2 ，】，f - f ，】 假设矗，z ，则f c _ m u 当且仅当 ( i ) f 的每个真子集是可满足的，且 1 1 ( i i ) f e m u 或者f 。肘u m u ( 3 ) 和m u ( 4 ) 都是多项式可解的 在本章中，如果不加特别说明，f 总是指满足如下条件的公式： ( i ) f 中的每一文字至少出现两次， ( i i ) 不存在，g e f ，使得，g 性质4 设 f 一【 v ) ，0 v 正) ，b ，( 吣v9 1 ) ，( 吖vg f ) 】 为m ( 3 ) 中的一公式f 的每一真子集都是可满足的，则f e m u ( 3 ) 当且仅当存在 【色，c ，儿卜b ，使得静d ( 只) ，撑c z p 。) 1 且 【五，正，e ，c 】 虹，g2 ) ， 【g l ，g t ，b 。，c 】 f u ( j 3 证：由推论3 直接得到 性质5 【2 0 】设 f 一【o v 五) ，o v 正) ，曰，( ，z v9 1 ) ，( 吖v & ) 】 为中( 4 ) 中的一公式，j ，f 3 ，f 的每一个真子集都是可满足的，贝i j f e m u ( 4 ) 当且仅当 存在【以，c ，b 。卜b ，使得群c f ( e ) ，# c l ( b 。) 蔓l 且 【五，正，e ，c e m u ( s2 ) ，【，岛，b 。，c e m v ( s 3 ) 证：根据推论3 知f e m u ( 4 ) 当且仅当存在【e ，c ，b 。】t b ，使得 【 ，正，e ，c e m u ( 3 ) ， g ，g ，b 。，c e m u ( 2 ) 用只和l 分别表示【五，正，吃，c 】和【g 。，毋，占0 ，c 】因为f o ( 4 ) ，容易看出， 口，一 x ) e 且艮一 一石) 只， 从而，群v 缸只) - 样v 砥l ) - n - 1 ，故 撑c f ( e ) s 撑d ( f 肛】) = n + 4 - t 芋n 一1 且 x ) = n + a - t n + l且 群c f 伊【_ ，石】) 一忍4 - 4 - s s ，l + 1 这一事实蕴涵了引理的结论 性质6 9 1 一公式f m ，( 3 ) 是否是极小不可满足的问题可在0 0 5 ) 时间内判定，其中n 是 f 中变元的个数 证：用如下算法来判定中( 3 ) 的公式是否是极小不可满足的该算法基于过程脚( f ，3 ) 与s a t ( f ，3 ) 以及引理4 a l g o r i t h ma ( ，3 ) ( i n p u t ：公式f 中+ ( 3 ) ) o u t p u t ：y e s ，如果f e m u ( 3 ) 否则，n o b e g i n s i m p l i f i c a t i o n b e # n i f f 含有一文字但不含，t h e nr e t u mn o i f # v a t ( f ) - 1 且f 乒b ，一x t h e nr e t u r n l l o r e p e a t i f f 中存在重言子旬t h e nr e t u mn o ， i f 存在f ，g e f 使得，g t h e nr e t u r n n o i f f - 【( lv ，) ，( 工v9 1 ) ，( 1 工vg ，) ，】t h e nf ，r e s v ( f ，l ) u n t i l f 中无重言子句，不存在f 和g 使得，g ，且，中每一文字至少出现两次 i f f - - 口 t h e nr e t u r n y e s i f k = lt h e nr e m m n o ， e n d s a t i s f m b i l i t yt e s t ， b e g i n ， f ：【，岛，f 删】 以i 静v a r ( f ) f o r f 匕满足万一2 # c l ( f ) 甩+ 1 i f 【口f ，纬，f e m u g2 ) t h e nr e t u r nn o e n d f o r e n d， s p l i t t i n go ft h ef o r m u l a b e g i n l e t 石为f 中的第1 个变元 f - ( x v f o ， v 正) ，曰，( 一x v g ，) ，or a l ( - x v g t ) 口f 中无x 和_ ，x 的出现) f o r 集且和儿满足孝c z 暇) 静c f ( 儿) 墨1 和b 一限，c ，b 。】 e 1 【 ，且，c 】 l - g l ，晶，b 。，c 】 i f e e m u ( 0v x v a r ) ( 2 ) f 中没有重言式子旬 ， f n t h l t 证明：( t - ) 假定存在一个公式f ( 含有n 个变元脚个子句) 满足如下条件： ( 1 ) p o s ，f ) 0 n e g f ) 0v x e v a r ) ( f 中没有重言式子句 ( 3 ) f n t 一脚 并假定f - 正，厶) ，v a r ，f ) - ，毛) 由f 包含变元 气，吒 ，有9 ( 联。) - 1 由f e n t h i t ，有妒( 日乞) 一伊( 日纛) - 1 由f 中无重言式子句，有妒( e 巳) 一1 因此，伊( 以，) 一1 ( - ) 假设日。是可满足的，我们有一个真值指派妒使得妒( 以，) - i 我们对含有万个变元而，一，毛，m 个子旬的f 构造如下： 步骤1 对任一七，1 s k 葺m ，无- 彩； 步骤2 叠 t i 妒( 鼍) 一1 ，l sz s 埘 ； 步骤3 k t 2 ： 步骤4 对于1 i s n , 1 sz 1 因此，我们必须考虑子句对：( ，2 ) ，( ，厶) ( ，4 ) ，并且只有两个变元( 如吃) 不失一般性，我们假设： 9 ( h ：) 一驴( 沁) - 妒( h ) t 1 或 伊( 1 m ) 一妒( 3 讪) 一1 和妒( j ) ，1 情形i 伊( 钆，2 - 驴( 、l ，3 ) 一妒( ) - i 由妒饵i ) - 1 ，我们有妒( j ) 一伊( 3 t ) 一妒( 黾a ) 一0 由妒( 日；。) 一1 ，我们有驴瓴，2 ) ) i p 魄2 a ) 一妒也剐) 。1 于是妒( ，江2 jv ，毛；4v 一屯a 4 ) - 0 这又与妒( 砭4 ) 1 相矛盾，因为( 一屯鼬v 叫吃2 - 4v 一工2 ，3 ) 是n 。4 的一个子旬 情形z 妒( 3 m - 妒( 畸舶) 一1 和伊，1 4