SAT问题(Satisfiability problem)，是第一个被证明的NPC(Non-deterministicPolynomial Complete)问题，在计算机科学理论和应用中具有重要的意义。对于理论研究，它是计算复杂性理论的奠基石，所有的NPC问题都可以在多项式时间内转化为SAT问题。对于工业应用，SAT可用于解决等价性验证、有界模型检测、电子设计自动化、统计物理学等多方面问题。因此，高效实用的SAT算法和技术是目前研究的热点。局部搜索算法是目前求解SAT问题比较有效的算法，Sattime算法是典型的局部搜索算法，曾在2011年的SAT问题国际求解大赛中获得随机类型算例组的银牌。它是基于Novelty系列的算法，在选择翻转变元时它利用了子句满足的历史信息，对其求解过程进行行为分析与模式挖掘可以发现变元与子句间蕴含的因果关系。建立数据库记录局部搜索算法的求解行为，对翻转事件进行数据挖掘，包括关联规则模式挖掘和频繁序列模式挖掘。通过对挖掘结果进行分析，发现Sattime算法有时会出现先后选择同一个变元的现象，这种现象可能使搜索过程产生回环。从而提出两种概率控制策略：加强子句选择策略和加强变元选择策略。将这两种策略应用到Sattime算法中，形成新的局部搜索算法Sattime-P。使用Sattime算法和Sattime-P算法对不同类型的算例进行求解，对比它们的平均翻转次数、平均求解时间。实验结果表明使用改进策略的Sattime-P算法在大多数情况下减少了平均翻转次数，提高了求解效率。