一个求解结构SAT问题的高效局部搜索算法

AN EFFICIENT LOCAL SEARCH ALGORITHM FOR STRUCTURED SAT PROBLEMS

逻辑表达式可满足性（SAT）问题是第一个被证明的NP完全问题．它也是解决人工智能和计算理论中许多实际问题的基础．人们发现，对于某些类型的SAT问题，局部搜索算法要比一些传统的算法（例如Davis－Putnam过程）更为有效．在本文中，我们主要讨论如何用局部搜索算法求解结构SAT问题．我们对一个典型的局部搜索算法GSAT＋walk做了改进与扩展．首先，我们除去了GSAT＋walk中GSAT部分的“平移”；其次，我们给每一个子句赋权，并在GSAT＋walk的搜索过程中动态地调整子句的权．文中给出的实验结果表明改进后的新算法对于求解结构SAT问题非常有效．

Satisfiability (SAT) problem is the first problem that was proved to be NP--complete. Itis fundamental to solving many problems in artificial intelligence and computational complexitytheory. Recently, it was shown that local search methods can outperform many traditional algorithmson some large classes of SAT problems. This paper proposes two modifications to GSAT+walk, atypical local search method. First, 'sideways moves' from the GSAT part of GSAT+walk areremoved; second, each clause is associated with a weight, and the weights are dynamically updatedduring the entire course of the search. Experimental results indicate that the new local searchalgorithm is very efficient in solving many structured SAT problems.