两种新的基于扩展规则#SAT问题求解算法
来源期刊：东北大学学报(自然科学版)2019年第5期
论文作者：吕帅 张桐搏 王强 刘磊
文章页码：630 - 1280
关键词：自动推理;扩展规则;模型计数;极大项空间;启发式策略;
摘 要：提出一种新的基于扩展规则的#SAT求解算法NCER,该算法在#ER的基础上加入启发式策略.该策略每次选择当前子句集的最长子句来减小极大项空间,使得递归调用的次数减少,从而加快求解效率.为解决基于扩展规则的#SAT求解器在互补因子较小的样例上的不良表现,结合NCER和CDP的优点提出混合#SAT求解算法NCDPER.实验结果表明:NCER较先前的#ER在所有85个随机SAT测试用例上有了显著的提高.通过与目前最好的基于扩展规则的#SAT求解器的比较,该求解器具有更好的性能.
吕帅，张桐搏，王强，刘磊
吉林大学计算机科学与技术学院
摘 要：提出一种新的基于扩展规则的#SAT求解算法NCER,该算法在#ER的基础上加入启发式策略.该策略每次选择当前子句集的最长子句来减小极大项空间,使得递归调用的次数减少,从而加快求解效率.为解决基于扩展规则的#SAT求解器在互补因子较小的样例上的不良表现,结合NCER和CDP的优点提出混合#SAT求解算法NCDPER.实验结果表明:NCER较先前的#ER在所有85个随机SAT测试用例上有了显著的提高.通过与目前最好的基于扩展规则的#SAT求解器的比较,该求解器具有更好的性能.
关键词：自动推理;扩展规则;模型计数;极大项空间;启发式策略;
