基于扩展规则的模型计数方法研究

发布时间：2017-04-06 09:01

  本文关键词：基于扩展规则的模型计数方法研究，由笔耕文化传播整理发布。

【摘要】：早在二十世纪五十年代,智能规划一经提出便成为了人工智能领域中的一个前沿研究领域,自此,随着国内外诸多研究学者们不懈努力,在该领域的研究成果方面取得了突破性的进展。目前求解该问题存在着许多种方法,其中一种较为高效的求解方法则是将规划问题编译为命题可满足性问题(SAT问题),然后利用SAT求解器进行求解。有时此种间接求解的方法会比直接求解的方法更为高效快捷,目前已成为求解智能规划问题的主流方法之一。在1971年,Cook等人证明SAT问题是NP完全的。事实上,许多NP问题都可以转为SAT问题进行求解。然而,在人工智能研究领域还有许多经典问题的计算复杂度是高于NP的,对于这些问题的求解仅仅判断给定命题公式是否可满足是不够的,还需要知道问题模型的个数。由此扩展出了模型计数问题(#SAT问题)。如贝叶斯网络推理,概率规划问题等都可以转化成#SAT问题进行求解。因此,如何高效地求解#SAT问题,对人工智能的很多领域都有重要意义。目前,求解#SAT问题的算法可以分为精确求解和近似求解两种。精确算法可以保证计算出给定命题公式的准确模型个数;而近似算法只能计算出给定公式模型的近似个数。在精确求解的算法中主要有基于DPLL(Davis Putnam Logemann and Loveland)的方法和基于扩展规则的方法。这两种方法是互补的求解方法。一般情况下,当互补因子较高时,基于扩展规则的求解方法要优于基于DPLL求解方法;反之,当互补因子较低时,要差于基于DPLL求解方法。本文在对基于扩展规则的模型计数求解方法CER深入研究的基础上,从不同角度对其进行改进,提出了两种更为高效的求解方法:(1)结合扩展规则重构的#SAT问题增量求解方法:对CER中的重要计算公式进行重构,并证明了重构的正确性;给出了极大项相交集和扩展极大项相交集的定义,并提出结合两者关系复用极大项相交集求解结果的增量计算方法,还删减了所有广义互补子句集对应的扩展极大项相交集,有效避免了许多冗余计算;给出用互补表记录子句间互补关系的方法,提出一种对极大项相交集的基础子句集进行增量判定互补的方法,很好地避免了在判定子句间及基础子句集互补性时的大量冗余计算。实验结果表明:与CER方法相比,RCER方法效率更高,尤其是互补因子较低的情况下。(2)结合互补度的基于扩展规则#SAT问题求解方法:在计算给定子句集的模型个数时,利用SE-Tree(set enumeration tree)形式化地表达计算过程,逐步生成需要计算的子句集合。并在SE-Tree中添加终止结点,避免大部分含互补文字子句集合的生成,且不会因剪枝而导致求解不完备。提出互补度的概念,在扩展SE-Tree结点时按照互补度由大到小的顺序扩展,较早地生成含互补文字且长度较小的子句集合,有效减少枚举树生成的结点个数,进而减少对子句集合判断是否含互补文字的计算次数。实验结果表明,与CER方法相比该方法效率较好,且进一步改进了CER方法在互补因子较低时求解效率低下的不足。以上两种方法从不同角度对CER方法进行了改进,并取得了较好的效果。两种方法分别利用了CER方法中重要公式的计算项间的关系和计算顺序减少了求解过程中的冗余计算,从而达到提高效率的目的。
【关键词】：智能规划 命题可满足性问题 模型计数 扩展规则 增量方法
【学位授予单位】：吉林大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：TP18
【目录】：

• 摘要4-6
• Abstract6-10
• 第1章 绪论10-16
• 1.1 研究背景和意义10-12
• 1.2 研究现状12-13
• 1.3 本文工作13-16
• 第2章 模型计数问题16-31
• 2.1 算法的复杂度16-17
• 2.2 SAT问题17-19
• 2.3 SAT问题求解方法19-24
• 2.4 #SAT问题24-26
• 2.5 #SAT问题求解方法26-31
• 第3章 基于扩展规则的#SAT问题求解方法31-39
• 3.1 扩展规则31-33
• 3.2 CER算法33-37
• 3.3 本章小结37-39
• 第4章 结合扩展规则重构的#SAT问题增量求解方法39-51
• 4.1 公式重构39-44
• 4.2 极大项相交集增量计算方法44-46
• 4.3 互补表增量判定方法46-47
• 4.4 实验结果与分析47-51
• 第5章 结合互补度的基于扩展规则#SAT问题求解方法51-58
• 5.1 互补度51-52
• 5.2 集合枚举树52-53
• 5.3 CDCER算法53-56
• 5.4 实验结果与分析56-58
• 第6章 总结与展望58-61
• 6.1 工作总结58-59
• 6.2 展望59-61
• 参考文献61-66
• 作者简介及在学期间所取得的科研成果66-67
• 致谢67

【相似文献】

中国期刊全文数据库 前10条

1 徐东霞,陈为民,陈卫,陈雍乐;凸轮轴测量中计数方法的研究[J];微计算机应用;2003年03期

2 陈本永,吴晓维,李达成;一种新型的干涉条纹软件计数方法及其实现研究[J];传感技术学报;2004年03期

3 于杰;肖国强;代毅;;粘连蚕卵计数方法的研究[J];计算机工程与应用;2011年08期

4 孙洋;;视频中行人快速检测计数方法研究[J];数字技术与应用;2013年11期

5 朱亚华;;悬浮细胞图像的计数方法研究[J];佳木斯大学学报(自然科学版);2010年01期

6 赵斌,侯金龙;外差干涉信号的一种相位计数方法[J];华东交通大学学报;2003年02期

7 邹应国;康宜华;;成捆钢筋快速计数方法的研究[J];机床与液压;2006年02期

8 ;其它测量[J];电子科技文摘;1999年11期

9 杨慧赞;林勇;唐章生;张永德;陈忠;黄姻;甘西;;基于图像处理的鱼卵计数方法研究[J];水生态学杂志;2011年05期

10 王晓城,高小榕;基于混合隐Markov模型的红细胞计数方法[J];清华大学学报(自然科学版);2004年06期

中国重要会议论文全文数据库 前3条

1 王彦敏;林小竹;杜天苍;田瑞卿;;基于watershed变换的粘连物体的分割和计数方法[A];第十二届全国图象图形学学术会议论文集[C];2005年

2 钟新玉;刘峡壁;魏雪;曹月;;融合视频与激光信息的双向人流计数方法[A];全国第22届计算机技术与应用学术会议(CACIS·2011)暨全国第3届安全关键技术与应用（SCA·2011）学术会议论文摘要集[C];2011年

3 冯爱平;;基于种子搜索法的金属棒材计数方法研究[A];2010年西南三省一市自动化与仪器仪表学术年会论文集[C];2010年

中国重要报纸全文数据库 前1条

1 记者 邓晖;清华简《算表》或为“九九”表延伸[N];光明日报;2014年

中国硕士学位论文全文数据库 前9条

1 贾凤雨;基于扩展规则的模型计数方法研究[D];吉林大学;2016年

2 高静伟;通济桥高密度人群计数方法研究与实现[D];中山大学;2013年

3 辛海涛;基于运动目标检测的行人计数方法[D];河北工业大学;2011年

4 李姝霖;智能监控系统中行人计数方法的研究与实现[D];西安电子科技大学;2011年

5 刘向东;高密度人群计数方法的研究与应用[D];浙江工业大学;2012年

6 唐亮;一种新的发光二极管自动精确计数方法[D];复旦大学;2012年

7 黄奕国;基于Flow Mosaicking的视频行人计数方法研究[D];中山大学;2013年

8 雷波;基于数字图像处理的卡片计数方法研究[D];华中科技大学;2013年

9 于杰;粘连物体计数方法研究[D];西南大学;2011年

  本文关键词：基于扩展规则的模型计数方法研究，，由笔耕文化传播整理发布。

本文编号：288580