基于加强概率控制策略的SAT局部搜索算法

来源：计算机工程与应用杂志2017年第14期北京时间：

作者：洪剑珂1，张峥华2，许贵平2

单位：1.北京林业大学 信息学院，北京 100083；2.华中科技大学 计算机学院，武汉 430074

摘要：局部搜索算法是目前求解SAT问题比较有效的方法，而Sattime算法是在SAT国际大赛中获得大奖的一种典型局部搜索算法。在Sattime算法的求解过程中，记录变元翻转事件流数据库，通过数据分析与模式挖掘，发现Sattime算法的局部搜索行为中会出现相邻搜索步选择同一个变元的现象，即所谓的回环现象，从而降低了求解效率。为解决此问题，提出两种概率控制策略：加强子句选择策略和加强变元选择策略，并将这两种策略应用到Sattime算法中，形成新的局部搜索算法Sattime-P。实验结果表明，与Sattime算法相比，改进后的Sattime-P算法求解效率有显著的提升。该方法也对其他局部搜索算法的改进具有参考价值。

关键词：SAT问题,局部搜索,概率控制,子句,布尔变元