可满足性问题（The Satisfiability Problem,SAT问题）是理论计算机科学中备受关注的重要问题。随机k-SAT问题中相变现象的理论分析和实验验证均表明,子句约束密度是一个影响公式可满足性的重要参数。当公式的子句约束密度接近相变点时可满足性问题是难以判断的,当远离相变点时可满足性问题是易于判断的。但正则（k,s）-SAT问题的NP完全性却表明,子句约束密度对可满足性问题求解难度的刻画是粗糙的。由应用领域中的实际问题编码转化过来的SAT问题往往具有一些特殊的结构。如何有效利用他们的特殊结构进行快速求解,一直被人们所关注。为了更好的研究SAT问题的难解本质、设计更有效地SAT求解算法,我们用参数d来描述变元正负出现次数的差,引入d-正则（k,s）-CNF公式类。d-正则（k,s）-CNF公式是指一个CNF公式,其中每个子句包含k个不同变元,每个变元恰好出现s次且正负出现次数差不超过d。本文主要围绕d-正则（k,s）-CNF公式的结构特征、d-正则（k,s）-SAT问题的临界现象、唯一可满足的d-正则（k,s）-CNF公式的存在条件、几类（1,0）-SAT问题的临界现象展开研究。（1）通过分析d-正则（k,s）-CNF公式的结构特征,研究了d-正则（k,s）-SAT问题的NP完全性和临界现象。我们给出一种从k-CNF公式到d-正则（k,s）-CNF公式的多项式时间归约转换方法,发现在k?3时,如果d-正则（k,s）-CNF公式类存在不可满足实例,则d-正则（k,s）-SAT问题是NP完全问题。从而证明,在k?3时存在一个函数f（k,d）,使得当s?f（k,d）时,所有d-正则（k,s）-CNF公式都可满足;当s（29）f（k,d）时,d-正则（k,s）-SAT问题是NP完全问题。也就是说,当k?3时d-正则（k,s）-SAT问题存在一种从平凡性（不需要计算可直接得出确定的结果）到NP完全性的临界现象。函数f（k,d）被称为d-正则（k,s）-SAT问题的临界函数。结合对d-正则（k,s）-CNF公式结构特征的分析,给出了f（k,d）随k,d的变化规律,并证明f（k,d）是关于k的增函数,关于d的减函数。另外借助于改进的有限非递增整数序列构造方法,获得在k较小时f（k,d）的上界。（2）研究了唯一可满足的d-正则（k,s）-SAT问题。唯一可满足的k-SAT问题从理论角度已被证明和一般的k-SAT问题求解难度相当。我们提出构造唯一可满足的d-正则（k,s）-CNF公式的方法,并给出这类公式的存在条件。尤其,当k?7时,如果s?f（k,d）（10）1,则一定可以找到一个唯一可满足的d-正则（k,s）-CNF公式。另外,我们还提出一种从k-SAT问题到d-正则（k,s）-SAT问题的简约归约（parsimonious reduction）,能在k?3、s?f（k,d）（10）1和（s（10）d）/2（29）k-1的条件下,把任意一个k-CNF公式转换为一个SAT等价的d-正则（k,s）-CNF公式,并使得归约前后两个公式的解的数目保持不变。这种归约方法添加了大量的新变元和新子句,虽没有改变解的个数,但解空间却明显被扩大,同时子句约束密度也被调整到s/k。这不仅说明这个简约规约稀释了公式的解,使得公式难以求解,而且说明仅用子句约束密度不足以刻画公式求解的难易程度。（3）研究了几类特殊（1,0）-SAT问题的临界现象。（1,0）-超解能够满足公式中每个子句的至少2个文字,使得当任一变元的值被翻转后仍能满足这个公式。判定一个给定的CNF公式是否有（1,0）-超解的问题,被称为（1,0）-SAT问题。通过分析（k,s）-CNF公式、正则（k,s）-CNF公式、d-正则（k,s）-CNF公式的结构特征,给出关于（1,0）-超解存在性的一些结论。通过设计一些多项式时间的归约方法,证明了在k（29）3时,（1,0）-（k,s）-SAT问题和（1,0）-正则（k,s）-SAT问题存在临界现象,且临界函数一致;在k（29）4时,（1,0）-d-正则（k,s）-SAT问题也存在临界现象。此外,通过分析这些特殊公式的结构特征,给出这些临界函数的一些性质。