###
Journal of Software:2020.31(2):395-405

基于格局检测的模型计数方法
贺甫霖,刘磊,吕帅,牛当当,王强
(吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012;吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012;西北农林科技大学 信息工程学院, 陕西 杨凌 712100)
Model Counting Methods Based on Configuration Checking
HE Fu-Lin,LIU Lei,Lü Shuai,NIU Dang-Dang,WANG Qiang
(College of Computer Science and Technology, Jilin University, Changchun 130012, China;Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun 130012, China;College of Computer Science and Technology, Jilin University, Changchun 130012, China;Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun 130012, China;College of Information Engineering, Northwest A&F University, Yangling 712100, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 83   Download 70
Received:November 06, 2017    Revised:May 29, 2018
> 中文摘要: 模型计数是指求出给定命题公式的模型数,是SAT问题的泛化.模型计数在人工智能领域取得了广泛应用,很多现实问题都可以规约为模型计数进行求解.目前,常用的模型计数求解器主要有Cachet与sharpSAT,它们均采用完备方法且具有高效的求解能力,但其求解效率对模型数不敏感.有理由猜测:当给定问题的模型较少时,不完备算法可能发挥其效率优势而更适合模型计数.局部搜索是求解SAT问题的高效不完备方法,Cai等人提出了格局检测策略,并将其应用到局部搜索方法中,提出了SWcc算法,具有很高的求解效率.对SWcc算法进行扩充,分别得到了迭代法与优化后的增量法两种效率较高的不完备模型计数方法,给出了两种方法的思路和具体实现.最后给出了大量测试样例的实验结果,以验证当给定合取范式的模型较少时,该迭代法与优化后的增量法的求解效率有所提升.
中文关键词: 模型计数  局部搜索  格局检测
Abstract:Model counting is the problem of calculating the number of the models of a given propositional formula, and it is a generalization of the SAT problem. Model counting is widely used in the field of artificial intelligence, and many practical problems can be reduced to model counting. At present, there are two complete solvers which are commonly used for model counting, i.e. Cachet and sharpSAT, both of which have high solving efficiency. But their solving efficiency does not relate to the numbers of the models. It is reasonable to suppose that incomplete methods are more likely to take their advantage in efficiency and maybe they could be more suitable to solve model counting problems when the number of the models of given propositional formula is little. Local search is an efficient incomplete method for solving SAT problem. A new strategy called configuration checking (CC) has been proposed by Cai et al. and it is adopted to the local search. In this way, the SWcc algorithm has been proposed with high solving efficiency. This study puts forward two incomplete methods on basis of the SWcc algorithm, i.e. the iteration method and the improved incremental method, both of which have high efficiency. Then, the specific implementation process of the two methods is presented. At last, the experimental results of a large amount of benchmarks, according to which is found, show the advantages of the iteration method and the improved incremental method in terms of time, when the amount of the models of given conjunctive normal formula is small.
文章编号:     中图分类号:TP18    文献标志码:
基金项目:国家自然科学基金(61300049,61763003);吉林省自然科学基金(20180101053JC) 国家自然科学基金(61300049,61763003);吉林省自然科学基金(20180101053JC)
Foundation items:National Natural Science Foundation of China (61300049, 61763003); Natural Science Research Foundation of Jilin Province (20180101053JC)
Reference text:

贺甫霖,刘磊,吕帅,牛当当,王强.基于格局检测的模型计数方法.软件学报,2020,31(2):395-405

HE Fu-Lin,LIU Lei,Lü Shuai,NIU Dang-Dang,WANG Qiang.Model Counting Methods Based on Configuration Checking.Journal of Software,2020,31(2):395-405