基于膨胀图的SAT算法

命题公式的可满足性问题是理论计算机科学和人工智能中的著名问题,判断命题公式可满足性的一个直接办法就是穷举法,但该方法计算量大,因此高效实用的SAT算法设计与分析一直是计算机科学界的研究热点。膨胀图是具有良好连通性的稀疏图,已引起了科学家们的关注,并广泛应用于证明计算复杂性理论的结论。本文在膨胀图的基础上,利用膨胀图来诱导SAT算法搜索的随机步,提出了一种新的SAT算法。经证明:新的SAT算法能够降低随机算法对随机位的依赖程度。