1.引言

1.1课题背景与意义

课题背景：

命题逻辑公式的可满足性问题（SAT）是数理逻辑、计算机科学、集成电路设计与验证和人工智能等领域中的核心问题，并且是第一个被证明出来的NP完全问题。

从1960年至今，SAT问题一直备受人们的关注，世界各国的研究人员在这方面都做了大量的工作，提出了许多求解算法。每年可满足性理论和应用方面的国际会议都会组织一次 SAT竞赛以求找到一组最快的SAT求解器，而且会详细展示一系列的高效求解器的性能。国内也经常会组织一些SAT竞赛及研讨会，这些都促进了SAT算法的飞速发展。尽管命题逻辑的可满足性问题理论研究已趋于成熟，但在SAT求解器被越来越多地应用到各种实际问题领域的今天，探寻解决SAT问题的高效算法仍然是一个吸引人并且极具挑战性的研究方向。