（计算机应用技术专业论文）基于调查传播方法的qbf求解器.pdf

摘要 智能规划已经成为人工智能的研究热点，把智能规划问题转化为命题逻辑公式求解 是研究智能规划的重要方法。 量化布尔公式( q u a n t i f i e db o o l e a i lf o m u l a e ，简称q b f ) 是一种带有存在和全称量 词前缀的命题逻辑公式。当q b f 公式的量词中只含存在量词时，q b f 问题就转化为命 题可满足( s a t ) 问题。因此q b f 问题通常可以看作是s a t 问题的泛化。判断一个量化 布尔公式的可满足性需要判断是否存在一组命题变量的真值指派，使得公式在该真值指 派下为真。判断量化布尔公式问题的可满足性的计算复杂性要高于s a t 问题，是 p s p a c e 完备的。随着q b f 问题的求解效率不断提高，q b f 问题在诸如一致性规划、 验证、非单调推理、知识推理等方面都有着广泛的应用。 本文设计了一种新的基于d p l l 算法的q b f 求解器一s p q b f 系统。它将s u n ，e y p r o p a g a t i o n 信息传递方法第一次应用到q b f 求解问题中。把s u e yp r o p a g a t i o n 作为启 发式，引导d p l l 算法选择合适的变量进行分支，从而可以减小搜索空间，并减少算法 回退的次数。在分支处理过程中，s p q b f 系统结合了单元传播、冲突学习和满足蕴涵 学习等一些优秀的q b f 求解技术，从而可以提高q b f 问题的求解效率。实验结果表明， s p q b f 无论在随机问题上还是在q b f 标准测试问题上都有很好的表现，验证了调查传 播技术在q b f 问题求解中的实际价值。 关键词：人工智能；q b f 问题；q b f 问题求解器；因子图；调查传播；冲突学习； 满足蕴涵学习 a b s t r a c t r e c e n t l y ，m o r ea n dm o r er e s e a r c h e r sf o c u so ni m e l l i g e mp i a n n i n g t h ep l a j l n i n gs o l u t i o n b a s e do np r o p o s i t i o n a ll o g i cf o r m u i ai so n eo ft h em o s ti m p o r t a n tm e t h o d so fr e s e a r c h i n g i n t e l l i g e n tp i 猢i n g o n eo ft h ep r o p o s i t i o n a il o g i cf o 肌u l a ei sq u a n t i f i e db o o l e a i lf o m u l a e ，w h i c hc 锄b e s e e n 祁a ne x t e n s i o no fs a t i s i a b i l i 够( s a r ) w i t he x i s t e n t i a lo ru n i v e r s a jq 啪t i f i e r st oe v e 巧 v a r i a b l em p r o p o s i t i o n a lf o r m u l a c g i v e naq u a n t i f i e db 0 0 l e a i lf o m u l a ，t h eq u e s t i o no f d e c i d i n gt h es a t i s f i a b i l i 够o ft l ef o m u l ai sc a l l e daq u a n t i f i e db o o l e a ns a t i s f i a b i l i t yp r o b l e m ( q b f ) q b fi sa j li m p o n a n ti s s u ei na ib e c a u s ei ti st h ep r o t o t y p i c a lp r o b l e mc o m p l e t ef o ra c o m p l e x i 够c l a s s ，i e p s p a c e t h u s ，m a n yp r a c t i c a lp r o b l e m sc a j lb et r a n s f o r m e di n t oq b f e g c o n f o m l a j l tp l a n n i n g ，v e r i f i c a t i o n ，n o nm o n o t o n i cr e a l s o n i n ga n dr e a s o n i n ga b o u t k n o w l e d g e i nt h i st h e s i s ，w ep r e s e n tan o v e ld p l l - b a s e ds o l v e rf o rq u a m m e db o o l e a nf o 姗u l a e ( q b f ) ，n 锄e l ys p q b f t bt h ee x t e n to fo u rk n o 、纠e d g e ，t h i ss o l v e ri st h ef i r s tq b fr e a s o n i n g e n g i n et h a ti n c o 印o r a t e ss u n ，e yp r o p a g a t i o nm e t h o df o rp r o b l e ms o l v i n g u s i n gt h e i n f o m a t i o no b t a i n e d 行o mt h es n e yp r o p a g a t i o np r o c e d u _ r e ，s p q b fc 锄s e l e c tab r a n c h m o f ee x a c t l y f u n h e m o r e ，w h e nh a n d l i n gt h eb r a n c h e s ，s p q b fu s e ss o m ee m c i e n t t e c h n o l o g i e sf o rs o l v i n gq b fp r o b l e m sm o r ee 衔c i e n t l y ，s u c hz l su n i tp r o p a g a t i o n ，c o n n i c t d r i v e nl e a m i n ga s 、e ua ss a t i s f i a b i l i t yd i r e c t e di m p l i c a t i o na n dl e a r n i n g t h ee x p e r i m e n t a l r e s u l t sa l s os h o wt h a ts p q b fc a ns o l v eb o t hr a n d o mp r o b l e m sa n dq b fb e n c h m a r k p r o b l e m se 确c i e n t l y ，w h i c hv a l i d a ：t e sm ee 位c to fu s i n gs u n ，e yp r o p a g a t i o ni nq b fs o l v i n g p r o c e s s k e yw o r d s ：a r t i f i c i a li n t e l “g e n c e ；q u a n t i f i e db o o l e a nf o r m u l a ep r o b l e m s ；q b fs o l v e e f a c t o r 黟a p h ；s u r v e yp r o p a g a t i o n ；c o n n i c td r i v e nl e 锄i n g ；s a t i s 6 a b i l i 够d i r e c t e di m p l i c a t i o n a n dl e 1 l i n g i l 独创性声明 本人郑重声明：所提交的学位论文是本人在导师指导下独立进行研究工作所取得的 成果。据我所知，除了特别加以标注和致谢的地方外，论文中不包含其他人已经发表或 撰写过的研究成果。对本人的研究做出重要贡献的个人和集体，均已在文中作了明确的 说明。本声明的法律结果由本人承担。 学位论文作者签名： 学位论文使用授权书 本学位论文作者完全了解东北师范大学有关保留、使用学位论文的规定，即：东北 师范大学有权保留并向国家有关部门或机构送交学位论文的复印件和电子版，允许论文 被查阅和借阅。本人授权东北师范大学可以采用影印、缩印或其它复制手段保存、汇编 本学位论文。同意将本学位论文收录到中国优秀博硕士学位论文全文数据库( 中国 学术期刊( 光盘版) 电子杂志社) 、中国学位论文全文数据库( 中国科学技术信息研 究所) 等数据库中，并以电子出版物形式出版发行和提供信息服务。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名： 日 期： 学位论文作者毕业后去向： 工作单位： 通讯地址： 指导教师签名： 日 电话： 邮编： 东北师范大学硕士学位论文 己l 。皇 丁i 口 量化布尔公式( q u a n t i f i e db 0 0 l e a nf o m u l ，简称q b f ) 是指带有存在和全称量词 前缀的命题逻辑公式n3 。当q b f 公式的量词中只含存在量词时，q b f 问题就转化为命题 可满足( s a t ) 问题。因此q b f 问题通常可以看作是s a t 问题的泛化。判断一个量化布 尔公式的可满足性需要判断是否存在一组命题变量的真值指派，使得公式在该真值指派 下为真。判断量化布尔公式问题的可满足性的计算复杂性要高于s a t 问题，是p s p a c e 完备的引。 为了促进q b f 问题求解技术的发展，g i u n c h i g l i a 等人创办了国际q b f 问题求解器比 赛。3 。在该项比赛中涌现出一批优秀的q b f 问题求解器，如a d 印t i v e 2 c l s q 、g r l 喵。、 q b f b d d 旧3 、q c h a f j f l e a m 口3 、s k i z z o j 等。随着q b f 问题的求解效率不断提高，q b f 问题 在诸如一致性规划、验证、非单调推理、知识推理等方面都有着广泛的应用1 引。 目前大多数q b f 问题求解器都是在扩展原有的s a t 问题求解器的基础上设计的： ( 1 )g e n t 等人设计的q b f 求解器w a l k q s a t 在启发式设计中利用了s a t 问题求解器 w a l k s a t 的启发式方法”4 i 。 ( 2 )r o w l e y 等人设计的q b f 求解器w a t c h e d c s b j 使用的数据结构是通过扩展 s a t 求解器z c h a 神的监视文字这种放松的数据结构而得到的。副。 ( 3 )g i 吼c h i g l i a 等人设计的q b f 求解器q u b e 所使用的算法是通过扩展s a t 求解算 法d p l l 获得的，它所使用的数据结构和w a t c h e d c s b j 一样是通过扩展s a t 求解器z c h 碉呻所使用的监视文字这种放松的数据结构而得到的，它使用的 子句学习技术也参考了z c h a 肿所使用的子句学习技术n 刮。 ( 4 )r i n t a n e n 等人设计的q s a t 求解器所使用的启发式参考了s a t 求解器c s a t 中 所使用的m o m s 方法n 。 ( 5 )z h a n g 等人设计的q u a m e 求解器所使用的启发式采用了s a t 求解器z c h a f 冲的 变量状态独立衰退总和方法，它所使用的子句学习技术直接利用了z c 脚 所使用的子句学习技术n 副。 事实上，几乎所有高效的q b f 问题求解器都是基于d p l l 算法设计的，影响d p l l 算法效率的最主要的因素之一是分支的选取。为此研究人员采用了各种方法来确定 d p l l 算法的选择分支。c a d o “等人设计的e v a l u a t e 求解器采用了一种最朴素的方法一随 机选取方法，该系统也是最先将s a t 问题的求解方法引入到q b f 的求解方法中的系统之 一n 引。z h a j l g 等人设计的q u a m e 求解器借鉴了z c h a 觫解器中使用的变量状态独立衰退 总和的启发式方法n 副。r o w l e y 等人设计的w a l k q s a t 求解器借助的是w a l k s a t 启发式 方法：通过w a j k s a t 求解器找到一个文字来确定分支n 副。g i 岫c h i g l i a 等人设计的q u b e 求 解器采用的是b o l 吼和j w 2 的启发式方法：根据在最短的子句中出现次数最多的文字来确 定分支啪1 。 l 东北师范大学硕士学位论文 近年来，命题可满足问题( s a t ) 的求解能力有了很大程度的提高，但依然存在一 些开放性问题。1 9 9 9 年z e c c h i n a 等人在n a t l j r e 杂志上发表的论文指出求解怨s a t 问 题时，存在着从可满足到不可满足的相变，当0 【砒蹴， a 0 ) 。另一种是变量向子 句发送的消息，表示变量的赋值不能满足子句的概率。例如：图4 2 中右图，5 个子句 小6 、c 、d 、p 都包含变量x ，其中子句口、6 、厶p 包含文字x ，子句d 包含文字哨。 子句玑6 、厶p 向变量x 发送调查，因为变量x 以否定的形式出现在子句d 中，根据 这些调查，变量x 的赋值不能满足子句d 。 4 3 3 基于s u n ，锣p m p a g a t i o n 的分支选择 首先给出s u r v e yp r o p a g a t i o n 算法，如图4 3 所示。s u r v e yp r o p a g a t i o n 算法的输入参 数为最大迭代次数要求精度占。算法首先在f = 0 时随机初始化所有调查，然后反 复地利用调查迭代函数( u p d a t es p ) 依次更新调查( 第3 行) ，当连续两次迭代得到的所 有调查差的绝对值小于要求精度时，表明算法收敛，得到所有的调查。 东北9 币范大学硕士学位论文 p m c e d u ms u n r e yp r o p a g a t i o n ( 厶斌，占) j i f ( f = 0 )t h e ni n i t i a l i z e - - 圳； 2 f o rf = 1t of 2 3 仇，( 力2 u p d a t e - s p ( ) ； 彳 i f ( i _ ，( 力一仉卅( f 1 ) i 曩u 占) 5 t h e ng o t o7 6 e n d i b r 7 i f ( f = 。jt h e nr e t u mu n c o n v e r g e d ； 8 e l s e m t u r n ，7 0 。2 仉卅( 力 图4 3s u n ，e yp r o p a g a t i o n 算法 s p 算法得到的调查可用于估计每个变量在所有解中的统计特性( 称为偏量) ，这种偏 量分为正偏量和负偏量。正偏量指当随机选取一个簇时，变量f 被约束【“冻结”) 到而= l 的概率。类似的，负偏量指当随机选取一个簇时，变量f 被约束( “冻结”) 到施= o 的 概率。下面给出正偏量和负偏量的计算公式。 正偏量： i 志 ， 负偏量： 廿盎 ( 1 3 ) 其中， 蚺卜! ! ) ( 1 叩o 呱卜儿) ( 1 4 ) l4 d ：o )j 4 d ：“) 7 n i2 卜跗叫+ 一忸) ( 1 - 叮一 ( 1 5 ) l 4 e t i f j 4 e l ( ，) 、 n ? = 兀( 1 一儿。) ( 1 6 ) 口e r o ) 根据变量的正偏量和负偏量，可以得到变量的偏量值： 形= m 积形，时一- ) ( 1 7 ) 在求解q b f 公式时，s p 方法可以为求解提供全局信息，该信息可用于估计每个变 量在所有解中的统计特性，进而指导d p l l 过程的分支选择。在选择分支的过程中，首 先根据q b f 公式的量词层按照从小到大的顺序选择变量。对于同一量词层的变量，通 过调用s p 过程可以得到变量的正偏量即+ ，和负偏量形。根据偏量值，可以将变量分为 三类：偏向变量( 彬t + ，l 或形c ，1 ) 、平衡变量( 形一形t 一，并且形t 。，很小) 、约束不足变量 ( 刃。，1 ) 。由于选择平衡变量会改变问题的解簇的结构，损失大量解簇，约束不足变量 东北师范大学硕士学位论文 不能提供足够的求解信息，因此选择已经“冻结”的偏向变量作为待分支的变量，即那 些具有最大i 研- 彬i 值的变量。根据约束变量的量词不同，对变量赋值方式也不同。如 果约束当前分支变量的量词是存在量词，首先考察将变量赋值为其偏向值的分支，这是 因为对于存在变量只要与或树的一个分支是可满足的就可以保证原公式可满足，因此应 该选择有较多的满足解的子空间；如果约束当前分支变量的量词是全称量词，因为这时 只有当该变量对应节点的两个分支都是可满足的才可以保证原公式可满足，所以首先考 察将变量赋值为其偏向值的反的分支，如果该分支不可满足，就不需要继续考察另一个 分支。实验结果证明，上述方法可以显著提高d p l l 方法的求解效率。 东北师范大学硕士学位论文 第五章分支处理 在选择好待处理的q b f 子公式后，进入分支处理阶段。分支处理的目的在于判断 搜索树当前分支所对应的q b f 子公式的可满足性。在这一阶段采用了冲突推理，冲突 学习和满足蕴涵学习等技术对搜索空间剪枝，提高分支处理的效率。 5 1 冲突推理 在判断给定q b f 公式的可满足性前，先利用冲突推理技术对该公式进行化简。这 一过程主要采取单文字规则和冲突规则。 定义4 ( 单元子句) 给定一个q b f 公式产q 1 蜀g 恧且x l ，加) ，c 为f 中的子句， 称c 是一个单元子句当且仅当： ( 1 ) c 中有且仅有一个存在文字，； ( 2 ) c 中所有全称文字的量词层都大于z 的量词层。 其中，称存在文字，为单元文字。 定义5 ( 单元文字规则) 如果q b f 公式f 中存在单元文字，则将，赋值为真得到一个 新公式f 。 给定q b f 公式f ，c 为单元子句，若，为c 中的单元文字，显然在所有使c 为真的赋 值中，的真值都应该为真，因此可以得到如下结论： 命题6 给定q b f 公式f ，设，为在趾应用单元文字规则得到的新q b f 公式集合， 则阿满足当且仅当f 可满足。 定义7 ( 赋值冲突) 给定一个q b f 公式户q l 蜀级撼段x l ，x 。) ，c 为f 中的子句， 如果在赋值过程中c 满足： ( 1 ) c 中所有存在文字的赋值都为假； ( 2 ) c 中所有全称文字的赋值都不为真。 这时称f 出现赋值冲突，称c 为冲突子句。 定义8 ( 冲突规则) 给定一个q b f 公式户q l 蜀g 凰鳅l ，鳓) ，在赋值过程中， 如果当前分支存在冲突子句，则在该分支中环可满足。 东北师范大学硕士学位论文 在应用单元文字规则和冲突规则后，需要根据推理的结果做进一步的处理。当推理 的结果是c o n n i c t 时，表示当前分支不可满足，需要进行冲突学习，具体内容在5 2 节 中讨论，当推理结果为s a t i s f a c t i o n ，表示当前分支可以满足，需要进行满足蕴涵学习， 具体内容在5 3 节中讨论。 5 2 冲突学习 如果当前d p l l 分支出现冲突，这就表明当前分支下的子q b f 公式是不可满足的。 这时可以进行冲突学习，冲突学习的主要目的是记录当前存在的冲突分支。这样，当随 后的搜索过程中遇到同样的情况，就可以不用继续搜索而直接判断当前的搜索分支是不 可满足的。冲突学习主要是由冲突分析过程实现的，图5 1 给出了该过程的算法框架。 r o u t i n ea n a l y z e _ _ c o n n i c t ( ) j c o n n i c t c l = f i n d _ c o n f l i c l c l a u s e ( x 2 n e w c l = g e n e r a t e - c l a u s e ( c o n l l i c l c l ) ； 3 a d d _ c l a u s e ( n e w 1 ) ； 4 证( d l 【n e 、 ：9 1 ) o ) 5 t h e nb a c k t r a c k ( d l ( n e 矾l - c 1 ) ) ； 6 e n d 图5 1 冲突分析子过程 冲突分析过程首先判断当前q b f 公式是否存在冲突子句( 巧n d o n f l i c t i n g _ c l a u s e ( ) ) ， 如果存在则利用g e n e r a t e l a u s e ( ) 过程生成新的学习子旬( n e 、v _ c 1 ) 。在生成新子句过程 中，可以保证生成的新子句为单元子句，这样只要将对应的变量赋为原赋值相反的值， 就可以保证搜索沿着一个新的空间进行。将生成的新子句加入到数据库中 ( a d d l a u s e ( ) ) ，这样在下次搜索到同样的分支时就不需要继续向下搜索。 5 3 满足蕴涵学习 如果当前d p l l 分支为可满足，这时进行满足蕴涵学习。满足蕴涵学习的主要目的 是记录当前存在的满足分支。这样，当随后的搜索过程中遇到同样的情况，也可以不用 继续搜索而直接判断当前的搜索分支是可满足的，进而直接搜索全称变量的另一个分 支。图5 2 给出了满足蕴涵学习的主要过程。 东北师范大学硕士学位论文 r o u t i n e 锄a l y z e s a t ( ) j e m i t ) ，= f i n d - s a l e m i 够( ) ； 2 i f ( e n t i t y = n u l l ) 3 t h e ne m i 锣= g e n e r a t es a li n d u c e 畦一e n t i 妙( ) ； 4 i f ( ! t e m m a t e - - c o n d i t i o n ( e n t i 妙) ) 5 t h e nn e w e n = c o 舾e n s u s 乌e n e r a t e _ e m i 够( e m i t ) ，) ； 五 a d d - n e w e m n y ( n e w e n ) ； 7 i f ( d l ( n e w e n ) 0 ) 8 t h e nb a c l ( t r a c k ( d l ( n e w e n ) ) ； 9 e n d 图5 2 满足分析子过程 与冲突学习存储的单元子句不同，满足蕴涵学习存储的是单元短语( 即文字的合取) 。 定义9 ( 扩展的合取范式) 给定一个c n f 范式珧1 ，鳓) ， 扩展的合取范式e = 目x l ，鳓) ve lv 矾v v e m ，其中叫是短语。 定义1 0 ( 单元短语) 给定一个以扩展合取范式表示的q b f 公式卢q l 蜀酝忍 ( 如l ，砧v 跳v 跳v v 刷) ，设矾( 1 f 朋) 为，中的短语，称e m 是一个单元短语 当且仅当： ( 1 ) 矾中有且仅有一个全称文字z ； ( 2 ) 腻中所有存在文字的量词层都大于，的量词层。 满足蕴涵过程首先判断当前公式是否存在满足实体( f i n d a l e n “t ) ，( ) ) ，如果存在， 子过程执行第4 行，根据当前的赋值生成相应的短语( g e n e r a t e a i - i n d u c e d j m i 妙( ) ) 。根 据得到的短语反复进行实体学习过程( c o n s e n s u s _ g e n e r a t 9 - e n t 时( ) ) ，直到生成新的单元短 语，并存储学习到的短语( a d d j e w e n t i t ) r ( ) ) ，这样在下次搜索到同样的分支时就可以直 接判断该分支是可满足的。 东北师范大学硕士学位论文 第六章实验比较 我们在l i n u ) 【环境下用c + + 语言实现了q b f 问题求解器s p q b f 系统，其基本的算 法即s p q b f 算法如图3 2 所示。为了比较q b f 求解器的求解效率，我们在有关q b f 问题研究网站上下载了目前公认求解效率最高的几个q b f 求解器，如：2 c l s q 、s q b f 、 q u b e r e l l 3 等。所有的实验在一台d e l lp o w e r e d g e2 6 5 0 上运行，实验的运行环境如 下，c p u ：2 术l m e lx e o n2 0 0 g h z ，内存：l g ，操作系统：r e d h a te s 3 o 。 6 1 d p l l 算法和s p q b f 算法比较 第一个实验主要考察第4 章中介绍的s u r v e yp r o p a g a t i o n 分支选择技术和第5 章中介 绍的冲突学习等分支处理技术在加速d p l l 算法效率中的作用。在该实验中所有的问题 实例都是由著名的g e n t & w a l s h 随机问题产生器生成的。表l 给出了具体的实验结果， 其中表中第一列中以l q b f ，2 q b 饼口3 q b 研头的问题实例分别对应为1 q b 桐题，2 q b f 问题， 3 q b 侗题，5 c n f 表示问题的每个子句的最大长度为5 ，1 6 0 v a r 表示最多有1 6 0 个变量， 2 5 6 0 c l 表示子句最大个数为2 5 6 0 个。我们用c + + 语言实现了图3 1 中介绍的基于d p l l 的o b f 求解算法，表中的第二列给出了该算法的实验结果。第三列是在d p l l 算法的基 础上融入分支处理技术后的实验结果，可以看到几乎在所有的问题上算法的效率都有4 倍以上的提高，对于一些问题( 如3 q b 仁5 c n 仁2 0 v 铲8 0 c 1 3 ) 甚至有l 0 0 0 倍以上的提高。第 四列给出了在d p l l 的基础上融入调查传播技术后的实验结果，可以看到这时在除了 2 q b 仁5 c n f 2 0 v 小8 0 c 1 0 问题和3 q b f 5 c n 2 0 v 褂8 0 c 1 1 外的几乎所有问题上，系统的效率 都有很大的提高。第五列为最终系统的实验结果，可以看到相对d p l l 算法，s p q b f 在 所有的问题上效率都有提高，对于很多问题甚至有1 0 5 规模以上的加速。上述实验说明， 基于s u r v e yp r o p a g a t i o n 的分支选择技术和冲突学习等分支处理方法在提高d p l l 算法的 效率方面有着显著的效果。 表ls p q b f 与d p l l 在随机问题中的实验比较 ( 时间单位是秒，“一”表示在1 2 0 0 秒内执行失败的求解器) d p l l + p r o b l e md p l ld p l l + s p s p q b f l e a r n i n g 1 q b f 5 c 罅1 6 0 v 小2 5 6 0 c 1 0 2 9 3 0 86 5 2 70 1 5o 0 8 1q b f 5 c n f16 0 v 孙2 5 6 0 c 1 16 4 9 0 41 5 61 0 10 8 6 1q b 乒5 c n fl6 0 v 扑2 5 6 0 c 1 21 0 1 4 5 22 5 5 60 0 80 0 4 l q b 仁5 c n 1 6 0 v 褂2 5 6 0 c 1 3 1 7 6 4 l0 0 9o 1 3 1q b f 5 c n fl6 0 v 小2 5 6 0 c 1 41 1 1 5o 4 51 7 60 9 4 2 i 东北师范大学硕士学位论文 lq b f 5 c n bl6 0 v 小2 5 6 0 c 1 50 7 o 3 7 1 q b f 5 c n f l 6 0 v 扑2 5 6 0 c 1 6 9 0 4 4 36 2 2o 1 2o 0 6 lq b f 5 c n 鼻16 0 v a r - 2 5 6 0 c 1 72 5 0 6 31 2 70 0 4o 0 2 l q b f 5 c n f l 6 0 v 孙2 5 6 0 c 1 8 3 7 4 4 16 8 8 41 1 8 71 2 0 6 1 q b 矗5 c n 1 6 0 v 扑2 5 6 0 c i 9 7 1 90 7 33 8 25 9 2 q b 5 c n 2 0 v 小8 0 c 1 o 8 2 71 3 4 31 0 5 8 8 0 9 2 q b 5 c n 2 0 v 褂8 0 c 1 1 2 7 51 3 82 1 71 7 2 2 q b 5 c n f 2 0 v 孙8 0 c 1 2 4 4 78 2 81 5 31 2 3 2 q b f _ 5 c n f - 2 0 v a 卜8 0 c 1 3 3 1 6 8o 6 5o 5 1 2 q b f 5 c n f 2 0 v 孙8 0 c 1 4 11 23 1 12 2 11 8 5 2 q b 5 c n f 2 0 v 孙8 0 c 1 5 4 9 2o 8 62 4 11 8 9 3 q b 矗5 c n 仁2 0 v 小8 0 c 1 0 5 8 1 4 65 4 2 74 2 2 6 3 q b f - 5 c n 2 0 v 小8 0 c 1 1 2 2 7 5 28 5 22 6 5 6 51 6 3 0 8 3 q b f 5 c n 2 0 v 小8 0 c 1 2 1 0 0 7 7 86 3 6 8 28 4 7 0 8 6 2 9 6 6 3 q b f 5 c n f 2 0 v a 卜8 0 c 1 3 9 5 5 50 2 23 5 74 9 2 3 q b f 5 c n f - 2 0 v 孙8 0 c 1 4 9 0 8 3 53 4 9 5 13 5 4 2 4 3 q b f - 5 c n f - 2 0 v 小8 0 c 1 5 5 9 7 4 l4 3 4 53 2 1 8 6 2s p q b f 和参赛q b f 求解器效率比较 2 c l s q 、s q b f 、q u b e r e l l 3 是目前公认的几个求解效率最高的q b f 问题求解器， 第二个实验是将s p q b f 系统和上述求解器比较。实验的测试用例包括由g e m & w a l s h 随机问题产生器生成的随机问题和在q b f l i b 上下载的一些标准测试问题。 表2 随机q b f 问题的求解效果列表 s o l v e r 2 c l s qs q b fq u b e r e l l 3s p q b f 1q b 5 c n f - 16 0 v 小2 5 6 0 c 1 02 0 6 90 0 8 lq b f 5 c n f16 0 v 小2 5 6 0 c i 19 7 1 40 8 6 1q b f 5 c n 16 0 v 褂2 5 6 0 c 1 2o 9 4o 0 4 lq b f 5 c n f - 16 0 v 小2 5 6 0 c 1 34 3 2 52 8 9 3o 1 3 1q b 二5 c n f16 0 v 小2 5 6 0 c l f 41 5 3 35 7 2 20 9 4 lq b f 5 c n f16 0 v 小2 5 6 0 c 1 54 6 5 70 - 3 7 lq b f - 5 c n f - l6 0 v 小2 5 6 0 c 1 61 4 9 3 22 73 3 8 2o 0 6 1q b 仁5 c n f - l6 0 v 小2 5 6 0 c 1 72 2 9 17 2 0 93 6 0 10 0 2 1 q b f 5 c n f 1 6 0 v 小2 5 6 0 c 1 8 1 2 0 2 5 0 7 8 1 2 0 6 1 q b f 5 c n f1 6 0 v 孙2 5 6 0 c 1 9 2 5 3 0 16 9 4 8 41 2 3 9 75 9 2 q b f 5 c n f - 16 0 v 护51 2 0 c 1 0 o 0 80 0 40 2 q b f 5 c n 16 0 v 小5 1 2 0 c 1 10 0 5 o 0 5 0 0 1 2 q b f 5 c n 0 l6 0 v 冰5l2 0 c 1 20 0 80 0 70 2 q b f 5 c n 仁16 0 v 孙5 l2 0 c 1 3o 0 70 0 5o o l 2 q b f 5 c n f l6 0 v 小512 0 c l - 40 0 50 0 4o 东北师范大学硕士学位论文 2 q b f 5 c n l6 0 v 小512 0 c 1 5 0 0 60 0 40 2 q b f 5 c n f l6 0 v a r - 5l2 0 c 1 6 o 0 70 0 30 2 q b f 5 c n f 16 0 v 铲5l2 0 c 1 7o 0 5 o 0 40 0 l 2 q b f 5 c n l6 0 v 褂5l2 0 c 1 8 o 0 9 o 0 4 o 2 q b f 5 c n 1 6 0 v 小5 1 2 0 c 1 90 0 7o 0 4o 表2 给出了上述4 个系统在随机问题中的表现。从表中可以清楚的看出，只有 q u b e r e l l 3 和s p q b f 能够求解所有问题。除了在1 q b 5 c n 1 6 0 v a 卜2 5 6 0 c 1 8 问题中 s p q b f 差于q u b e r e l l 3 外，在其它的大部分问题中，s p q b f 的表现要远优于其它三个 求解器。这是因为对于大部分随机问题，由于s p 方法能较早确定具有偏向性的变量， 从而使得问题能够快速的解决。 表3m i s c e l l a j l e a 域中的i m p l 问题的求解效果列表 s o l v e r 2 c l s qs q b fq u b e r e l l 3s p q b f i m p l 0 2 oooo i m p l 0 4 oooo i m p l 0 6 o o l00o i m p l 0 8 0 0 400o i m p l l o o 1 20o o i m p l l 2 o 4 500o i m p l l 4 2 0 9000 i m p l l 6 2 7 8 8 0 。o0 表3 给出了上述4 个系统在m i s c e l l a n e a 域中的i m p l 问题中的实验比对，可以看出 除了2 c 1 s q 外，其它三个系统都能够很快的解决上述问题。 表4 p l a n n i n g 域中的e v - p r 问题的求解效果列表 s o l v e r 2 c l s qs q b f q u b e r e l l 3s p q b f e v - p r - 4 x 4 5 - 3 - 0 - 0 1 - l g 1 5 51 0 61 2 2 e v - p r _ 4 x 4 7 - 3 0 - 0 1 一l g 3 6 4 8 3 4 38 6 7 21 1 0 6 e v - p 卜4 x 4 9 3 - 0 - o - l l g 5 4 7 4 55 7 91 1 7 0 8 表4 给出了四个求解器对p l 锄i n g 域中的e v - p r 问题求解的测试结果。从表中可以 看出s p q b f 要明显好于2 c l s q 和q u b e r e l l _ 3 ，但略差于s q b f 。 表5m i s c e l l 卸e a 域中的l 凹h _ p 问题的求解效果列表 s o l v e r 2 c l s qs q b fq u b e r e l l 3s p q b f k - p h - p - l oo0 k p h - p - 2 0 0 1o00 k - p h p 一3 0 o l 0 0 1o0 东北师范大学硕士学位论文 k p h p - 4 0 0 20 0 7o 0 20 0 l k - p h - p - 5 o 0 9l 。0 40 1 70 1 3 k p h - p 一6 o 7 34 1 51 2 9o 4 5 k p h p 一7 5 1 72 7 5 59 4 03 1 k - p h - p - 8 7 6 5 26 5 3 0 42 0 6 。5 71 6 。7 8 k p h p 一9 1 0 8 0 4 58 4 5 2 表5 给出了四个q b f 求解器对m i s c e i l a n e a 域中的i 凹h 问题求解的测试结果。 从表中可以看出s p q b f 要明显好于其它三个求解器。在有些问题上s p q b f 甚至有1 0 倍以上的加速。 表6f o r m a lv e r i f i c a t i o n 域中的c o u m e r 问题的求解效果列表 s o l v e r 2 c l s qs q b fq u b e r e l l 3s p q b f c n t o l000o c n t 0 20 0 l00 0 lo c n t 0 30 1 3o 0 50 ，0 2 0 0 1 c n t 0 41 1 8 1o 0 70 4 90 0 4 c n t 0 50 2 l2 8 7 12 2 2 c n t 0 61 2 70 9 8 c n t 0 7 0 8 9 1 1 5 5 c n t 0 83 4 67 9 9 6 c m 0 93 4 3 43 4 8 7 4 c m l 0 4 3 6 42 3 7 8 6 表6 给出了四个q b f 求解器对f o m a lv e r i f i c a t i o n 域中的c o u m e r 问题求解的测试 结果。从表中可以看出，只有s p q b f 和s q b f 可以求解上述问题，其中s p q b f 要明显 好于2 c l s q 和q u b e r e l l 3 ，有些问题的求解速度甚至提高了近3 0 0 倍，但略差于s q b f 。 综合上述两个实验不难看出，由于在分支选择中利用了s u n ，e yp r o p a g a t i o n 方法， 在分支处理时利用了冲突学习等技术，s p q b f 不仅比原有的基于d p l l 方法的q b f 求 解算法在效率上有了很大提高，相对于目前最好q b f 求解器，同样具有竞争力。需要 指出的是，在利用s u r v e yp r o p a g a t i o n 方法确定d p l l 分支时，步长对调查传播算法有 着很大的影响，这主要体现在两个方面：( 1 ) 算法的效率；( 2 ) 算法的有效性。z e c c h i n a 等就指出在求解s a t 问题时随着步长的递增，调查传播算法的时间耗费快速递减，并 且趋于平缓，同时，随着步长的递增，调查传播算法的有效性快速递减。我们在求解 q b f 问题时发现步长对系统的求解效率也有很大的影响，这主要体现在s p 算法提供信 息的量和信息的效率两方面。在上述实验中，我们经过效率比对，将步长统一设置为 3 0 。事实上，如何确定步长的大小对于我们依然是一个悬而未决的问题，在此，我们将 之留为一个开放式问题。 东北师范大学硕士学位论文 第七章总结 目前大多数q b f 问题求解器都是在扩展原有的s a t 问题求解器的基础上设计的， 例如g e n t 等人设计的q b f 求解器w a j k q s a t 在启发式设计中，利用了s a t 问题求解 器w a l k s a t 的启发式方法；i 沁w l e y 等人设计的q b f 求解器w a t c h e d c s b j 使用的数据 结构是通过扩展s a t 求解器z c h a f r 中的监视文字这种放松的数据结构而得到的； g i u n c h i g l i a 等人设计的q b f 求解器q u b e 所使用的算法是通过扩展s a t 求解算法d p l l 获得的，它所使用的数据结构和w a t c h e d c s b j 一样是通过扩展s a t 求解器z c h a f l f 中所使用的监视文字这种放松的数据结构而得到的，它使用的子句学习技术也参考了 z c h a 行中