CDCL算法框架下的学习子句优化策略研究

作     者：毕舜阳 

作者单位：西安电子科技大学 

学位级别：硕士

导师姓名：游海龙;苏宇

授予年度：2022年

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：CDCL算法 学习子句 LBD标准 HEC标准 分支启发策略 

摘      要：可满足性问题(Boolean Satisfiability Problem),又称SAT问题,是指对于一个给定的合取范式(Conjunctive Normal Form),能否找到一组变量的赋值使得该式成立。该问题因在集成电路设计自动化的形式验证和自动测试模式生成(ATPG)问题中被广泛应用,而成为近年来的研究热点。求解SAT问题的算法分为两种:完备算法和不完备算法,完备算法因为具有可证明结果不满足的特性,因此适合应用在形式验证和ATPG问题中。CDCL算法(Conflict-Driven Clause Learning)是目前完备算法中最高效的算法框架。CDCL算法框架的主要原理是利用分支启发策略选择一个变量赋值,赋值的变量进行布尔约束传播,产生冲突后得到学习子句,之后的传播会通过学习子句避免相同的冲突,进而完成所有变量的赋值。CDCL算法成功的原因之一在于其采用了学习子句策略,可以有效地缩小算法的搜索空间,实现高效的求解。因此本文的研究工作集中在学习子句的优化策略上,主要包括以下四方面: 1、本文通过实验测试观测到,传统的学习子句评价标准——LBD标准,在近几年提出的分支启发(LRB策略)下产生了评价误差。在具体的实验结果中,出现评价误差的测试例子占到总测试例子的48.9%。对此,分析其误差产生的原因可能是LRB分支启发下更频繁的变量更新导致的; 2、针对LBD标准出现的评价误差和导致其误差的潜在原因,本文提出了一种新的学习子句评价标准——基于冲突频率和LBD值的混合标准(HEC标准)。HEC标准采用指数加权平均的处理方式巧妙地将冲突频率和LBD值结合起来,可以动态地反映学习子句的质量。在给出HEC标准的算法实现后,本文对其进行了初步的验证,结果显示,采用该标准的学习子句使用率要比LBD标准高32.8%;在应用到求解器上时,除了在LRB分支启发下有较好的提升之外(比原算法多解决5个例子),在传统的VSIDS分支启发下也有高效的表现(比原算法多解决5个例子); 3、基于BCP传播的次数远大于冲突分析的次数的事实,本文通过一组实验观测到,学习子句在BCP传播的速度是冲突分析中的20倍以上,因此考虑将学习子句的更新添加到BCP传播中,其目的是为了加快学习子句的更新速度,更有利于筛选出高质量的学习子句。在经过测试对比后结果显示,基于BCP传播的更新方式可以加快学习子句的更新速度,应用在求解器上比冲突分析中的更新多解决9个测试例子; 4、本文提出了一种新的学习子句删除算法框架,并将前两部分的工作——BCP传播的更新方式和HEC标准结合起来,整合在学习子句删除的框架中,实现了一种新的学习子句删除算法。两组不同分支启发下的测试和一组ATPG电路中的测试都显示,应用该算法的求解器求解提升率都在约15%以上。