可满足性问题(Satisfiability Problem,SAT问题)是数理逻辑中的一个经典问题,也是自动推理的一个重要研究方向。在理论应用方面,许多的NPC(Non-deterministic Polynomial Complete)问题如图着色问题、欧拉回路问题和旅行商问题等,都可以转化成SAT问题进行求解。在实际应用方面,如计算机辅助设计与制造领域和人工智能领域中的一些现实问题,通过逻辑形式化方法可以转化为SAT问题进行求解。另外,形式化验证中的一个不可缺少环节就是逻辑公式可满足性的判定。因此,研究SAT问题不仅具有重要的理论价值而且具有广泛的应用前景。目前,求解SAT问题的算法主要分为完备算法和不完备算法两种。完备性算法主要基于穷举和回溯思想,不完备算法主要基于局部搜索思想。基于DPLL(Davis Putnam Logemann Loveland)算法发展而来的CDCL(Conflict driven clause learning)算法是具有代表性的完备算法,也是目前求解SAT问题的一种主流算法。它的求解结构主要包括预处理、子句学习、分支决策和重启等模块。在CDCL算法求解框架中,随着搜索的进行求解器会不断地记录产生冲突的原因,能够避免后续搜索过程进入相同的冲突空间。研究结果表明,基于冲突学习的能力是CDCL算法求解高效的关键因素。在CDCL算法框架下,针对基于冲突分析的分支决策环节,本文主要做了以下两方面的工作:1.为减少求解器在分支决策环节出现过多随机赋值的现象,本文在VSIDS(Variable State Independent Decaying Sum)分支策略的基础上,融入了冲突次数和变量所在子句的LBD值两种特征,提出了一种基于变量特征的分支策略,称为BVA(Breaking the Balance of Variable Activity)分支策略。BVA分支策略在分支决策过程中不改变变量活性值的整体增长趋势,只是小幅度地提升了部分变量的活性值。这样不仅保留了VSIDS分支策略的原有优势,而且更有利于减少VSIDS分支策略的随机性,使分支变量的选择更准确。2.基于上面的工作,将BVA分支策略形成算法,嵌入到著名的求解器Glocose4.1和2018年国际竞赛冠军求解器Maple＿LCM＿Dist＿Chrono BT中,分别形成了Glocose4.1+BVA求解器和Maple＿LCM＿Dist＿Chrono BT+BVA求解器。在实验部分,实验选择2017-2019年的竞赛例作为测试例。通过实验对比分析表明改进的两个求解器在求解效率和求解能力方面均优于原版求解器,尤其在求解不可满足性问题上表现出明显的优势。