可满足性问题(SAT)是第一个被证明的NP-完全问题，在人工智能和计算机科学中占据着重要的位置，许多问题都可以转化为SAT问题进行求解。最近杨洋等人提出了一种新的基于局部搜索的扩展规则方法ERACC(Extension Rule Based on Accurate Configuration Checking)，该方法突破了传统基于扩展规则方法对实例规模的局限。然而，ERACC在k-SAT(k＞3)实例上的表现有待进一步提高，因此本文提出了两种新的基于扩展规则的SAT问题求解方法。其次，随着SAT求解技术的发展，其扩展问题如MaxSAT问题、WPMS(Weighted Partial MaxSAT)问题、#SAT问题的研究也取得了很大的进展。在上述问题中，WPMS问题具有广泛的应用，譬如应用在相关的团问题上。团问题包含最大团问题，最大加权团问题，极大团枚举问题等。本文给出了一个极大团枚举的变种问题top-k极大加权团，即在给定图中寻找前k大极大加权团的加权团问题，并且提出了相应的求解算法。主要创新点如下：
　　（1）提出了新的基于扩展规则的SAT问题求解方法。首先在搜索由极大项组成的空间时，利用IMOM(Improved Maximum Occurrences on Clauses of Maximum Size)思想生成初始极大项。接着受CCA启发式思想的启发，设计了适用于扩展规则推理的CCA_ER(Configuration Checking with Aspiration for Extension Rule-Based Reasoning)启发式策略，为极大项中格局信息未发生变化的变量对应文字提供一定的翻转机会。然后对于可扩展当前极大项子句和不可扩展当前极大项子句，本文提出了一种新的子句权重更新策略PAWS_ER(Pure Additive Weighting Scheme for Extension Rule-Based Reasoning)。最后对于不可扩展的子句，本文给出变量的Subscore_ER属性并且提出了其衍生的CScore_ER和HScore_ER属性。其中，变量的Subscore_ER属性用于打破平局，即当有多个变量具有最大贡献值时，选择具有最大Subscore_ER值的变量。CScore_ER和HScore_ER分别用于贪心过程和随机过程翻转文字对应变量的选择。
　　（2）提出了基于局部搜索的top-k极大加权团问题求解方法。首先从输入图中分离出一个关键子图。该子图的顶点集为top-q度数顶点和其邻居组成。将该子图编码为WPMS问题，并利用WPMS相关技术求出top-k极大加权团。其次为了使算法更有效地寻找极大加权团，提出了一些新的策略并将其融入到算法中。新策略的主要过程为，如果当前有新增变量，以一定的概率p1选择新增的变量，如果当前有新增变量但概率不在p1或者没有新增变量，以一定的概率p2，从候选集Vm随机选择一个变量，其中，Vm为前m个在候选解中出现次数（赋值为1的次数）最少的变量组成的变量集，否则按照Dist的变量选择策略选择变量。最后扩大关键子图并进行迭代求解，其中扩大关键子图通过增大q的值实现，算法直到没有找到新的极大加权团或者达到最大翻转步数结束。
　　本文研究了SAT问题求解方法以及WPMS相关求解技术在top-k极大加权团上的应用，分别对上述两个问题的对应方法进行了测试。对于SAT问题实验结果：当给定的公式为k-SAT(k＞3)实例时，本文提出的ERACC_IAPS(ERACC with IMOM,CCA_ER,PAWS_ER and Subscore_ER)以及CERACC_IAPS(ERACC with IMOM,CCA_ER,PAWS_ER,CScore_ER and HScore_ER)的求解效率显著优于ERACC以及其它的基于扩展规则方法。与目前部分流行的局部算法对比，在一些实例上的求解效率也有一定优势。对于top-k极大加权团问题实验结果：为了适应top-k极大加权团问题，本文修改了4个极大团枚举算法Tomita、Hybrid、Degeneracy以及D2K算法。当给定的基准实例为DIMACS时，与修改后的算法相比，本文提出的算法在解的质量以及时间都明显优于其它的对比算法。