利用近似解加速求解SAT问题的启发式完全算法  

A Heuristic Complete Algorithm for SAT Problem by Approximation Solution

作　　者：荆明娥[1] 周电[1,2] 唐璞山[1] 周晓方[1] 

机构地区：[1]复旦大学专用集成电路国家重点实验室 [2]Electronic Engineering Department,the University of Texas at Dallas,Dallas,TX75083 USA

出　　处：《计算机辅助设计与图形学学报》2007年第9期1184-1189,共6页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金(90307017;60176017;90207002);中国博士后科学基金(KLH1202005);上海市自然科学基金(06ZR14016).

摘　　要：结合DPLL完全算法能够证明可满足性(SAT)问题的不可满足性和局部搜索算法快速的优点,提出利用近似解加速求解SAT问题的启发式完全算法.首先利用局部搜索算法快速地得到一个近似解,并将该近似解作为完全算法的初始输入,用于其中分支变量的相位决策.该算法引导完全算法优先搜索近似解所在的子空间,加速解决器找到可满足解的过程,为SAT问题的求解提供了一种新的有效途径.实验结果表明,该算法有效地提高了决策的精度和SAT解决器的效率,对很多实例非常有效.The advantages of complete algorithm integrated into an algorithm. First, an approximation initial input of the complete algorithm, which is used and incomplete algorithm of the SAT problem are solution is obtained by an incomplete algorithm, as an to phase decision of branched variable. The algorithm guides the complete algorithm first search the subspace that the approximation solutions lie in, which accelerates the process that the solver find the satisfied solution and provides a new approach for SAT problem. Experimental results show that proposed algorithm improves the decision precision and the efficiency of solver and performs well in many instances.

关 键 词：SAT问题 完全算法 局部搜索 变量决策 

分 类 号：TN407[电子电信—微电子学与固体电子学]