命题逻辑中的可满足性问题（Satisfiability Problem,SAT）是计算机科学理论和实践中的一个基本问题。SAT问题的可满足性在于确定是否可以通过为其布尔变量赋值满足给定的公式。在理论方面,SAT问题求解被应用于组合优化、统计物理、计算理论等领域;在实际应用方面,SAT问题求解被广泛应用于计算机代数系统、核心图、基因调控网络、系统（软件和硬件）自动验证、电路验证、基于模型的诊断和机器诱导等。因此,研究求解SAT问题的高效算法有着重要的理论意义和应用价值。求解SAT问题的算法主要分为完备算法和不完备算法两类。随机局部搜索（Stochastic Local Search,SLS）算法是不完备算法中最重要的一种算法,有许多突破性不完备算法均基于局部搜索算法。本文针对研究基于SLS算法,在初始赋值、变量选择、子句选择方面提出了新的策略,并基于这些策略研发了不同版本的SLS SAT求解器。通过实验评估,将所研发的不同版本的SLS SAT求解器与同类求解器及国际上最先进的求解器进行比较,结果表明采用了新策略的求解器具有较明显的优势。特别是以历年SAT问题竞赛例为基准测试例进行对比分析,进一步证实了研发的基于一系列的新方法和新策略的SLS SAT求解器的先进性。在SLS算法的初始赋值策略上,通过分析SAT问题固有的属性,提出了分配策略、满足度（Satisfaction degree,Sd）和初始概率分布,有效地优化了SLS求解器搜索的方向。通过实验分析了基于初始概率分布的分配策略对于改进SLS求解器求解一致随机k-SAT（Uniform Random k-SAT,URS）问题的性能是有效的。在SLS算法的变量选择策略上,通过分析Walk SATlm求解器求解URS问题的搜索轨迹,提出了一种拟合求解器搜索行为的新技术（基于拟合函数Boltamann）。研究了基于Boltamann函数的概率选择策略,通过分析当前基于概率选择的SLS求解器中的变量选择策略采用多项式函数和指数函数的方法,提出了3种有效的基于概率的变量选择策略,分别称为基于伪正态函数的策略、基于伪正态多项式函数的策略和基于多项式伪正态函数的策略,有效地优化了基于概率选择的SLS的路径搜索。通过实验分析了不同变量选择策略在基于概率选择的SLS算法中的有效性。SAT问题的来源非常广泛,在不同类型的SAT实例上同一种SAT算法的求解效率一般存在较大的差异。国际上,在求解URS问题上已有一些非常先进的SLS求解器,然而它们在难随机SAT（Hard Random SAT,HRS）问题上都没有任何优势。在SLS算法的子句选择策略上,为了倾向于选择频繁变为不满足或容易保持可满足的不可满足子句,提出了两种全局的子句重要因子分配方案和二级偏随机游走策略;在SLS算法的变量选择策略上,提出了用于评估变量的线性函数;基于子句选择策略和变量选择策略,发展了一种SLS算法（命名为BRSAP）,该算法在求解HRS问题上的性能超过了2016年、2017年和2018年SAT国际竞赛随机组的冠军求解器,并且可以有效地求解具有长子句的URS问题。研究了基于强调翻转变量的启发式策略,通过分析SLS求解过程中的搜索决策,提出了基于强调翻转变量的偏随机游走策略和基于强调翻转变量的打破平局策略,并将其用于改进Prob SAT算法,提出了一种基于强调翻转变量的SLS算法（命名为EPEFV）。将EPEFV算法与国际顶级的SLS求解器和完备求解器在求解HRS问题和具有长子句的URS问题上的性能进行比较。实验结果表明,EPEFV的性能优于2017年和2018年SAT国际竞赛随机组的冠军求解器以及2018年和2019年SAT国际竞赛main组的冠军求解器。研究了基于选择属性的启发式策略,在SLS算法的子句选择策略上,提出了一种子句重要因子分配方案和偏随机游走策略;在SLS算法的变量选择策略上,提出了一种变量重要因子分配方案和配置检查（Configuration Checking,CC）策略的变体,发展了一种基于选择属性的SLS算法（命名为Select NTS）。将Select NTS与国际顶级的SLS求解器和完备求解器在求解HRS和URS问题上的性能进行比较。实验结果表明,在整体性能上,Select NTS超过了2016年、2017年和2018年SAT国际竞赛随机组的冠军求解器,并且讨论了Select NTS、EPEFV和BRSAP的主要区别:在HRS实例上Select NTS建立了最先进的标准且EPEFV的性能优于BRSAP,并且在不同类型的URS实例上这三种求解器都有各自的优势,以及通过理论和实验分析了在这三种求解器中不同属性之间的关系。