###
DOI:
Journal of Software:2009.20(7):1714-1725

一种基于扩展规则的#SAT 求解系统
殷明浩,林海,孙吉贵
(吉林大学 计算机科学与技术学院,吉林 长春 1300122;吉林大学 符号计算与知识工程教育部重点实验室,吉林 长春 130012;东北师范大学 计算机学院,吉林 长春 130117)
Solving #SAT Using Extension Rules
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 3600   Download 4393
Received:May 31, 2007    Revised:February 20, 2008
> 中文摘要: #SAT 问题是SAT 问题的扩展,需要计算出给定命题公式集合的模型个数.通过将问题求解沿着归结的反方向进行,并利用容斥原理解决由此带来的空间复杂性问题,提出了一种基于扩展规则的模型计数和加权模型计数问题求解框架,可以看作是目前所有模型计数问题求解方法的一种补方法.证明了该方法的完备性和有效性,设计了基于扩展规则的#SAT 求解系统:JLU-ERWMC.实验结果表明,JLU-ERWMC 在有些问题中优于目前最为高效的#SAT 问题求解系统.
Abstract:#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.
文章编号:     中图分类号:    文献标志码:
基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60573067, 60773097 (国家自然科学基金); the Specialized Research Fund for the Doctoral Program of Higher Education of China under Grant No.20050183065 (国家高等学校博士学科点专项科研基金); the Science Foundation for Young Teachers of Northeast Normal University of China under Grant No.20070601 (东北师范大学青年基金) Supported by the National Natural Science Foundation of China under Grant Nos.60573067, 60773097 (国家自然科学基金); the Specialized Research Fund for the Doctoral Program of Higher Education of China under Grant No.20050183065 (国家高等学校博士学科点专项科研基金); the Science Foundation for Young Teachers of Northeast Normal University of China under Grant No.20070601 (东北师范大学青年基金)
Foundation items:
Reference text:

殷明浩,林 海,孙吉贵.一种基于扩展规则的#SAT 求解系统.软件学报,2009,20(7):1714-1725

.Solving #SAT Using Extension Rules.Journal of Software,2009,20(7):1714-1725