在计算机科学的许多领域，可满足性问题(SAT)都是一个重要的研究课题。SAT是一个NP完全问题，但在各种领域都需要快速算法来解决规模较大的问题，比如在人工智能中比较突出的规划问题、约束满足问题、地图着色问题等。但是要找到一个对所有类型的SAT问题实例都有效的完全算法不太现实，所以研究热点较多的集中在局部搜索算法上。 本文主要研究求解SAT问题的快速局部搜索算法。文章首先介绍了一个通用问题求解框架。该框架以SAT问题作为中间域，其它各类NP问题如规划问题等都可以先把问题转换为SAT问题，然后利用SAT问题的求解器进行求解，最后把求解结果转换到原问题域。然后文章系统地介绍了用局部搜索算法求解SAT问题的各种技术，并重点分析了GSAT、WalkSAT、Novelty、R-Novelty和UnitWalk等算法和各种跳离局部最优的策略。虽然各种局部搜索算法在实现细节上千差万别，但通用的搜索策略是一致的。算法开始时给公式F中的所有变量赋一个初始的真值，在每一搜索步骤中，有一个变量的真值被置反。这类搜索步骤也称为变量翻转。因为F的模型是使得F中所有子句都满足的赋值，变量翻转的目标是最小化目标函数，该函数是由赋值B到B下不满足子句数的映射。 本文在详细分析目前有代表性的局部搜索算法UnitWalk的基础上提出了一个改进算法Pre-UnitWalk。UnitWalk是一个用单元子句消解来指导局部搜索的算法。与其他局部搜索算法不同，UnitWalk在搜索过程中不仅修改当前解也修改输入公式。在2003年SAT求解器大赛中，UnitWalk在求解随机SAT问题中表现出最好的性能。我们对UnitWalk算法的结构进行分析，发现如果输入公式包含单元子句(实际应用问题往往包含单元子句)，那么这部分单元子句在搜索过程中将被处理很多次(每个周期都要处理一次)。基于以上分析，本文提出一个改进的UnitWalk算法Pre-UnitWalk。Pre-UnitWalk在UnitWalk的主过程开始之前加上一个预处理过程。在预处理过程中算法把输入公式包含单元子句全部消解，那么这部分单元子句以及由他们蕴含的单元子句只需要处理一次。这样算法主过程处理的将是更精简的公式：比原问题有更少的变量和子句。实验表明改进后的算法在解决cnf-ssa等实际问题方面较原算法有明显改进。 本文在分析另一个有代表性局部搜索算法SAPS的基础上提出了一个与SAPS相近的新算法RW-SAPS。放大与概率平滑算法(SAPS)是目前性能最好的动态局部搜索算法。通过对SAPS的加权搜索步骤的分析，一般认为SAPS选择变量过于贪婪：每次从出现在未满足子句中翻转后能使不满足子句总权重有最大减少的变量中随机选择。RW-SAPS算法在SAPS的基础上引入随机游动策略，即在加权搜索过程中以概率p从不满足子句中出现的变量中随机选择，以概率1-p采用SAPS中的选择策略选择变量。实验表明在VLSI设计问题、积木世界规划问题和Jobshop排工问题等实例上，RW-SAPS性能优于SAPS算法。