计算机工程与科学

作者：冯心妍, 吴贯锋, 张丁荣, 王恪铭,

单位：1.西南交通大学信息科学与技术学院,四川 成都 611756；2.西南交通大学系统可信性自动验证国家地方联合工程实验室,四川 成都 611756；3.西南交通大学数学学院,四川 成都 611756；4.西南交通大学计算机与人工智能学院,四川 成都 611756

关键词：SAT问题,子句评估策略,CDCL,学习子句,

基金：国家自然科学基金(62106206)

为了维护学习子句数据库的大小，并以合理的成本执行单元传播，在SAT求解器求解过程中需要对学习子句进行评估，从而删除对求解过程无用的子句。因此，需要对学习子句数据库进行动态管理，包含对学习子句的分析和删除等，并提出新的评估子句有用性的方法，从而保留对求解最有促进作用的学习子句，以提高求解效能。从捕获学习子句近期的极性分配出发，结合现代求解器的回溯环节中常用到的基于字面极性的启发式方法——进度节省，来推断给定学习子句与剩余搜索步骤的相关性。以最先进的2种基于冲突驱动子句学习算法CDCL的求解器Glucose和MapleLCMDistChronoBT求解器为基准，针对其在子句评估环节的算法进行改进测试。实验结果表明，这种基于近期文字极性分配的子句评估策略能够普遍提高CDCL串行和并行求解器的求解效率，有效改善了原有求解器在一些问题上求解耗时过长的问题，并在先进求解器的水平上多求解了2个合取范式CNF文件，单个文件的平均求解时间缩短了13~34 s。

来源：2023年第11期

《计算机工程与科学》期刊编辑部

查看计算机工程与科学杂志2023年第11期