（微电子学与固体电子学专业论文）动静结合排序决策的可满足性问题解决器.pdf

摘要 摘要 可满足性问题是被广泛研究的基本n p 问题之一。电子设计自动化、人工智 能，计算机科学、运筹管理等方面的许多问题都可以简化成可满足性问题，可满 足性问题的算法上的改进也极大地促进这些相关领域的发展。 本文在研究、探讨可满足性问题算法及其实现技术的基础上，选择目前的 主流算法基于d p l l 完全算法，针对其中很重要的组成都分搜索决策方 面作了深入的研究，提出了一种新的，高效的搜索决黄策略，采用动静态排序相 结合的策略可满足性问题解决器。 具体贡献是： 1 ) 研究了静态排序对算法的贡献，针对静态排序的特点，采用了一种有效 地体现实际问题特征的静态分析方法，根据变量正反文字出现次数的乘积，进行 初始排序，优先考虑正反文字出现次数较多变量的赋值； 2 ) 权衡比较了多种动态排序策略，采用一种既能及时反映算法过程中问题 特征，动态更新排序，又不需耗费大量计算机资源的策略，给冲突子旬中的变量 活跃性因子增加一个随时间增大的变量，把变量顺序提到比它活跃性因子小的前 面，体现了冲突驱动，并动态更新变量顺序，优先考虑发生冲突子旬中变量的赋 值，尽可能避免当前冲突； 3 ) 把这两种不同的排序方法结合到一起，互相促进，弥补各自的缺陷，成 功地提高了算法的速度。 实验表明：与采用其它决策策略的解决器相比，本文的解决器拥有一定的 速度优势。 关键字可满足性问题；d p l l ；决策；冲突；动静结合排序 中图法分类号t n 4 0 7 3 一 a b s t r a c t a b s t r a c t s a tp r o b l e mi sw i d e l ys t u d i e d t h ep r o b l e m si nm a n ya r e a ss u c h e l e c t r o n i c d e s i g na u t o m a t 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 m p u t es c i e n c ea n do p e r a t i o n sr e s e a r c hc a l l b ep r e d i g e s t e di n t os a tp r o b l e m s t h ei m p r o v e m e n ti ns a ts o l v e r sc a nr a p i dt h e d e v e l o p m e n t i ns u c ha e a s a f t e rs t u d i e dt h es a ta l g o r i t h m sa n ds a tt e c h n i q u e w ec h o o s et h em a i n a l g o r i t h m s t h ec o m p l e t e ds o l v e rb a s e do nd p l lm e t h o d ，s t u d yt h es e a r c ht e c h n i q u e ， o n eo ft h em a i np o r t i o n so fd p l l ，a n dd e v e l o pan e we f f i c i e n ts a ts o l v e r w e c o m b m ed y n a m i ca n ds t a t i co r d e r i n gs e a r c ht e c h n i q u e i nt h e p a p e rw eh a v es u c hc o n t r i b u t i o n sa sf o l l o w ： f i r s lw es t u d yt h ec o n t r i b u t i o n so fs t a t i co r d e r i n g a c c o r d i n gt ot h ec h a r a c t e ro f s t a t i co r d e r i n g ，w eo s et h em o s te f f i c i e n to n e ，o r d e r i n gb yt h ev a l u ef 【x ) + f t - - x ) ，w h e r e f ( x ) i st h en u m b e ro fl i t e r a lxi na 1 1c l a u s e s w ea s s i g n e dt h ev a r i a b l e sw i l l ll a r g e r f t e q u e n c yb o t hp o s i t i v ea n dn e g a t i v el i t e r a l s s e c o n d ，f r o mm a n yd y n a m i co r d e r i n gt e c h n i q u e sw ec h o o s et h eo n e ，w h i c hc a n n o to n l yr e f l e c tt h ec h a r a c t e r sd u r i n gt h ec , o l , l r s eo fa l g o r i t h m si nt i m e , b u ta l s o d y n a m i cu p d a t et h eo r d e rw i t h o u tm u c hc o m p u t e rs o u r c e w ea d dai n c r e a s i n g v a r l a b kt ot h ea c t i v i t i e so f t h ev a r i a b l e si nt h ec o n f l i c tc l a u s e s ，t h e nm o v et h ev a r i a b l e i nf r o n to ft h eo t h e rv a i l a b l e sw i t hl e s sa c t i v i t i e s ，w et h i n ko f t h ev a i l a b l e si nc o n f l i c t c l a u s e sf r r s t , t r yt oa v o i ds o m es i m i l a r i t yc o n f l i c t s t h r d , w ec o m b i n e dt h et w ot e c h n i q u e s t h e yb r i n go u tt h eb e s ti ne a c ho t h e r , m a k eu pt h el i m i t a t i o no f e a c ho t h e r w ei m p r o v et h es o l v e rs u c c e s s f u l l y m a n ye x p e r i m e n t ss h o wt h a to n rs o l v e rg a i n sm u c hp e r f o r m a n c et h a no t h e r s t a t e o f - a r ts o l v e l nw i t hs o m eo t h e rs e a r c ht e c h n i q u e k e yw o r d s ：s a t ；d p l l ；d e c i s i o nm a k i n g ；c o n f i i c t ；o r d e r i n gc o m b i n i n g d y n a m i ca n ds t a t i c 4 第一章绪论 第一章绪论 1 1 可满足性问题的研究背景 可满足性问题( p r o p o s i t i o n a ls a f i s f i a b d i t yp r o b l e m ，以下简称s a t ) 是：给 定一个命题逻辑公式，判定是否存在一个真值指派使公式为真。看似简单，却是 六大基本n p 完全问题之首，是第一个被证明具有n p 完全性的问题【1 1 。同时， 它是计算机科学和人工智能等学科中一个很重要的问题，从1 9 6 0 年提出到现在， 得到了越来越广泛的研究和应用。它具有如下的特点： ( 一) 基础性 数理逻辑是用数学方法研究逻辑问题，是哲学和数学之间交叉学科。一般来 说，数理逻辑可以分成五大部分：逻辑演算、证明论、集合论、模型论、递归论 【5 1 。在这五大部分内容中，逻辑演算( 命题演算和谓词演算) 是数理逻辑的基 础部分，这部分讨论的内容是纯逻辑的内容，其它四部分和数学密切相关，或者 本身就是数学问题。命题演算研究大致可以分为经典一阶逻辑( 简称经典逻辑) 、 非经典逻辑两大类。非经典逻辑大致可以分成两大类：一类持有与经典逻辑不同 的观点，如多值逻辑、构造性逻辑；另一类是经典逻辑的扩充，如模态逻辑和时 序逻辑。证明命题的可满足性是其中很基础的一类，s a t 问题是数理逻辑中很基 础的一类问题。 命题演算 谓词演算 经典一阶逻辑 性( s a t ) 非经典逻辑雕薹霎辑 5 - 足性性满靠备 可可完 ，f1【 ) 算演 论论论论 辑 明合型归 逻 证集模递 辑 逻理 数 第一章绪论 ( 二) 实用性 根据文献1 6 】的归纳，s a t 技术应用到了如下诸多领域： 数学：判定图的同构、图着色、寻找图的欧拉回路和生成树等： 计算机科学及人工智能：逻辑规划、产生式系统、真值维护等； 集成电路设计自动化：测试和验证，逻辑综合、布线和路径延迟分析等； 机器视觉：图像匹配等； 机器人：装箱问题等； 数据库系统：数据库一致性维护、查询优化等； 文本处理：手写文字识别等。 此外还应用于计算机图形学、计算机体系设计、高速网络以及通讯等领域。 总的来说，s a t 问题是一个多学科交叉研究的问题，包含了数理逻辑、计算 机科学、人工智能、运筹学、优化决策以及工程领域的研究。一方面促进了相关 学科的发展，同时也在相关产业中解决实际问题作出了贡献。 ( 三) 复杂性 早在1 9 7 1 年的a c m 的计算机理论研讨会( s 1 d c ) 上，s a t 问题就在算法 复杂度上被证明是一个n p c o m p e t e ( n o n d e t e r m i n i s t i cp o l y n o m i a l ) f q 题 1 】根据 目前计算机界的研究成果，人们通常认为，对于n p - c o m p l e t e 问题，现阶段不 可能有多项式时间复杂度的算法，7 0 个变量的规模，就是2 7 0 的计算量，是当今 计算机处理的极限。由此产生了一种主导观念：无论解的效果如何，能用一个算 法或集合已有的各种方法，求得一个解即可。因此，启发式算法在求解s a t 问 题的过程中被广泛使用。经典的理论结果一般是考虑所有情况，特别是最坏庸况， 但在各个领域的实际应用中，最坏情况不会每次都出现，人们往往可以利用实例 的一些具体特性对算法加以优化，从而突破理论上的禁区。现在，人们在s a t 问题上已经可以处理1 0 0 0 0 个变量以上规模的实例，因此，s a t 问题的理论研究 已经走向了实际应用。在此同时，人们还是在寻求一些可以适用于大部分领域的 优化方法。 1 2s a t 问题及其算法研究的历史和现状 s a t 问题及其算法的研究经历了一个起伏的过程。早在2 0 世纪6 0 年代初就 提出了s a t 问题的完备算法：基于回溯的搜索算法d p l l 算法 7 ，8 】。但是 因为s a t 问题的复杂性，特别是在s a c o o k 证明了s a t 问题的n p 完全性之 后，人们研究s a t 问题的兴趣慢慢减弱。直到9 0 年代，新的思想、算法的出现， 特别是基于d p l l 的完全算法中学习、非同步回溯技术的提出，使解决问题的规 6 第一章绪论 模极大地发展，s a t 问题的研究重新焕发了新的活力。大家尝试从不同的角度出 发寻找思路，采用新的方法，包括：数值优化( 最速下降法、拉格朗日乘数法等) 、 运筹学( 割平面法、内点法等) 、仿生( 遗传算法、神经网络等) 、仿物理现象( 模 拟退火、电荷吸引等) ，局部搜索( 爬山法、随机搜索等) 。同时，计算机运算速 度，内存空间及其并行处理能力大幅度提高，为算法测试提供了良好条件。另外， 科学家们也纷纷开始用s a t 来解决各种实际问题。 从1 9 9 6 年开始，举办了全世界范围内的s a t 竞赛( 9 ，用来验证新的有挑战 性的测试实例、促进新解决器的提出、当前国际领先的解决器的性能比较，鼓励 基于s a t 技术在实际问题中的应用。在其中表现突出的高效率算法的代表主要 有：基于d p l l 的完全算法以及启发式的局部搜索算法。 1 3 本文的研究内容及文章结构 本文研究内容包括：对s a t 问题及其解法的研究，重点研究d p l l 完全算 法，在此基础上，对d p l l 算法提出一些新的启发式算法，提高算法速度。在程 序开发的过程中，结合当前国际上研究的最新理论和技术，对各种算法和技术进 行整合和修正，并提出自己的改进方案，来提高算法解s a t 问题的效率。 本文的组织如下：第二章详细介绍s a t 问题及著名的c o o k 定理。第三章介 绍解s a t 问题的主要算法。第四、五、六章为本文的重点，介绍基于d p l l 的 完全搜索算法、以及一些启发式策略，本文在决策策略、以及在学习子句管理上 的研究。第七章为实验结果及其展望。 7 - 第二章可满足性问题基础 2 1 命题逻辑 第二章可满足性问题基础 数理逻辑是用数学的方法研究思维形式的逻辑结构及其规律的一门学科 【2 , 3 ，4 ，5 。所谓数学方法，就是用一套符号，来表达思维的逻辑结构和规律。命 题逻辑( 又称为命题演算、布尔逻辑) 是数理逻辑的基本组成部分，也称为“联 结词逻辑”。命题逻辑是研究以简单命题为基本单位由联结词结构构成的复合 命题的逻辑特征及其规律的逻辑理论。命题是反映事物情况的思维形态，比如事 物的属性、所处环境、与其它事物间的联系等。简单命题就是不包含任何其它命 题的命题，复合命题则包含其它命题。真和假是命题最重要的一种性质，命题逻 辑只考虑命题的真假含义，不考虑命题的其它意义内容( 如心理的、情感的内容 等等) ，因而又称为二值逻辑、布尔逻辑。命题联结词是表示命题与命题问关系 的语词，通过联结词的联结，就能得到更多的复合命题。在数理逻辑中常见的 联结词有五个： “一”表示否定，相当于“非”； “ ”表示合取，相当于“并且”； “v ”表示析取，相当于“或者”： “一”表示蕴涵，相当于“如果，则”； “一”表示等值，相当于“当且仅当”。 复合命题的真假完全取决于其中命题的真假，即一旦支命题的真假确定之 后，相应的复合命题的真假也就确定了，复合命题和支命题间的关系是有数学上 自变量和变量的函数关系的。 称复合命题联结符的集为完备的，当且仅当任何n ( n 1 ) 元的联结符号能 由其中的联结符定义。 一、 ，v 就是一个联结符的完备集。 2 2 命题逻辑的基本概念 定义2 2 1 命题变量和原子公式 命题是表示知识的陈述性形式。命题变量是指任意的一个命题，每个命题 变量可能为真，也可能为假。一般命题变量用小写的字母来表示，可以用1 、0 来分别表示命题的真假值，也可以用t ( t r u e ) 、f ( f a l s e ) 来表示。命题变量 8 第二章可满足性问题基础 本身称为原子公式； 定义2 2 2 文字正文字和负文字 原子公式本身称为正文字，其否定称为负文字。正文字和负文字统称文字 ( i n e r a l ) ，文字的正负有时称为符号( s i g n ) ，有时称为相( p h a s e ) ； 定义2 2 3 子旬 若干个文字的析取构成一个子句； 定义2 2 4 合取范式( c o n j u n c t i v en o r m a lf o r mc n f ) 范式就是规范、标准的公式，在数学中一般称为“通式”。命题逻辑的范式 只包含联结词一、 和v ，并且其中否定符号一只属于一个命题变量，就是范式， 若干个子旬的合取称为合取范式，同样若干个子句的析取称为析取范式 ( d i s j u n c t w en o r m a lf o r m ) 。任意公式，都有与之等值的合取范式和析取范式； 定义2 2 5 子句长度 一个子句中文字的个数称为这个子句的长度： 定义2 2 6 正子句负子句和混合子句 只含正文字的子句称为正子句，只含有负文字的子句称为负子句，既含有 正文字、又含有负文字的子旬称为混合子旬； 定义2 2 7 单子句 只有一个文字的子句称为单子旬，或称为单元子句； 定义2 2 8 空子句 不含文字的子旬称为空子旬； 定义2 2 9 赋值和解释 从命题变量集合到真假值集台 o ，1 ) 的函数称为真值赋值，简称赋值，又叫 解释。如果这个函数没有完全定义，即只有一部分变量具有真假值那么称为部分 赋值。一个变量x 的赋值，可以记做v o 【) ，v ( x ) o ，1 ，给x 赋值为v o 【) 可以 表示为( x ，v ( x ) ) ，或者x v ( x ) ； 定义2 2 1 0 模型可满足性、不可满足性和重言式 如果有一个赋值，可以为部分赋值，使公式j 的值为1 ，那么j 是可满足的a 使得它满足的这个赋值称为j 的一个模型。如果所有可能的赋值都无法使到j 满 足。则j 是不可满足的。如果对于所有可能的解释公式j 的值都为1 ，则称j 为重 言式或永真公式； 定义2 2 1 1 自由变量和自由文字 如果一个公式中的一个命题变量其真值没有确定，则称为自由变量，自由 变量对应的文字称为自出文字； 定义2 2 1 2 纯文字 9 第二章可满足性问题基础 在一个c n f 中如果一个命题变量只以一种形式的文字出现，要么全是正文 字，要么全是负文字，则称相应的文字为纯文字。 2 3 可满足性问题 可满足性问题是六大基本n p 完全问题之首 5 ，也是第一个被证明具有n p 完全性的问题【1 1 。可满足性问题的描述十分简单，可以用c n f 表达式描述： 定义：可满足性问题。给定一个c n f 表达式，问是否存在在变量集合v 上 的一组真值赋值，使表达式的值为l 。若存在这样的真值赋值，则称原问题可满 足，否则称为不可满足。 如果c n f 中所有子句的长度都为k ，则该公式所表示的s a t 问题称为 k s a t 问题，如2 - s a t ，3 - s a t 问题。 值得提醒的是，并不是所有的c n f 表达式的可满足性问题都是n p 完全问 题。可满足性问题一般表示成子句长度不定的c n f 表达式。当然也存在一些特 殊的c n f 表达式，它们的可满足性问题是多项式时间可解的，如子句长度都小 于3 1 5 1 或所谓的h o m 子旬【1 1 ，1 2 ，2 - s a t 问题就是多项式可解的【1 3 。虽然可解 的c n f 表达式种类很有限，但是对于它们的分析有助于解决一般性的可满足问 题。 由于在第一章中提及，n p 完全问题具有相互多项式时问复杂性内转化的特 点，因此所有其他的n p 完全问题都可以转化为可满足性问题。而可满足性问题 因其提出较早，表述简单而被广泛的研究。 2 4 n p 完全 n p c o m p l e t e f n p 完全) 一词是用以描述下列意义下的n p 类中最难解决的问 题【1 0 】：若n p 完全中的某一问题存在一个多项式时间算法，则n p 类中每一个 问题都存在着一个多项式时间算法。常见的图的最大独立集和最小覆盖集问题， 哈密尔顿回路问题，作业调度问题，装箱及背包问题都是经典的n p 完全问题 通俗地说，若有一个n p 完全问题找到了多项式时间的算法，则所有的n p 完全问题都有多项式算法。我们可以用下面这个简单的示意图来表示这样的关 系，如图2 1 所示： 1 0 第二章可满足性问题基础 图2 1p 、n p 问题关系示意图 对问题进行分类是人们在研究实际问题中常用的手段。人们发现了n p 问题 是一类很大的问题集，在这类问题集中，有些对计算机来说是容易解决的，即所 谓的p 问题。还有一些问题是难对付的，然而在多项式可规约的观点下，我们再 对这些难题作进一步的划分，从中分出一类可视为相互“等价”的问题( 等价是 说它们的求解难度相当，而且只要其中一个找到了有效的算法，则意味着其余的 都可以找到有效的算法) ，即n p 完全问题。 2 5 多项式时间和非多项式时间 为什么强调哪些问题是有多项式时问算法的，哪些问题是非多项式时间算 法呢? 这是因为对这些离散的组合优化问题来说，理论上都是可解得，比如用简 单的穷举法就可以得到答案，而在实际中往往不可行。穷举法大多是非多项式时 间的。看下面两个表就可以知道多项式时间算法和非多项式时间算法( 以指数时 间算法为例) 的重大差别： 表2 1 多项式时间算法与指数时阋算法运行时间比较 规模n 时间复杂度 1 03 06 0 n 21 0 4 秒9 1 0 6 秒3 6 1 0 4 秒 一1 秒 2 7 1 0 4 秒2 1 6 1 0 3 秒 2 01 旷秒 1 0 7 4 秒 3 6 6 钜 3 “5 9 1 0 。4 秒9 + 1 0 4 秒 1 3 1 0 “世纪 第二章可满足性问题基础 表22 提高计算机速度对单位时间内可解问题规模的影响 单位时间内可解问题规模 时间复杂度 当前计算机快1 0 0 倍快1 0 0 0 倍 n 2n 1 0 n3 l6 n n46 4 n1 0 n 2 “nn + 6 6 4n + 99 7 3 “nn + 4 1 9n + 62 9 由上面两个表可以看到，非多项式时间的算法解较大规模问题是不可行的， 即使提高计算机的性能也不能带来太大的帮助，同时也反映了设计好的求解算法 意义重大。 2 6 c o o k 定理 s a c o o k 在他著名论文“定理证明过程的复杂性”中成功地证明了第一个 n p 完全问题s a t 问题。他在1 9 7 1 年给出了著名的c o o k 定理及其推论 1 】。 定理：若len p 类，则les a t 推论：p = n p 等价于s a tep 。 c o o k 定理告诉我们任何n p 问题都能通过多项式时间归约为s a t 问题；其 推论说明只要s a t 问题获得多项式时间解法，则所有n p 类问题都可以获得多项 式时间解法，即证明了p = n p 。 从c o o k 定理及其推论可知，, s a tf 司题是n p 完全问题，并且，人们己将 其作为n p 完全问题的难度标准 迄今为止尚未能够证明p = n p ，即对于任何一个n p 完全问题都未找到多项 式解法，丽同时也未能证明p ：# n p ，因为同样未能证明其中属于n p 类的一个问 题不存在多项式解法。对p n p 的研究是计算机理论科学中璀璨的也是棘手的 跨世纪问题， c o o k 定理奠定了s a t 问题在研究n p 及n p 完全问题的计算机理论界的极 为重要的地位。 一1 2 - 第二章可满足性问题基础 2 7 算法评价 算法的评价是一项非常重要而且艰难的工作。对于可满足性问题算法，目 前常见的主要有如下三种：最坏情形分析，概率分析和计算实验分析。 2 7 1 最坏情形分析 主要在理论上分析算法在最坏情形下时间复杂性或得到的最坏的解。因为 算法不是针对问题的某个实例而设计，它应该针对问题所有实例都适用。很多时 候，算法在某些实例上的效果非常好，在某些实例上则不那么令人满意。最坏情 形分析是把算法最不令人满意的情况找出来。常常用组合数学和不等式等数学工 具，分析的方法多是构造性的。【4 5 ，4 6 ，4 7 】 2 7 2 概率分析 最坏情形分析是以算法最差的性能来评价算法，而概率分析则不同，它是 从整体上对算法惊醒评价，既考虑算法差的性能，同时也考虑好的表现。这种方 法通常假设问题的某些参数服从一定的概率分布，本质上是假定实例的分布情 况，然后用概率的方法分析不同性能的概率分布，整体评价算法。用到概率和统 计等方面的数学工具。【4 9 ，4 9 j 2 7 j 计算实验分析 计算实验分析与前面两种分析方法不同主要在于：前两种分析方法郜需要 对问题和算法都有很深入的了解，而且需要较深的数学理论，所以实际执行起来 有很大的困难；而计算实验分析则可以通过模仿物理实验的方法，用大量的实例 来测试算法，通过测试结果来评价算法的优劣。这样，计算实验分析的方法就更 容易实施，而且适用性更广泛，特别工程上的应用。事实上，最坏情况和概率分 析方法大多只能针对简单问题，规模较小的问题，作假设，然后分析，而大规模、 复杂问题是力不从心的。在可满足性问题上国际上举行的s a t 竞赛，采用的 就是计算试验分析，通过测试大量的实例，比较运行时间。同时，也评价哪些具 体实例是难测的。 1 3 第二章可满足性问题基础 2 8 本章小结 本章从数理逻辑出发，介绍了可满足性问题的一些基本概念以及计算复杂 性方面的知识。可满足性问题之所以引起广泛的研究，其中主要是因为它是n i p 完全问题，这类问题有相当的难度，而且有很重要的现实意义和理论价值，特别 是大部分学者都认可p n p 这一著名的猜想，这类问题目前不可能有一般意义 下的有效算法。这促使人们想方设法去寻找更有效的方法，从而促进算法学的飞 速发展。 1 4 第三章可满足性问题算法 第三章可满足性问题算法 如绪言所说，解s a t 问题的算法很多，当前主要的算法可以分成以下几类： 基于d p l l 的完全算法、启发式局部搜索算法、二叉判定图法( b i n a r yd e c i s i o n d i a g r a m s ) 、随机探索算法、整数规划方法等。d p l l 算法将在第四章作详细介 绍，下面简单介绍余下的算法。 3 1 局部搜索算法 局部搜索算法( 1 0 c a ls e a r c h ) 是解决很多n p 完全问题( 特别是优化问题) f 的一种常用的方法。像s e l m a n 的g s a t 1 4 ，1 5 】、w s a t 1 6 ，顾钧的系列解法 【1 7 ，l s ，m a z u r e 的t s a t 1 9 ，b e n j a m i n 的离散拉格朗日算法 2 0 】。这类算法的基 本思想是，先给所有的变量赋值，可能使部分子旬的值为宾，部分子句的值为假。 然后反复地对现有赋值进行局部调整( 如改变一、二个变量的赋值) ，使得被满 足的子句个数越来越多。理想的情况下，最终将能得到一个解，使所有的子旬满 足。 算法过程中对各变量的赋值进行不断地变化，使得已满足的子旬的数目n 尽量接近该问题的子句总数目m ，如果某一个时刻，n = m ，则表明一个解已经 找到。在整体思路上可以采取全局的启发式算法，比如模拟退火算法。算法必须 允许算法过程中相对于局部最优点的变差情况，用以不断搜索全局最优点( 可能 存在多个) 。如图3 1 所示； 如e s o h ，6 0 ns v a c t 图3 i 局部搜索算法示意图 这种算法的个显然的缺点就是它的不完备性。若一个解被找到，此解必 1 5 - 第三章可满足性问题算法 然成立，则这个s a t 问题为可满足。如果在算法执行的时问之内，不能找到一 个解，则并不能说明没有解的存在，也就是说该算法不能证明一个s a t 问题的 不可满足性。 3 2 有序二叉判定图( o r d e r e db i n a r y d e c i s i o n d i a g r a m s ，o b d d ) 有序二叉图跟局部搜索算法不一样，它的表达方式不是合取范式，而是用 布尔算子( 逻辑连接符) i g t h e n - e l s e ，茼记为i t e 。它可定义为： i t e ( p ，e l ，e 2 ) 2 ( pae i ) v ( 呻ae 2 ) 这里，p 是布尔变量，e l 和既是布尔表达式。 对于布尔表达式f 和其中的变量x 。用“x 一0 】和f 【x 1 分别表示将 x 代换以0 或i 后所得到的表达式就可以得到s h a n n o n 展开式： f5x + f 【x l 】+ x + “x 一0 】 对应的i t e 表达式为 fi i t e ( x ，f x 一1 】，“x 一0 】) 我们往往用二叉判定树来形象地表示i t e 范式。树的每个叶节点标以0 或 l ( 表达式的值) ；而非叶节点v 以变量v a “v ) 为标记。非叶节点v 的两个子节点记 为l o w ( v ) 和h i 9 1 1 c v ) ，它们分别对应于该变量取值0 或1 的情况。把节点v 代表 的布尔表达式记为b e ( v ) 。可以递归地定义如下：如果v 是叶节点，b e ( v ) 就是它 所标记的真假值；即 b e ( v ) = m j ( v h ( v ) ，b e ( h i g h ( v ) ) ，b e ( 1 0 w ( v ) ) ) 如布尔表达式x v - - y ，等价于i t e ( x ， 1 ，i t e ( y ，0 ， 1 ) ) 。它可以 用下图3 2 ( a ) 来表示。 我们也可将判定树看成是有向图。每个非叶节点到它的每个子节点有一条 边，而树根和叶节点可分别看成是有向图中的源点和终点。所有的叶节点可合并 成两个；其中一个标记为0 ，另一个标记为1 。如上图3 2 ( b ) 所示。这样的图 称为二叉判定图( b i m r y d e c i s i o n d i a g r a m s ，b d d ) 。 1 6 第三章可满足性问题算法 ( a )( b ) 图3 2 二叉判定树和b d d 在从源点到终点的每条路径中，每个变量最多只出现一次。这样的路径对 应着给变量的一种赋值，而其终点表明在这种赋值下函数所取的值。每条终点为 l 的路径对应一种使布尔函数得到满足的赋值。 判定树( 图) 比较直观，但是大小随着变量的个数成指数级增长。因此。 只有在变量不太多的情况下，才用这两种方式来表示布尔函数。后来人们对b d d 进行改进。以得到更简洁的表示形式。 b r y a n t 2 1 ，2 2 1 对二叉判定图加以限制，得到有序二叉判定图( o b d d ) 。它是 一个与b d d 类似的有向图。所不同的是，它事先对变量排序，并要求：如果节 点u 到节点v 有一条边，那么u 的变量号必须比v 的变量号小( 除非v 是终点) 。 越靠近终点的内节点，其变量的序号越大。在从源点列终点的每条路径中，变量 都必须按照给定的顺序出现。例如，图3 2 ( ”中，变量的排列顺序为x v “( 瞄那么就选比较小的那个作为分裂变量x = w k r g ) 。之所 以如此，是因为不管b 等于0 还是1 ，f 【x b 】对应的节点就是r f 。而g 【x l 】和g 【x 一0 1 所对应的节点分别是r g 的两个子节点。假如我们让x = v a r ( r f ) 那 就不太好确定g 【x b 】对应的节点 对上面所述的a p p l y 运算还可以作一些优化。如果o p 是“与。而r f 是终 节点0 ，那就不需要选分裂变量，而是直接返回终节点0 。此外，还可以用一张 表记录中间结果，以避免重复计算。该表的每一项对应于二元组，j ，表示 a p p l y ( i ，j ) 所得到的节点号。 由于o b d d 是精简的判定图，所以在构造过程中一般还要用到一个哈希表 ( h a s ht a b l e ) ，避免生成同样的节点。我们可以根据三个参数x ，1 ，h 对表进行 查询，这里x 是变量号，1 和h 是节点号。如果目前已经有一个节点v 满足v a l ( v ) = x ，l o w ( v ) = l ，h i g l l ( v ) = h ，那么查询结果就是v 。这时就不需要分配新的节 点号。 除了a p p l y 运算外，还有其他运算，如r e s t r i c t 。它从函数f 中选择一 个变量x ，将其赋以真假值，得到一个新的函数，也就是本节开始时提到的f x 一1 】或f 【x 一0 】。给定f 的一个o b d d ，我们对其进行深度搜索。在为“x 一 0 】构造o b d d 时，对于v a r ( v ) = x 的节点v ，我们将指向v 的边改成指向 l o w ( v ) ；如果要为f 【x _ 1 构造o b d d ，就将指向v 的边改成指向1 1 i g h ( v ) 。同 a p p l y 运算一样，为了保证所得到的判定图是精简的，在r e s t r i c t 的实现过 程中也要用到哈希表。 利用a p p l y 和r e s t r i c t 运算，我们可以对布尔函数进行各种操作，比如 两个函数的复合此外，我们还可以根据下述等式判断q b f 的真假值 j x f = “x 一1 】+ f 【x 一0 】 v x f = f 【x 一1 】+ f 【x _ 0 一1 9 第三章可满足性问题算法 变量排序给定两个不同的变量排序，由同一个布尔函数可以得到不同的 o b d d 它们的节点数可能相差很大一个经典的例子【2 1 ，2 2 】是布尔函数x l y l + x 2 y 2 十十x 。y n 。如果所采用的序是均 y l x n y n ，那么得到的o b d d 只 有2 n 十2 个节点：而采用的序如果是x l x n y l 撤销假设赋”童莰冲突可满足解 图4 3d p l l 算搜索过 d p l l 算法就是从空的赋值开始，通过决策树始终维持为真的赋值方向， 来回穿梭于隐含真赋值的空间，直到使所有子句满足，或者遍历所有搜索空间， 证明式子不满足，是一种完全算法。 d p l l 深度优先算法的提出，消除了以往算法指数膨胀的内存需求，在s a t 问题研究上产生了深远的影响。 完全算法都是基于d p l l ，以下的算法都是在d p l l 算法基础上采用了启发 式算法，大致上采取的伪代码如下： w h ll e ( t r u e ) i fn oc o n f l i c tt h e n i fa l lv a r i a b l e sa s s i g n e dt h e n r e t u r ns a t i s f i a b l e e l s e d e c i d e0 p i c ku pa nu n a s s i g n e dv a r i a b l ea n da s s i g n i t p r o p a g a t e ( ) p r o p a g a t eu n i tc l a u s e s e l s e a n a l y z e 0a n a l y z ec o n f l i c t 突a n da d dal e a r n e d c l a u s e i ft o pl e v e lc o n f l i c tt h e n r e t u r nu n s a t i s f i a b l e 2 3 第四章基于d p l l 的完全算法 e l s e b a c k t r a c k ( )u n d ot h ea s s i g n m e n t sl e a d i n gt oc o n f l i c t 基本的d p l l 算法包含三个主要步骤： a ) 搜索决策 b ) 赋值过程 c ) 回溯过程 所谓搜索决策也叫变量决策，是指在还未被赋值的变量中选择某个变量，并 赋一个真值。变量的决策过程决定了。虚拟”搜索树的形状，也即找寻了一个变 量顺序。 在决策过程中，某个变量被选择赋值时所在搜索树的高度称为该变量的决策 层。同时称该变量为决策变量。相应的赋值称为决策相位。 搜索树高度的上界就是变量数。根据一般的s a t 算法的实现方式，同时为了 以后讨论的方便，节点在搜索树中的高度与普通标号方式相反，即令根节点对应 的高度为l ，其子节点依次递增。若某个变量的决策层越大，习惯称该变量的决 策层越“深”。 所谓赋值过程，即是对子句根据变量决策过程的赋值加以简化。例如对于子 句( x 。+ x ：+ x 0 ，如果变量决策过程选取了x 。并令它为0 ，则子句简化为( x 。十x 。) 。 当然，如果x l = l ，则子句已满足，可以暂时从问题中被删去，使原始问题中的子 句数相应减少。 所谓回溯过程，即当搜索遇到冲突时，搜索过程从深的决策层返回到浅决策 层。所谓冲突，即当对某个变量赋值时，至少存在一个子句同时不满足( 即子句 所有文字的值为0 ) 。 图4 3 说明了一个具体实例的基本d p l l 算法流程。 4 2 加速搜索过程的启发式策略 基本的d p l l 算法比最早的d p 算法优越在它所需要的内存空间并不是指数增 长的，而后者的内存空间呈指数增长。算法本身的处理规模虽然不大，当时主要 应用于定理证明等可满足性问题规模较小的领域，但它给以后进一步的提高奠定 了基础，特别是近十几年来的一些改进策略，使算法渐渐能够处理实际较大规模 的可满足性问题。本节及下一节就将回顾这些发展。本节主要从算法技术层上回 顾这些改进策略。 4 2 1 布尔约束传递过程( b c p ，b o o l e a nc o n s t r a i n tp r o p a g a t i o n ) 一2 4 第四章基于d p l l 的完全算法 布尔约束传递过程( b c p ) 是最早针对d p l l 算法提出的优化过程。随着搜索 过程的进行，变量不断被赋值，子句中未赋值的变量数的减少，会出现所谓的一 元子句，即子旬中除了一个文字外，其余所有文字的值均为0 。例如对于实例 ( x l + x 2 + x ，) ，当取a = o ，b = o 时，最后一个子句( x 。+ x ：+ x ；) 即成为一元子旬。显然， 若子旬需要满足，文字x 3 必须为1 ，即变量x 。必须为1 。这就是所谓一元子句规 则。所谓b c p 就是不断应用元子句规则，直到问题中不再存在一元子旬。b c p 过程是最简单的优化过程，然而对于d p l l 算法性能的提高有决定性的作用。b c p 过程之所以重要，是因为在实际的可满足性问题中，平均每个子旬所包含的文字 数目是有限且通常很小。因此搜索过程中一元子句出现的次数会很频繁。同时根 据实验，无论以后的优化措施有哪些，一般基于d p l l 的可满足性问题算法的运 行总时间有8 0 - - 9 0 耗费在b c p 过程中。 4 2 2 基于冲突的学习过程和非同步回溯 总结d p l l 算法的发展，具有里程碑性质的优化改进就是基于冲突的学习过 程和非同步回溯。所谓对d p l l 算法的优化，是指希望能减少搜索过程所搜索的 空间，即所谓的剪枝，剪去不需要搜索的空间。b c p 过程显然是利用了实际问题 转换得到的可满足性问题的结构特点来减少搜索空间。然而，仅仅利用了b c p 过程，还不能使算法实用化。而基于冲突的学习过程及其相伴随的非同步回溯是 使d p l l 算法能解决实际问题的关键。 在介绍基于冲突的学习过程前，我们先从蕴涵图的角度重新审视d p l l 算法。 定义4 1 ：蕴涵图。所谓蕴涵图( i g ， m p l l