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

• 作者: 刘思光 张立明 欧阳丹彤 贾凤雨
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 扩展规则 模型计数 极大项相交集 互补表 增量方法
• 年，卷（期）: 2015,（12）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 3117-3129
• 页数: 13页
• 分类号: TP18
• 字数: 11062字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004827

摘要

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