命题逻辑公式的可满足性问题(SAT)是数理逻辑、计算机科学、集成电路设计与验证和人工智能等领域中的核心问题,并且是第一个被证明出来的NP问题。SAT问题在计算复杂性理论中具有非常重要的地位,设计并实现解决该类问题的高效算法意义重大。但目前不存在一种求解算法在最坏情况下的时间复杂度是多项式级别,其求解速度仍是制约SAT算法发展的一大难题。因此,世界各国的学者都在努力研究新的求解算法,以寻求出一种高效的求解算法。SAT算法分为完备算法和局部搜索算法这两类。其中,完备算法能给出命题逻辑公式的解或证明公式是不可满足的,但是效率较低;而局部搜索算法求解速度相对较快,但是不一定能够找到对应SAT问题的解。本文在对比分析这两类算法的基础上,对DPLL算法进行了改进,并通过实验证明了改进后算法的优越性。基于上述思想,本文的研究工作主要包括:(1)深入分析了基于DPLL的完备性SAT算法的实现原理,给出了算法思想和详细的实现过程,并对该算法中所使用到的数据结构和一些关键技术(加速搜索的启发式策略、子句删除机制、随机重启动机制)给予总结和分析。(2)结合完备算法能够进行完备求解和局部搜索算法能够以较快速度进行求解的优点,在DPLL这一基本算法框架之上提出了一种混合的SAT求解器,将局部搜索算法WALKSAT作为一个必要步骤融入到DPLL算法的求解过程中。一方面,WALKSAT算法得出的近似解可以指导DPLL对决策变量进行赋值,从而减小对决策变量赋值的随机性和盲目性;另一方面,每当顶层变量的赋值确定后,都引入WALKSAT对算法进行加速,从而提高求解效率。(3)改进DPLL算法的整体框架和实现,给出了改进后算法的框架和实现步骤,并选取一些难的随机SAT实例对改进前后的算法进行了测试,实验结果表明,改进后的算法对于求解可满足的随机3-SAT实例效果显著。(4)将改进后的算法应用到图论中的实际问题--四色问题。问题通过编码转换为CNF公式的形式后,输入到改进后的DPLL求解器中进行求解,并最终转换为对应的着色方案。实验表明,算法在极短的时间内就得出了四色问题的解。
