两种新的基于扩展规则#SAT问题求解算法

• 作者: 刘磊 吕帅 张桐搏 王强
• 来源期刊: 东北大学学报（自然科学版）
• 学科: 工学
• 关键词: 自动推理 扩展规则 模型计数 极大项空间 启发式策略
• 年，卷（期）: 2019,（5）
• 所属期刊栏目: 信息与控制
• 页码范围: 630-634,646
• 页数: 6页
• 分类号: TP181
• 字数: 4505字
• 语种: 中文
• DOI: 10.12068/j.issn.1005-3026.2019.05.005

摘要

提出一种新的基于扩展规则的#SAT求解算法NCER,该算法在#ER的基础上加入启发式策略.该策略每次选择当前子句集的最长子句来减小极大项空间,使得递归调用的次数减少,从而加快求解效率.为解决基于扩展规则的#SAT求解器在互补因子较小的样例上的不良表现,结合NCER和CDP的优点提出混合#SAT求解算法NCDPER.实验结果表明:NCER较先前的#ER在所有85个随机SAT测试用例上有了显著的提高.通过与目前最好的基于扩展规则的#SAT求解器的比较,该求解器具有更好的性能.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘磊	吉林大学计算机科学与技术学院	211	1231	18.0	25.0
2	王强	吉林大学计算机科学与技术学院	81	415	12.0	17.0
3	吕帅	吉林大学计算机科学与技术学院	42	204	8.0	13.0
4	张桐搏	吉林大学计算机科学与技术学院	7	6	2.0	2.0