布尔可满足性问题是理论计算机科学中的核心问题,人们一直致力于寻找CNF公式实例难解的本质,通过限定CNF公式的结构,如子句长度、布尔变元出现次数等,并以此为基础,分析CNF公式的结构信息,设计高效的求解算法。本文研究的平衡正则(k,2r)-CNF公式是一类具有规则结构的CNF公式,通过限定每个子句的长度为k,每个布尔变元的正出现次数和负出现次数都为r,其实例求解难度比一般的k-CNF公式实例求解难度大。本文从实例生成模型、结构信息、求解算法、相变性质等方面对平衡正则(k,2r)-CNF公式进行研究,主要研究成果如下:(1)为了便于分析平衡正则(k,2r)-CNF公式的结构信息及相变性质,构建了一个生成平衡正则(k,2r)-CNF公式实例的随机模型—BR(n,k,2r)模型。该模型可以有效地生成不重复的平衡正则(k,2r)-CNF公式子句。(2)通过将平衡正则(k,2r)-CNF公式分别表示为变元交互图和因子图,研究了平衡正则(k,2r)-CNF公式的结构信息。实验发现:在变元交互图中,顶点的度与公式的子句变元比正相关;在因子图中,子句与变元呈现交错分布。(3)基于平衡正则(k,2r)-CNF公式特殊的结构信息,改进了随机局部搜索(Stochastic Local Search,SLS)算法的初始赋值方式来求解该类正则公式。实验结果表明:改进后的SLS算法比原算法能更有效地求解平衡正则(k,2r)-CNF公式。(4)平衡正则(k,2r)-CNF公式实例随着子句变元比的增大,会出现可满足性相变现象。通过理论分析,给出了平衡正则(k,2r)-CNF公式可满足性相变阈值点的一个上界为2~kln 2-kln 2/2,一个下界为2~kln 2-kln 2/2-2ln 2.