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

《基于扩展规则的模型计数方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号：TP31单位代码：10183研究生学号：2013532035密级：公开吉林大学硕士学位论文基于扩展规则的模型计数方法研究ResearchofAlgorithmBasedonExtensionRuleforModelCounting作者姓名：贾凤雨专业：计算机软件与理论研究方向：可满足性问题求解指导教师：欧阳丹彤培养单位：吉林大学计算机科学与技术学院2016年4月基于扩展规则的模型计数方法研究Ｒｅ巧ａｒｃｈｏｆＡｌｏｒｉｔｈｍＢａｓｅｄｏｎＥｘｔｅｎｓｉｏｎＲｕｌｅｆｏｒＭｏｄｅｌｇＣｏｕｎｔｉｎｇ作者姓名；贾

2、凤雨专业名称；计算机软件与理论指导教师：欧阳丹形教授学位类别；工学硕±答辩日期：年１月＞王日未经本论文作者的书面授权，依法收存和保管本论文书面版本、电子版本的任何单位和个人，均不得对本论文的全部或部分内容进行任何形式的复制、修改、发行、出租、改编等有碍作者著作权的商业性使用（但纯学术性使用不在此限）。否则，应承担侵权的法律责任。吉林大学硕古学位论文原创性声明本人郑重声明：所呈交学位论文，是本人在指导教师的指导下，独立进行研巧工作所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人

3、或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体，均己在文中明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文作者签名：日期；年Ｊｒ月班日摘要摘要基于扩展规则的模型计数方法研究早在二十世纪五十年代，智能规划一经提出便成为了人工智能领域中的一个前沿研究领域，自此，随着国内外诸多研究学者们不懈努力，在该领域的研究成果方面取得了突破性的进展。目前求解该问题存在着许多种方法，其中一种较为高效的求解方法则是将规划问题编译为命题可满足性问题(SAT问题)，然后利用SAT求解器进行求解。有时此种间接求解

4、的方法会比直接求解的方法更为高效快捷，目前已成为求解智能规划问题的主流方法之一。在1971年，Cook等人证明SAT问题是NP完全的。事实上，许多NP问题都可以转为SAT问题进行求解。然而，在人工智能研究领域还有许多经典问题的计算复杂度是高于NP的，对于这些问题的求解仅仅判断给定命题公式是否可满足是不够的，还需要知道问题模型的个数。由此扩展出了模型计数问题(#SAT问题)。如贝叶斯网络推理，概率规划问题等都可以转化成#SAT问题进行求解。因此，如何高效地求解#SAT问题，对人工智能的很多领域都有重要意义。目前，求解#SAT问题的算法可以分为精确

5、求解和近似求解两种。精确算法可以保证计算出给定命题公式的准确模型个数；而近似算法只能计算出给定公式模型的近似个数。在精确求解的算法中主要有基于DPLL(DavisPutnamLogemannandLoveland)的方法和基于扩展规则的方法。这两种方法是互补的求解方法。一般情况下，当互补因子较高时，基于扩展规则的求解方法要优于基于DPLL求解方法；反之，当互补因子较低时，要差于基于DPLL求解方法。本文在对基于扩展规则的模型计数求解方法CER深入研究的基础上，从不同角度对其进行改进，提出了两种更为高效的求解方法：(1)结合扩展规则重构的#SAT

6、问题增量求解方法：对CER中的重要计算公式进行重构，并证明了重构的正确性；给出了极大项相交集和扩展极大项相交集的定义，并提出结合两者关系复用极大项相交集求解结果的增量计算方法，还删减了所有广义互补子句集对应的扩展极大项相交集，有效避免了许多冗余计算；给出用互补表记录子句间互补关系的方法，提出一种对极大项相交集的基础子句集进行增量判定互补的方法，很好地避免了在判定子句间及基础子句集互补性时的大量冗余计算。实验结果表明：与CER方法相比，RCERI摘要方法效率更高，尤其是互补因子较低的情况下。(2)结合互补度的基于扩展规则#SAT问题求解方法：在计

7、算给定子句集的模型个数时，利用SE-Tree(setenumerationtree)形式化地表达计算过程，逐步生成需要计算的子句集合。并在SE-Tree中添加终止结点，避免大部分含互补文字子句集合的生成，且不会因剪枝而导致求解不完备。提出互补度的概念，在扩展SE-Tree结点时按照互补度由大到小的顺序扩展，较早地生成含互补文字且长度较小的子句集合，有效减少枚举树生成的结点个数，进而减少对子句集合判断是否含互补文字的计算次数。实验结果表明，与CER方法相比该方法效率较好，且进一步改进了CER方法在互补因子较低时求解效率低下的不足。以上两种方法从不

8、同角度对CER方法进行了改进，并取得了较好的效果。两种方法分别利用了CER方法中重要公式的计算项间的关系和计算顺序减少了求解过程中的冗余计算，从而达到