-
题名基于近期文字极性分配的学习子句评估算法
- 1
-
-
作者
冯心妍
吴贯锋
张丁荣
王恪铭
-
机构
西南交通大学信息科学与技术学院
西南交通大学系统可信性自动验证国家地方联合工程实验室
西南交通大学数学学院
西南交通大学计算机与人工智能学院
-
出处
《计算机工程与科学》
CSCD
北大核心
2023年第11期1941-1948,共8页
-
基金
国家自然科学基金(62106206)。
-
文摘
为了维护学习子句数据库的大小,并以合理的成本执行单元传播,在SAT求解器求解过程中需要对学习子句进行评估,从而删除对求解过程无用的子句。因此,需要对学习子句数据库进行动态管理,包含对学习子句的分析和删除等,并提出新的评估子句有用性的方法,从而保留对求解最有促进作用的学习子句,以提高求解效能。从捕获学习子句近期的极性分配出发,结合现代求解器的回溯环节中常用到的基于字面极性的启发式方法——进度节省,来推断给定学习子句与剩余搜索步骤的相关性。以最先进的2种基于冲突驱动子句学习算法CDCL的求解器Glucose和MapleLCMDistChronoBT求解器为基准,针对其在子句评估环节的算法进行改进测试。实验结果表明,这种基于近期文字极性分配的子句评估策略能够普遍提高CDCL串行和并行求解器的求解效率,有效改善了原有求解器在一些问题上求解耗时过长的问题,并在先进求解器的水平上多求解了2个合取范式CNF文件,单个文件的平均求解时间缩短了13~34 s。
-
关键词
SAT问题
子句评估策略
CDCL
学习子句
-
Keywords
SAT problem
clause evaluation strategy
conflict driven clause learning(CDCL)
learnt clause
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
TP391
[自动化与计算机技术—计算机科学与技术]
-
