论文部分内容阅读
命题可满足性问题(SAT)是判定一个给定的CNF形式的命题逻辑公式是否存在可满足的赋值的问题。SAT问题是数理逻辑、人工智能和理论计算机科学中的核心问题,也是解决许多实际问题的基础。因此研究和改进SAT问题的求解算法不仅具有重大的理论意义,而且应用前景广阔。对于某些类型的SAT问题,局部搜索算法比一些完备搜索算法更为有效。
通过对现有SAT局部搜索算法的研究,本文发现这些算法使用的前看一步策略存在贪心程度不够的问题。为了加强SAT局部搜索的贪心程度、减少翻转次数从而提高算法的求解能力,本文在前看一步策略的基础上提出了一种改进策略——前看两步策略——对算法中翻转变量的选取方法进行改进。前看一步策略和前看两步策略共同组成了本文的前看两次策略。将前看两步策略应用于WalkSAT算法类中的WSAT、TSAT和Novelty对它们进行改进,产生了三组新的算法变体WSAT_AT、TSAT_AT和Novelty_AT。然后程序实现了这些改进算法。为了验证前看两步策略对现有算法的改进效果,本文在多个不同规模的均衡3-SAT实例、两种不同规模的结构SAT问题实例以及几个利用相变现象构造的难解SAT实例上进行了实验。实验结果表明:改进后的算法的求解能力和收敛速度不同程度地优于对应的现有算法。
由于本文提出的前看两步策略不是和WalkSAT算法很相关,所以该策略也可以用于对其它SAT局部搜索算法的改进,并对其它领域的局部搜索算法的改进具有一定的参考价值。