可满足问题中的模型计数  

The model counting of a satisfiability problem

作　　者：谷文祥[1] 朱磊[1] 黄平[1] 殷明浩[1] 

机构地区：[1]东北师范大学计算机科学与信息技术学院,吉林长春130117

出　　处：《智能系统学报》2012年第1期33-39,共7页CAAI Transactions on Intelligent Systems

基　　金：国家自然科学基金资助项目(61070084;60573067;60803102)

摘　　要：模型计数问题是指计算给定问题的解的个数,这是一类比决策更困难的问题,也是人工智能领域研究的一个热点问题.对模型计数问题的研究不仅可以提高算法的求解效率,更能促进对问题困难本质的了解.以可满足问题(命题可满足(SAT)和约束可满足问题(CSP))为例,从精确算法和近似求解两方面综述了模型计数问题的研究现状,重点介绍了相关概念以及各个算法之间的优缺点,并提出了有待解决的开放性问题,对模型计数问题的研究予以了总结和展望.A model counting problem refers to computing the number of solutions for a given problem which is harder than the decision-making problem.Model counting problems are also a hot topic in the field of artificial intelligence.Research on model counting problems can not only improve the efficiency of an algorithm,but also enhance the understanding of the nature of hard problems.Taking a satisfiability problem in propositional logic,known as an SAT,and a constraint satisfaction problem（CSP） as an example,a model counting problem was reviewed from two aspects： an exact algorithm and approximate algorithm.For each aspect,the development and related concepts along with the advantages and disadvantages were emphasized.Moreover,this paper proposed some unsolved questions of the model counting and gave a summary and outlook of the research on model counting.

关 键 词：人工智能 约束可满足问题 命题可满足问题 模型计数 

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