【摘要】 结合DPLL完全算法能够证明可满足性(SAT)问题的不可满足性和局部搜索算法快速的优点,提出利用近似解加速求解SAT问题的启发式完全算法.首先利用局部搜索算法快速地得到一个近似解,并将该近似解作为完全算法的初始输入,用于其中分支变量的相位决策.该算法引导完全算法优先搜索近似解所在的子空间,加速解决器找到可满足解的过程,为SAT问题的求解提供了一种新的有效途径.实验结果表明,该算法有效地提高了决策的精度和SAT解决器的效率,对很多实例非常有效.更多还原

【Abstract】 The advantages of complete algorithm and incomplete algorithm of the SAT problem are integrated into an algorithm. First, an approximation solution is obtained by an incomplete algorithm, as an initial input of the complete algorithm, which is used 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.更多还原