命题逻辑公式的可满足性问题（SAT问题）是指给出一个合取范式,判断是否存在一组赋值使得这个合取范式可满足。SAT问题是计算机科学与工程、人工智能、计算机视觉和计算机辅助设计等领域的一个核心问题,它也是第一个被证明的NP完全（Non-Deterministic Polynomial-Complete,NPC）问题。正因为如此,研究SAT问题并提高求解器的效率是很有价值的。求解SAT问题的算法分为完备算法和不完备算法。完备算法的特点是在问题可满足时,给出一个模型;不可满足时,给出证明。基于完备算法的优点,本文以CDCL（Conflict Driven Clause Learning,CDCL）算法为框架,研究CDCL算法的以下主要流程:决策、冲突分析、学习子句和回溯之间的关系。SAT求解器的成功绝大多数归因于从错误赋值中学习的能力、快速地删除搜索空间以及首先集中在那些“重要”变量中^[1]。故本文集中在CDCL算法中的决策和冲突分析上,取得的主要研究结果如下:1.当一个命题逻辑中的逻辑公式以CNF的形式输入到数据库时,从中选择“重要”变量的依据是变量出现的次数和包含该变量子句的长度。因为越短的子句越难满足,故优先考虑短子句,相应地,短子句中的变量就“重要”。由这些信息,给出变量的初始计分和排序方法。2.当发生冲突时,即当前赋值使得某些子句为不可满足子句,参与冲突的那些子句中对应的变量的价值高于没有参与冲突的,因而在这个阶段考虑由这些子句或者变量所携带的信息刻画变量的贡献值。根据参考文献中的实验数据分析看出指数级的增长效果较好,因此,根据学习子句长度的不同,进行分段,在每个段,给出一个常数加上一个指数函数的方法进行计分排序。3.根据以上研究结果提出一种新的分支启发式策略并运用在glucose4.0算法上,用2016和2017年SAT竞赛例子和SATLIB例子测试,根据效果修改参数。结果表明在一定程度上比原始求解器glucose4.0有所提高。