可满足性问题(Satisfiability problem问题,简称SAT问题)是第一个被证明的NPC(Non-deterministic Polynomial Complete)问题,它是计算复杂性理论的奠基石,是计算机科学与人工智能领域具有基础性的重要问题。同时,SAT问题在机器定理证明、VLSI超大规模集成电路设计与检测、模型检测、安全协议验证、任务规划调度等问题中有着广泛地应用。因此,对SAT问题的高效求解算法的研究具有重要的实用价值与理论意义。SAT问题的求解算法大体上可以分为不完备算法和完备算法,相对于完备算法,不完备算法能在更短的时间内求解更大规模的算例,虽然不保证一定能找到解,但是大部分情况下都能找到问题的解。不完备算法当中又以随机局部搜索算法SLS(Stochastic Local Search)求解效率最高。TNM(Two Noise Mechanism)算法是典型的随机局部搜索算法,在选择翻转变元时利用到了翻转过程中的历史信息,同时利用两种噪声机制使搜索过程跳出局部最优。利用程序插桩技术,建立数据库并记录搜索过程中的动态行为信息,对翻转事件进行统计分析,发现TNM算法会出现在一段时间内先后选择多个不同变元连续翻转的现象,这种现象使搜索过程产生行为环,降低了搜索效率。因此提出新的控制策略避免环的出现,将这种策略应用到TNM算法中,形成新的随机局部搜索算法TNM+。使用TNM算法和TNM+算法对不同类型的算例进行求解,对比它们的求解速度(包括平均翻转次数、平均求解时间)。实验结果表明,使用环避免策略的TNM+算法在大多数情况下减少了求解过程中地平均翻转次数,提高了执行效率。