在逻辑问题中,布尔可满足性问题(即SAT问题)一直广受人们的关注。SAT问题是确定以合取范式(CNF)的形式给出的命题逻辑公式是否具有对其变量的一组布尔真值赋值,使得该公式是可满足的,或者证明它不可满足。SAT问题在算法时间复杂度上是首个被证明的NP完全问题。目前,SAT问题是许多领域的研究热点,如定理证明、自动推理、模型检查、电子设计自动化、计算机辅助设计等。因此,有关SAT问题的研究,不仅在理论方面意义重大,而且在实际应用中也有着巨大的价值。不完备算法和完备算法是解决SAT问题的两类主要算法。不完备算法主要基于随机局部搜索的思想,完备算法主要基于回溯搜索的思想。完备算法的优点在于一定能够判定SAT问题的可满足性。目前,最流行的完备算法是CDCL算法,本文则是基于CDCL算法结构展开研究,主要取得了如下研究成果:1.在EVSIDS和ACIDS算法的启发下,提出了一种基于动态奖励的分支启发式算法,也称为DRB算法。每当冲突发生时,DRB算法通过综合考虑变量决策层、冲突层、冲突次数和变量冲突频率进行活性分数更新,从而引导求解器的分支变量决策。2.根据学习子句的LBD值引入了层次差,用于评估LBD值相同的学习子句之间的质量差异。基于此,提出了基于层次差的学习子句删除启发式策略,也称为LDCR策略,从而指导求解器的子句数据库管理。3.将DRB算法和LDCR策略嵌入到Glucose 3.0与MapleLCMDistChronoBT求解器中,得到了6个新的SAT求解器。主要做了两类实验,实验一是基于Glucose 3.0的改进求解器与Glucose 3.0之间的对比实验,选择2015年、2016年和2017年三年的SAT竞赛实例进行测试;实验二是基于2018年冠军求解器MapleLCMDistChronoBT的改进求解器与MapleLCMDistChronoBT之间的对比实验,选择2018年的SAT竞赛实例进行测试。将改进求解器的测试结果与原来的求解器进行对比分析,实验结果表明改进求解器的性能均高于原来的求解器。因此,本文提出的两种新的启发式策略可以有效改进已有的CDCL算法框架,进而提升求解器的性能。