SAT问题是计算机科学理论和人工智能中的著名问题。在理论应用领域，许多NP完全问题，诸如旅行商问题、背包问题、路由选择问题等都可以在多项式时间内转换为SAT问题求解；在实际应用领域，许多现实问题也可以通过不同的编码技术转换为SAT问题进行求解，诸如组合优化问题、软件形式化验证、硬件形式化验证、模型检验以及人工智能领域的规划问题等。因此，研究求解SAT问题的高效算法有着重要的理论价值和应用价值。许多研究学者对SAT问题的求解算法进行了相关的研究，其中DPLL算法是求解SAT问题的一个经典的完备算法，在其基础上发展的CDCL算法已成为目前主流SAT求解器的求解框架。CDCL算法中主要的发展是利用归结原理产生学习子句，而基于徐扬教授等提出的基于矛盾体分离的演绎自动推理理论突破了传统二元归结每次归结只有两个子句参与且只删除两个文字的局限，基于此，本文开发了基于矛盾体分离的命题逻辑动态自动演绎推理与CDCL算法相融合的SAT求解器，并针对学习子句生成、变量决策、演绎结果评估、重启、重复演绎路径等问题提出了一系列的优化算法。
　　实现了基于矛盾体分离的命题逻辑动态自动演绎推理与CDCL融合的SAT求解基础算法，并对CDCL求解算法中基于蕴涵图的学习机制进行了研究，分析了蕴涵图中唯一蕴涵点之间的关系，提出了基于矛盾体分离的学习子句算法。通过分析蕴涵图确定与冲突有关的所有子句，并利用矛盾体分离规则对这些子句重新演绎推理，得到一个新的学习子句，使得CDCL求解器在每次冲突时生成两个互不矛盾的学习子句，利用生成的学习子句推导出更多的蕴涵变量，并且减小发生冲突时的决策层次，加强搜索空间的剪枝能力，加速求解过程。实验表明，针对求解2015SAT和2016SAT的应用类实例，基于矛盾体分离规则的学习子句生成算法在冲突次数、决策次数以及布尔约束传播次数等关键指标上有着明显的改善，整体提高了求解性能。
　　针对CDCL求解算法通常利用启发式算法中每个变量的得分值改变决策变量的赋值序列的问题，提出了一种基于演绎结果为导向的改变变量赋值序列的算法，在冲突分析时找到符合条件的相关子句集合，利用矛盾体分离规则得到演绎结果，通过此演绎结果可直接确定一个决策变量，该决策变量的决策层小于当前回退层，进而改变变量的赋值序列。并且根据演绎结果的LBD值和回退层次，定义了一种动态更新变量奖励值的方法。实验结果表明该算法改变变量赋值序列更频繁，增大找到解的可能性，并且使得每次回退时的层次更小，加强搜索空间的约简能力。对于求解可满足和不可满足实例，该改进算法也表现出了较好的求解性能。
　　研究了学习子句删除算法，分析了学习子句删除周期的合理性，并通过实验说明了删除学习子句的必要性，提出了一种基于演绎长度的评估学习子句质量的标准，针对现有删除学习子句策略中评估学习子句标准的单一性问题，将基于演绎长度的评估标准与基于LBD值的评估标准相结合，提出了一种基于均值化的学习子句评估标准，该标准可以保留更多对后续求解过程有利的学习子句，删除更多无用的学习子句，加速求解过程。实验验证了基于均值化的学习子句删除策略求解SAT竞赛实例时，无论是求解总数，还是求解时间均显现出求解优势。
　　研究了重启算法，从监测求解过程中的参数冲突决策层的变化出发，提出了基于指数平滑的动态重启算法，通过比较预测值与实际值的关系动态的触发重启。针对现有的重启策略仅监测求解过程中一种参数的变化状态决定是否重启，在基于指数平滑的基础上，引入冲突决策层和LBD值来综合反映当前搜索分支的状态变化，分析了冲突决策层与LBD值的相关系数，提出了基于回归分析的动态重启策略，通过比较预测值与实际值动态的触发或延迟重启。实验结果表明，所提的两种动态重启策略的求解性能均优于静态重启策略和动态重启策略。
　　研究了自适应调整重复路径的算法，在分析了静态重启算法和动态重启策略均存在重复路径的问题后，提出了一种动态改变变量赋值序列的算法，该算法根据重启前后产生的重复赋值序列的大小，动态调整相关变量的得分值，利用变量得分值的变化即可改变变量的赋值顺序，进而改变求解器的搜索路径，避免浪费过多不必要的求解时间。实验结果表明，所提算法可适应性的改变变量赋值的顺序，在一定程度上减少了重复路径的生成。同时，实验结果表明所提算法的求解性能也优于国际SAT竞赛中知名的求解器。