求解SAT问题的分级重排搜索算法

MULTI-STAGE SEARCH REARRANGEMENT ALGORITHM FOR SOLVING SAT PROBLEM

局部搜索法在ＳＡＴ问题上的成功运用已引起越来越广泛的重视，然而，它在面对不可满足问题例时的局限性不能不被考虑．分级重排搜索算法ＭＳＲＡ（ｍｕｌｔｉ－ｓｔａｇｅｓｅａｒｃｈｒｅａｒｒａｎｇｅ－ｍｅｎｔａｌｇｏｒｉｔｈｍ）正是为克服局部搜索法的不完备性而提出的，准确地讲，它是几种算法在思想上的集成，但为明确起见，把其最典型的分级重排过程作为名称．分级重排搜索算法在求解ＳＡＴ问题时，能表现出优于单一求解策略（如局部搜索法或回溯算法）的明显特性．由于可根据约束条件的强弱来估计ＳＡＴ问题例的可满足性，因此能够以此来确定更有效的求解策略．

Recently,local search method has been successfully applied to solve large scale SAT problem,but it will fail to find solution when an original SAT problem instance is unsatisfiable.MSRA(multi-stage search rearrangement algorithm)is just proposed to overcome the incompleteness of local search method.Properly speaking,MSRA is based on the'separate and conquer'strategy and is the integration of several algorithms While solving the SAT problem,MSRA is more efficient than a single method,such as local search and backtracking method.Since the satisfiability of a SAT problem instance can be estimated by the strength of constrained conditions,the authors could find a more efficient strategy to solve the instance.