SAT是理论计算机科学中的一个经典问题,也是被发现的第一个NP完全问题。SAT问题是对于给定的一个布尔逻辑表达式在SAT问题可满足的情况下给出一组解,使得该布尔逻辑表达式为“真”;在给定问题不可满足的情况下给出证明。比较著名的高效SAT求解算法有MiNiSat、zchaff、Grasp等。SAT求解算法广泛应用于实际生活中的各种领域,如电路设计的形式化验证、人工智能、资源调度等。虽然SAT求解算法的研究已经相当成熟,但它仍然是实际应用领域中必须打破的一个瓶颈。例如在电路设计的形式化验证中,将电路中的变量转化为布尔逻辑的合取范式形式(Conjunctive Normal Form简称CNF),再应用SAT求解来检测电路故障,传统算法往往要占用很长时间和大量的内存,而最后往往还不能得到满意的结果。所以到目前为止,众多国内外学者层出不穷的推出新型算法来提高计算效率,以便高效地应用于各行各业。虽然命题逻辑的理论研究已经相当成熟,但是在SAT问题及其算法被越来越多地应用到现实世界的生产和生活中的今天,探寻命题逻辑可满足性判定的高效算法仍然是一个令人兴奋的方向。SAT问题的解决方法一般分为两类:完备算法和不完备算法,它们的典型代表是Davis-Putnam提出的基于回溯搜索的DPLL算法和本地启发式搜索。当今流行的SAT算法主要是完备算法或在DPLL算法基础上的改进和衍生。本文在对现有的SAT问题相关理论的研究以及算法分析的基础上,基于DPLL算法结合集合理论提出了一种新型的SAT算法。具有高效的计算性能和空间利用率。主要内容包括对合取范式中布尔变量的集合划分,分支决策变量的选择策略,BCP过程的改进,冲突检测和回溯机制。在本课题中,作者参与了课题的理论研究与分析工作,并在老师的指导下完成了整体算法的设计与实现,并且进行了算法的对比测试以及在实际问题中的应用。