结合扩展规则重构的#SAT问题增量求解方法
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金(61272208,61133011,61402196,61003101,61170092);国家教育部博士点专项基金(20100061110031);中国博士后科学基金(2013M541302);吉林省科技发展计划(20101501,20140520067JH)


Reconstructive Algorithm Based on Extension Rule for Solving #SAT Incrementally
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61272208, 61133011, 61402196, 61003101, 61170092); Doctoral Fund of Ministry of Education of China (20100061110031); China Postdoctoral Science Foundation (2013M541302); Jilin Province Science and Technology Development Plan (20101501, 20140520067JH)

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

    #SAT问题是人工智能中的重要问题,在人工智能领域被广泛应用.在对基于扩展规则的模型计数求解方法CER深入研究的基础上,重构CER中使用的计算公式,并对其正确性进行了证明;提出极大项相交集和扩展极大项相交集的概念,并给出根据两者关系重用极大项相交集计算结果的增量求解方法,且对广义互补子句集对应的所有扩展极大项相交集进行剪枝,有效避免了计算所有极大项相交集对应极大项个数时的冗余求解;提出构建记录子句间互补关系的互补表方法,给出重用极大项相交集基础子句集互补结果的增量互补判定方法,较好地避免了判断子句间和各极大项相交集的基础子句集互补关系时的重复计算.实验结果表明:RCER方法易于实现,扩展性强,比CER方法效率更高,尤其是在互补因子较低时,效率提升更为显著.

    Abstract:

    #SAT problem is an important problem and used widely in the field of artificial intelligence. By the in-depth study of model counting algorithm CER based on extension rule, the calculation formula used in CER is reconstructed and its correctness is proved in this paper. Then, the concepts of maximum term intersection and extended maximum term intersection are put forward. An incremental method for #SAT is also proposed, and the extended maximum term intersections are computed preferentially based on the solution of the maximum term intersection. Pruning is performed on the extended maximum term intersections corresponding to the generalized complementary base clause sets to avoid the redundant calculation. A method is provided to decide if a clause set is generalized complementary or not by creating a complementary table for recording the complementarity of all pairs of clauses. Using this complementary table, the base clause set of extended maximum term intersection can be decided incrementally. Based on this method, the redundant calculation for deciding the complementarity of clauses and clause sets is avoided better. Experimental results show that the presented RCER algorithm runs faster than CER algorithm, especially in the instances where complementary factor is small.

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

贾凤雨,欧阳丹彤,张立明,刘思光.结合扩展规则重构的#SAT问题增量求解方法.软件学报,2015,26(12):3117-3129

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

京公网安备 11040202500063号