欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
#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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：