主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
贾凤雨,欧阳丹彤,张立明,刘思光.结合扩展规则重构的#SAT问题增量求解方法.软件学报,2015,26(12):3117-3129
结合扩展规则重构的#SAT问题增量求解方法
Reconstructive Algorithm Based on Extension Rule for Solving #SAT Incrementally
投稿时间:2014-12-04  修订日期:2015-02-15
DOI:10.13328/j.cnki.jos.004827
中文关键词:  扩展规则  模型计数  极大项相交集  互补表  增量方法
英文关键词:extension rule  model counting  maximum term intersection  complementary table  incremental method
基金项目:国家自然科学基金(61272208,61133011,61402196,61003101,61170092);国家教育部博士点专项基金(20100061110031);中国博士后科学基金(2013M541302);吉林省科技发展计划(20101501,20140520067JH)
作者单位E-mail
贾凤雨 吉林大学计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
 
欧阳丹彤 吉林大学计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
 
张立明 吉林大学计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
limingzhang@jlu.edu.cn 
刘思光 吉林大学计算机科学与技术学院, 吉林 长春 130012
符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012 
 
摘要点击次数: 1950
全文下载次数: 1766
中文摘要:
      #SAT问题是人工智能中的重要问题,在人工智能领域被广泛应用.在对基于扩展规则的模型计数求解方法CER深入研究的基础上,重构CER中使用的计算公式,并对其正确性进行了证明;提出极大项相交集和扩展极大项相交集的概念,并给出根据两者关系重用极大项相交集计算结果的增量求解方法,且对广义互补子句集对应的所有扩展极大项相交集进行剪枝,有效避免了计算所有极大项相交集对应极大项个数时的冗余求解;提出构建记录子句间互补关系的互补表方法,给出重用极大项相交集基础子句集互补结果的增量互补判定方法,较好地避免了判断子句间和各极大项相交集的基础子句集互补关系时的重复计算.实验结果表明:RCER方法易于实现,扩展性强,比CER方法效率更高,尤其是在互补因子较低时,效率提升更为显著.
英文摘要:
      #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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利