布尔可满足性（Boolean Satisfiability Problem,简称SAT）问题又称为SAT问题是人工智能、数理逻辑、计算机科学等领域的中心问题。自从1971年美国计算机学家Stephen Cook使用图灵机的理论概念首次证明SAT问题是NPC（Nondeterministic Polynomial Complete,简称NPC）问题以来,SAT问题就一直备受关注。由于在多项式时间内一个NPC问题可以转化为另外一个NPC问题且所有的NPC问题计算方式都是相同的,因此可以将SAT问题作为所有NPC问题的一个引子,若能设计出一个高性能的SAT求解算法在多项式时间内对SAT问题求解,则所有NPC问题也都可以在多项式时间内被解决,由此可证明NP=P。众多学者都在努力寻找一种新的高效求解SAT问题的算法,就目前看来设计一个强大的求解SAT问题的算法依然具有十分重要的意义。SAT问题的求解算法根据完备性主要分为两种:完备算法和不完备算法。虽然不完备算法的时间复杂度是多项式级的且在求解速度方面优于完备算法,但是不完备算法并不能保证一定能够找到对应问题的解。完备算法虽然在理论上能给出所有可满足问题的解,对于不可满足问题可直接给出证明,但是完备算法的时间复杂度最高是指数级的,理论上要穷尽二叉树搜索空间才能找到问题的解。由于在实际应用中对于给定的问题,当问题是可满足时需要求解器给出相应的可满足解,当问题不可满足时要给出完备的证明。因此,本文主要研究工作是在完备算法的基础上开展的。本文将在主流的完备算法-基于冲突子句学习（Conflict-Driven ClauseLearning SAT,简称CDCL-SAT）求解框架基础之上,以提高求解器性能为目标,对变量决策策略改进。早期变量决策策略都是依赖一些子句固有的特征,如将子句的数目大小、子句长度、未赋值变量的个数等作为选择决策变量的特征参数。目前主流的变量决策策略大多是基于冲突的变量评估,针对以上变量决策策略的缺点,提出学习子句删除影响后续布尔约束传播（Boolean Constraint Propagation,简称BCP）的猜想。改进求解器原代码,提取学习子句删除前和删除后变量所在子句的数目,设计实验证实猜想成立。鉴于这些策略并没有考虑到决策变量所在的子句数目对BCP的影响,提出了基于学习子句删除的变量决策策略（Variable Decision Algorithm Based on Learnt Clauses Deletion,简称VDALCD）,并改进了变量活跃度的计算方式。将VDALCD策略嵌入到Glucose4.1,Maple LCMDist Chrono BT-DL-v2.1和Relaxed＿LCMDCBDL＿new Tech求解器中,改进后的求解器分别记为Glucose4.1＿VDALCD、Maple-DL＿VDALCD和RLNT＿VDALCD。以2018年SAT竞赛Main组实例为测试基准,Glucose4.1＿VDALCD比原求解器Glucose4.1多求解出26个例子,增加了15.5%。以2019年SAT竞赛Main组实例为测试基准,Maple-DL＿VDALCD比原求解器Maple LCMDist Chrono BT-DL-v2.1多求解出17个例子,增加了7.6%;比2019年冠军求解器Ca Di Cal多求解出6个例子,增加3.1%。对于随机类问题改进后的RLNT＿VDALCD求解器较原求解器多求出82个,增加了12.8%;较2020年冠军求解器Kissat＿sc2020＿sat多求解出442个,增加了158.9%。因此,本文提出的VDALCD算法可以有效的提升SAT求解器求解性能。