可满足性问题（Satisfiability problem,SAT）是一个判定问题。给定一个合取范式,SAT问题适用于判定是否存在一组真值指派使得该合取范式可满足。作为第一个被证明的NP完全问题,SAT问题具有重要的理论研究价值和实际应用价值。现代SAT完备性算法主要基于冲突驱动的子句学习（Conflict Driven Clause Learning,CDCL）方法,即通过精确学习搜索过程中产生的冲突并以此来指导搜索。CDCL SAT求解器在搜索过程中会产生大量的学习子句,同时原始子句和新生成的学习子句中均可能含有大量的冗余文字。这些冗余文字会明显降低求解器的求解效率。为升CDCL SAT求解器的求解效率,全文以子句化简为主线,针对目前面临的三个方面的问题分别出了三个方法,主要工作和创新点如下。针对当前基于单子句传播的学习子句化简技术化简的子句数量少且时间开销大的问题,出了一种新的基于单子句传播技术的高效学习子句在线化简方法,称为LCM（Learnt Clause Minimization）。通过结合CDCL SAT求解器的性质采用启发式的策略,首先对化简时机进行优化选择,即选择在求解器搜索过程中某些重新启动的时刻进行化简操作,且随着搜索过程不断深入,逐渐降低化简操作的触发频率;之后对化简对象进行优化选择,即仅挑选质量相对较高的子句进行化简;最后对化简顺序进行优化选择,即按照文字在子句中的当前顺序,对其逐一进行单子句传播。通过实验分析可知,使用LCM化简方法显著升了CDCL SAT求解器的化简效果、运算速率和求解效率。在2016年SAT竞赛第一名的求解器Maple＿LRB上采用LCM化简方法,能够多求解15个算例,而在该竞赛中Maple＿LRB只比第四名求解器多求解了4个算例。针对全面深入多次在线化简所有子句面临巨大的计算开销问题,渐进式地出了两种基于子句质量的多次深入化简学习子句和原始子句的方法。首先,基于子句的文字块距离（Literal Block Distance,LBD）值在搜索过程中的变化情况制定了子句被再次化简的标准,出了CML（Clause Minimization based on LBD）化简方法。其次,基于子句参与“有效冲突”的情况制定了子句适合被化简的标准,从而进一步出了CMLC（Clause Minimization based on LBD and Conflict）化简方法。通过测试2014年、2016年和2017年SAT竞赛中共1450个算例发现,基于CML方法的求解器Maple＿CML相比于基于LCM方法的求解器Maple＿LCM多求解了34个算例。通过测试2018年和2020年SAT竞赛中共800个算例发现,基于CMLC方法的求解器Maple＿CMLC相比于基于CML方法的求解器Maple＿CML多求解了24个算例。针对难以挑选合适的分支策略来求解具体类型的算例的问题,出了一种基于学习子句化简率（冗余文字删除比率）的分支策略选择方法,称为BSS（Branching Strategy Selection）。该方法可以对具体类型的问题选择有效的分支策略,即对LCM化简率较低的算例,升学习速率分支策略（Learning Rate Branching,LRB）的使用频率以高求解性能。在2017年、2018年和2020年SAT竞赛的所有算例上进行测试发现,使用BSS方法能够显著升求解器的求解效率。特别是对于2020年SAT竞赛算例,BSS方法能够使得求解器Maple＿CML多求解16个算例。相关工作的有效性也在国际SAT竞赛中得到了验证:使用LCM和CML方法开发的求解器Maple＿LCM和Maple＿CML,分别在2017年和2018年SAT竞赛（SAT Competition）Main组中获得冠军和季军。