基于格局检测的模型计数方法
作者:
作者单位:

作者简介:

贺甫霖(1993-),男,吉林省吉林市人,硕士,主要研究领域为人工智能,自动推理;牛当当(1990-),男,博士,讲师,CCF专业会员,主要研究领域为人工智能,自动推理,抽象论辩;刘磊(1960-),男,教授,博士生导师,CCF专业会员,主要研究领域为软件理论与技术;王强(1994-),男,硕士,主要研究领域为人工智能,自动推理,机器学习;吕帅(1981-),男,博士,副教授,博士生导师,CCF高级会员,主要研究领域为人工智能,智能规划,机器学习,自动推理.

通讯作者:

吕帅,E-mail:lus@jlu.edu.cn

中图分类号:

TP18

基金项目:

国家自然科学基金(61300049,61763003);吉林省自然科学基金(20180101053JC)


Model Counting Methods Based on Configuration Checking
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61300049, 61763003); Natural Science Research Foundation of Jilin Province (20180101053JC)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    模型计数是指求出给定命题公式的模型数,是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.

    参考文献
    相似文献
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2017-11-06
  • 最后修改日期:2018-05-29
  • 录用日期:
  • 在线发布日期: 2020-02-17
  • 出版日期: 2020-02-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号