计算机应用研究

作者：何飞,王晓峰,唐傲,华盈盈,彭庆媛,王军霞,

单位：北方民族大学a.计算机科学与工程学院;b.图像图形智能处理国家民委重点实验室,银川750021；

关键词：布尔可满足性问题,CDCL,分支策略,GLR,变量决策层,

基金：国家自然科学基金资助项目(62062001)；宁夏青年拔尖人才资助项目(2021)；北方民族大学研究生创新项目(YCX23153)；；

冲突驱动子句学习（conflict-driven clause learning，CDCL）是现代SAT求解器的主流框架，而基于变量活性的分支算法是其高效求解的关键因素之一。将全局学习率（global learning rate，GLR）和变量决策层结合分析，得到两个有关CDCL搜索行为的重要推论：在GLR较高时，增加低决策层变量的碰撞分数可以降低搜索成本；而在GLR较低时，增加高决策层变量的碰撞分数可以充分探索解空间。通过实验数据分析，验证了两个推论的正确性。依据推论，提出一种结合GLR和变量决策层的Gdb启发式策略来优化现有分支算法，Gdb使用变量决策层设计两个权重w1和w2，分别用于较高和较低GLR情况下的变量活性。此外，还分析了EVSIDS和LRB两个分支算法的搜索行为，并针对 LRB 进行再次加权。实验结果表明，Gdb 分支策略有效提升了CDCL求解器的效率。

来源：2025年第2期

《计算机应用研究》期刊编辑部

查看计算机应用研究杂志2025年第2期