可满足性问题(简称SAT问题)是计算机领域和人工智能领域的核心问题之一。S.A.Cook于1971年首次论证SAT问题是NP-完全的,即任何NP问题都可在多项式时间内规约到SAT问题上求解,求解SAT问题有助于解决NP问题;SAT问题被广泛应用于众多领域,如:数学、计算机科学、形式化验证等;因此研究SAT问题具有重要的理论价值和应用前景。SAT问题的求解算法按照完备性可分为完备算法和不完备算法。不完备算法对于解决可满足的问题花费的时间较短,但是不能判断问题的不可满足性;完备算法比不完备算法出现的早,它对于解决可满足的问题花费的时间相对较长,但在问题不可满足时能给出证明。CDCL算法是目前流行的完备算法,它由经典的完备算法DPLL算法发展而来,现在大多数高效的求解算法都是基于CDCL算法而提出的,本文基于CDCL算法针对分支策略和删除策略进行研究,所做的工作如下:1.根据子句长度对初始阶段分支变量的影响,引入初始阶段变量得分函数,为初始阶段分支策略提供依据;依据子句LBD值对冲突阶段分支变量的影响,引入冲突后变量得分函数,用于计算冲突后变量得分情况,基于以上引入的初始阶段变量得分函数和冲突后变量得分函数,提出一种分支策略—基于子句LBD值的分支策略(CLBH)。2.根据学习子句LBD与长度对删除策略的影响,引入文字平均LBD的概念,作为评估学习子句的标准,在此基础上提出一种删除策略—基于文字平均LBD的删除策略(LABCD)。3.将基于子句LBD的分支策略形成算法,嵌入到著名求解器Glucose4.1中,得到求解器Glucose4.1+CLBH。选用SATLIB Benchmark中的实例进行测试,从成功求解个数、求解所花费时间、冲突次数、决策次数、传播次数等方面进行分析,以说明求解器Glucose4.1+CLBH的有效性和表现优异之处。4.将基于平均文字LBD的删除策略和形成算法,嵌入到著名求解器Glucose4.1中,得到求解器Glucose4.1+LABCD。选用2017年和2018年SAT竞赛Main Track组中的实例进行测试,从成功求解个数、求解所花费时间、冲突次数、决策次数、传播次数等方面进行分析,以说明求解器Glucose4.1+LABCD的有效性和表现优异之处。