从二十世纪五十年代开始,自动推理就成为了计算机科学的一个核心研究领域,而可满足性SAT (Satisfiability)问题是自动推理最重要的问题之一。基于扩展规则的方法是由林海等人于2003年提出的一种可用于求解SAT问题的方法,发表于人工智能领域的国际知名期刊Journal of Automated Reasoning。此方法一经提出,即得到包括欧美等地的众多学者的关注。基于扩展规则的方法不同于传统的基于归结的方法,对于互补因子高的子句集,具有明显的优势。求解SAT问题的方法被广泛应用于计算机科学的很多领域,包括定理机器证明、机器视觉、数据库等。很多NP问题,如：图染色问题、约束满足问题等,都可以转化成SAT问题求解。关于SAT问题的国际学术会议International Conference on Theory and Applications of Satisfiability Testing,每年举行一次,并且每两届会议举行一次SAT求解器竞赛。关于SAT问题的研究主要集中在提高SAT求解方法的效率上。本文的工作主要是研究如何将传统的归结方法与基于扩展规则的方法相结合以提高SAT求解方法的效率,以及将基于扩展规则的方法应用到模型计数(#SAT)问题的求解中,设计出高效的算法：(1)利用DPLL规则对基于扩展规则方法进行优化。减小待求解SAT问题的规模,将待求解SAT问题分解为一系列规模较小的问题进行求解。并提出MOAMD策略,对原子的排列顺序进行优化。设计出应用DPLL规则和MOAMD策略的算法CIER,实验结果显示,CIER算法保留了基于扩展规则方法在互补因子较高的SAT问题求解方面高效的特点,同时相比于IER算法,在不增加空间复杂性的前提下,时间效率上有1-2个数量级的提高。(2)提出基于碰集的SAT算法,此类算法不依赖于互补因子的高低。以扩展规则为理论基础,将求解子句集的可满足性问题,转化为判断子句集是否存在不包含互补文字的碰集的问题。并根据这个结论,提出基于碰集的SAT求解算法CBHST和RNHST。本文选择了具有代表性的基于归结的算法DR与算法CBHST和RNHST进行了实验比较,两者相对于基于归结的算法DR都有1个数量级以上的效率提升。当子句长度较大的时候,RNHST的搜索树高度较低,时间效率优于CBHST。当子句长度较小的时候,CBHST的搜索树中易出现剪枝,时间效率优于RNHST。对于布尔代数式形式的SAT问题,本文提出了算法SSBF。这个算法不需要将布尔代数形式的SAT问题转换成子句集的形式求解,可以直接用布尔代数进行计算,所以适用于布尔代数式形式的SAT问题。实验显示,该算法在相同参数下与RNHST算法的时间效率处于同一数量级。(3)将上述的基于碰集的方法与基于扩展规则的方法相结合,用于#SAT问题的求解。通过对扩展规则的研究发现,子句集所扩展不出的每一个极大项都对应这个子句集的一个模型,而且这个模型恰好是子句集的碰集所能扩展出的极大项。因此,当子句的长度较短,子句数较多的时候,可以先把子句集转化为一个规模较小的极小碰集的集合,然后使用基于扩展规则的方法对这个极小碰集的集合进行模型计数。依据这个思想,提出了可以精确进行模型计数的间接使用扩展规则方法的模型计数算法MCEHST。本文选择了同样可以精确进行模型计数的基于归结方法的算法CDP和基于扩展规则的算法CER与算法MCEHST进行实验比较。实验结果显示,当子句的长度较短,子句数较多的时候,这个模型计数算法的时间效率要高于模型计数算法CDP和CER,并且当子句数达到一定数量的时候,该算法所消耗时间的增长速度要小于CDP和CER。MCEHST算法适用于子句集形式的#SAT问题,对于布尔代数式形式的#SAT问题,本文提出了MCBE算法。MCBE算法与MCEHST具有类似的特点,当布尔代数式中项的长度较短且数量较大时,时间效率很高。因为MCBE算法直接应用布尔代数进行计算,所以更适合布尔代数式形式的#SAT问题求解。