可满足性问题(Boolean Satisfiability Problem,简称SAT)是一个关于判断一个布尔表达式是否可为真的问题。而布尔表达式都可以转换成或与表达式(Conjurictive Normal Form,简称CNF)。本文介绍的是作者在SAT问题算法方面的一些研究,以及对于通过简化CNF来提高解决SAT问题的效率的策略。在实际应用中,可满足性问题有许多应用,例如在电子设计自动化(Electronic Design Automation,简称EDA)中,形式验证(FormalVerification)验证逻辑电路等效性就常将可满足性算法作为引擎。由于逻辑电路的复杂度高,且重复性也比较高,本文尝试利用布尔表达式的蕴含和化简公式来简化CNF的方法以提高SAT解决器的效率。程序用C++及STL标准模板库编程实现,将原始的CNF式转化成简化后的CNF,再使用zchaff解决新的CNF式来提高SAT解决器的效率。实验结果显示简化程序成功地简化了CNF式,简化及Zchaff解决新CNF式的总时间消耗小于使用Zchaff直接解决原CNF的时间。