一种基于扩展规则的#SAT求解系统  

Solving #SAT Using Extension Rules

作　　者：殷明浩[1,2,3] 林海[1,2] 孙吉贵[1,2] 

机构地区：[1]吉林大学计算机科学与技术学院,吉林长春130012 [2]吉林大学符号计算与知识工程教育部重点实验室,吉林长春130012 [3]东北师范大学计算机学院,吉林长春130117

出　　处：《软件学报》2009年第7期1714-1725,共12页Journal of Software

基　　金：国家自然科学基金Nos.60573067,60773097;国家高等学校博士学科点专项科研基金No.20050183065;东北师范大学青年基金No.20070601~~

摘　　要：#SAT问题是SAT问题的扩展,需要计算出给定命题公式集合的模型个数.通过将问题求解沿着归结的反方向进行,并利用容斥原理解决由此带来的空间复杂性问题,提出了一种基于扩展规则的模型计数和加权模型计数问题求解框架,可以看作是目前所有模型计数问题求解方法的一种补方法.证明了该方法的完备性和有效性,设计了基于扩展规则的#SAT求解系统:JLU-ERWMC.实验结果表明,JLU-ERWMC在有些问题中优于目前最为高效的#SAT问题求解系统.#SAT problem is the extension of SAT problem. It involves counting models of a given set of proposition formulae. By using the inverse of resolution and the inclusion-exclusion principle to circumvent the problem of space complexity, this paper proposes a framework for both model counting and weighted model counting. It suggests a complementary method for current model counting methods. These methods are proved to be sound and complete. A model counting system, namely JLU-ERWMC, is built based on these methods. JLU-ERWMC outperforms the most efficient model counting methods in some cases.

关 键 词：扩展规则 模型计数 知识编译 加权模型计数 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]