摘要：在可计算性理论和复杂性理论中,可满足性问题是一个重要的NP-完全问题。可满足性问题已经广泛地应用于自动推演,计算机辅助设计,计算机辅助操作,机器视觉,数据库等等。通常来说,可满足性问题是指离散的有约束的一类判定性问题,其形式化定义为：给定一个布尔合取范式F,是否存在一个F的赋值,使得F为真。可满足性问题算法的时间复杂度计算过程主要涉及3类参数：范式中变量的个数n,范式中子句的个数m,范式中字符的个数L。本文从字符个数L的角度,研究了一般性可满足性问题的精确算法。在以同样参数来解决该问题的精确算法中,目前最好的算法时间复杂度为O*(1.0652L),其中L是范式中字符的个数。本文首先研究了可满足性问题的预处理过程。根据消除(resolution)原理和引入的度量--范式F中所有变量的频率权值之和,本文给出了12条化简规则的预处理过程及其证明。对于化简后的范式,所有子句都包含至少两个字符,同时明确了包含两个字符的子句和其他类型子句的关系,并且任意两个不同的字符都不可能同时包含在两个子句中。本文采用分支搜索技术对可满足性问题进行求解。算法在每次分支之前,对范式进行预处理。当预处理后的范式中含有特定的3种子句结构之一时,算法针对这种子句结构进行特殊分支。否则,算法将选出范式中频率最大的变量进行分支。本文的主要贡献除了改进可满足性问题算法时间复杂度外,还引入了一种全新的分析方法,即加权分治(Measure and Conquer)。该方法给范式中每个变量赋予一个权值,该权值在分支过程中会产生额外的减少量,从而使得最终的时间复杂度更紧。通过改进分支算法并在分析中引入加权分治分析技术,本文算法的时间复杂度为O*(1.0651L)。图2幅,表4个,参考文献43篇。