结合扩展规则重构的#SAT问题增量求解方法
#SAT问题是人工智能中的重要问题,在人工智能领域被广泛应用.在对基于扩展规则的模型计数求解方法CER深入研究的基础上,重构CER中使用的计算公式,并对其正确性进行了证明;提出极大项相交集和扩展极大项相交集的概念,并给出根据两者关系重用极大项相交集计算结果的增量求解方法,且对广义互补子句集对应的所有扩展极大项相交集进行剪枝,有效避免了计算所有极大项相交集对应极大项个数时的冗余求解;提出构建记录子句间互补关系的互补表方法,给出重用极大项相交集基础子句集互补结果的增量互补判定方法,较好地避免了判断子句间和各极大项相交集的基础子句集互补关系时的重复计算.实验结果表明:RCER方法易于实现,扩展性强,比CER方法效率更高,尤其是在互补因子较低时,效率提升更为显著.
扩展规则、模型计数、极大项相交集、互补表、增量方法
26
TP18(自动化基础理论)
国家自然科学基金61272208, 61133011,61402196,61003101, 61170092;国家教育部博士点专项基金20100061110031;中国博士后科学基金2013M541302;吉林省科技发展计划20101501,20140520067JH National Natural Science Foundation of China61272208, 61133011, 61402196, 61003101, 61170092;Doctoral Fund of Ministry of Education of China20100061110031;China Postdoctoral Science Foundation2013M541302;Jilin Province Science and Technology Development Plan20101501, 20140520067JH
2016-08-19（万方平台首次上网日期，不代表论文的发表时间）
共13页
3117-3129
