结合扩展规则重构的#SAT问题增量求解方法

来源：软件学报杂志2015年第12期北京时间：

作者：贾凤雨,欧阳丹彤,张立明,刘思光

单位：贾凤雨，吉林大学计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001211,欧阳丹彤，吉林大学计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001202,张立明，吉林大学计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001203,刘思光，吉林大学计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001204

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

关键词：扩展规则;模型计数;极大项相交集;互补表;增量方法

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