基于任务分配与调度的GSAT算法求解3-SAT问题

付慧敏,徐 扬，何星星,宁欣然

(1.西南交通大学信息科学与技术学院，四川 成都 610031；2.西南交通大学系统可信性自动验证国家地方联合工程实验室,四川 成都 610031)

1 引言

1971年Cook证明了SAT(SATisfiability)问题是NP完全问题，具有广泛的实际应用。许多学者将一些组合问题例如人工智能、超大规模集成电路VLSI(Very Large Scale Intergration)设计、积木世界规划、Job shop排工等转化为SAT问题来求解[1]。经过国内外学者的努力，求解SAT问题的优化算法已经有很多，总体分成两类：一是完备的方法，适应于应用类问题和组合问题，例如基于DPLL(Davis Putnam Logemann Loveland)的SATO(SAtisfiability Testing Optimized)[2]、BerkMin(Berkeley-Minsk)[3]、CDCL(Conflict-Driven Clause Learning)[4]等。其优点是对于任意SAT问题都能正确地判断其可满足或者不可满足，缺点是随着问题规模的不断增大，其解空间的复杂度成指数增长，计算效率很低，不适应于大规模问题[5]。二是不完备的方法，适应于随机生成问题。虽然对于任意SAT问题不能都正确地判断其可满足或者不可满足，但是对于可满足SAT问题其效率整体上超过完备的方法，因此受到很多学者的青睐，使得这种方法得以快速地发展。例如，MP(Message Passing)算法[6]、Local Search算法[7]、遗传算法[8]、不完备算法之间的结合[9,10]、组织进化算法[11]、多智能体社会进化算法[5]、GSAT算法[12,13]、完备算法和不完备算法相结合的混合算法[14]等。

GSAT算法是一个很有效的局部搜索算法，其主要的技术是贪心搜索，即通过一系列的搜索得到问题的最优解，而每一次搜索都是当前状态下某种策略的最好选择。早期在求解SAT领域中，贪心搜索很容易陷入“早熟”，Selman等人[15]用WalkGSAT的局部搜索算法跳出局部最优，大量的实验表明这个技术很适应于随机生成的3SAT问题。……