SAT问题是计算机科学理论和人工智能中的著名问题。NP完全问题(NP-complete,NPC)排在千禧年七大难数学问题之首,许多NP完全问题都可以在多项式时间内转换为SAT问题进行求解。SAT问题广泛应用于数学定理证明、计算机软件与理论、工程技术、软件验证以及逻辑电路等价性验证等多个领域。因而SAT问题一直是国内外学者关注的热点问题,设计并实现求解SAT问题的高效算法具有重要的钻研意义和应用远景。DPLL求解器开创了求解SAT问题的先河,但其算法自身的回溯机制对大规模问题的求解有一定程度的制约性。为了提升DPLL算法的求解效率,国内外学者们进行了大量的研究,添加了一些关键技术。例如启发式分支策略、基于冲突分析和子句学习、非时序回溯、学习子句的删除和周期性重启等,形成了当前最流行的CDCL(Conflict-Driven-Clause-Learning,CDCL)求解器。基于CDCL算法结构,本文做了以下研究工作:一、借鉴VSIDS策略及其延伸策略的思想,研究变量的决策层和变量参与冲突的冲突次数对分支决策阶段的影响,在此基础上提出一种改进的启发式分支策略——基于变量决策层的启发式变量选择策略(HSVDL),为分支决策提供依据,从而引导求解器的搜索进程。二、在充分考虑学习子句的子句长度和变量的决策层对子句删除的影响后,为了充分发挥短子句在演绎过程中的优势,因此给出平均子句长度的定义,在删除策略中用于删除较长的学习子句。然后提出了一种新的学习子句删除策略——基于学习子句长度和LBD的删除策略(LLBD)。三、分别将所提出的HSVDL策略和LLBD策略形成相应算法,嵌入到著名求解器Glucose4.1中,得到新的求解器Glucose4.1+HSVDL和Glucose4.1+LLBD;将所提出的HSVDL策略和LLBD策略同时嵌入求解器Glucose4.1中,得到新的求解器Glucose4.1+HSVDL+LLBD。选择2017年和2018年SAT国际竞赛Main Track组的竞赛例进行测试,测试结果从成功求解个数、平均决策次数、平均冲突次数、平均重启次数、平均用时等多项指标与求解器Glucose4.1的测试结果进行对比分析,显示出了新的求解器的有效性及优势。