基于动态奖惩的分支策略的SAT完备算法

• 作者: 刘燕丽 徐振兴 熊丹
• 来源期刊: 计算机应用
• 学科: 工学
• 关键词: NP完全问题 可满足性问题 冲突驱动子句学习 完备算法 分支策略
• 年，卷（期）: 2017,（12）
• 所属期刊栏目: 人工智能
• 页码范围: 3487-3492
• 页数: 6页
• 分类号: TP301.6
• 字数: 6361字
• 语种: 中文
• DOI: 10.11772/j.issn.1001-9081.2017.12.3487

摘要

针对学习子句数量有限或相似度高导致历史信息有限、搜索树不平衡的问题,提出了基于动态奖惩的分支策略.首先,对每次单子句传播的变元进行惩罚,依据变元是否产生冲突和产生冲突的间隔,确立不同的惩罚函数;其次,在学习阶段,利用学习子句确定对构造冲突有益的变元,非线性增加它们的活跃度;最后,选择活跃度最大的变元作为新分支变元.在glucose3.0算法基础上,完成了改进的动态奖惩算法——AP7.实验结果表明,相比glucose3.0算法,AP7算法的剪枝率提高了14.2％ ～ 29.3％,少数算例剪枝率的提高可达51％,且改进后的AP7算法相比glucose3.0算法,运行时间缩短了7％以上.所提分支策略可以有效降低搜索树规模,使搜索树更加平衡,减少计算时间.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	熊丹	武汉科技大学理学院	15	23	3.0	4.0
2	刘燕丽	武汉科技大学理学院	16	74	5.0	8.0
6	徐振兴	华中科技大学计算机科学与技术学院	1	3	1.0	1.0