布尔可满足性问题(Satisfiability Problem,SAT问题)是逻辑学中经典的判定问题,也被证明是一个NPC(Non-deterministic Polynomial Complete)问题。由于NPC问题能在多项式时间内相互转化,因此所有的NPC问题都能转换为SAT问题进行求解。此外,在实际应用中,如计算机辅助设计与制造、生物信息、人工智能等领域的许多问题都可转化为SAT问题进行求解。因此,快速求解SAT问题具有重要的研究价值。近几十年来,对SAT问题的研究已经取得了重大进展,特别是CDCL(Conflict Driven Clause Learning)算法的提出,使得求解器可以在几分钟内解决数十万变量和数百万个子句的工业实例。因此,本文的研究工作主要是以CDCL算法为算法框架,围绕分支变量决策和学习子句删除两方面进行了系统研究,在已有方法基础上提出了一些改进策略和新方法,并通过理论分析和实验进行了有效性验证。本文主要的研究工作如下:1.为解决求解SAT问题过程中分支决策效率不高的问题,本文在EVSIDS(Exponential Variable State Independent Decay Sum)分支策略的基础上,提出了基于二次奖励的分支启发式(Two Rewards Based Branching Heuristic,TRBH)策略。考虑到分支决策变量是在未赋值变量集中选取,针对在回溯期间转化为未赋值状态的变量,TRBH分支策略结合变量最近一次参与冲突分析的情况,再次给予这些变量一次奖励。通过二次奖励的方式可以增大最近一次参与冲突分析且未赋值的变量被选择为决策变量的可能性,以此改变决策变量的选择规则。2.为解决单一地利用LBD(Literals Blocks Distance)值来评估子句而导致子句利用率不高的问题。本文在LBD评估方法的基础上,增加了回跳层数(Back-Jump levels,BJL)的学习子句删除策略。该删除策略利用学习子句的回跳层数来评估学习子句的质量,因为学习子句回跳层数越大,在搜索过程中对二叉树的剪枝能力越强,也就是说可以加大剪枝效率,加快搜索速度,从而减少求解器的求解时间。3.将TRBH分支策略和BJL删除策略分别嵌入到Glucose4.1中,分别形成了求解器Glucose4.1+TRBH和Glucose4.1+BJL,然后实验测试了2017～2019的SAT竞赛实例。在分支策略实验中,对比Glucose4.1+TRBH和Glucose4.1两个求解器的求解个数、平均用时和决策次数,实验结果表明新提出的分支策略能有效减少分支决策次数,提高SAT求解器的求解效率。在删除策略实验中,对比Glucose4.1+BJL和Glucose4.1两个求解器的求解个数以及平均用时,实验结果表明BJL删除策略比单一的LBD删除策略更加科学合理。