摘要：求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值，成为近年来的研究热点。本文针对命题公式与一阶公式的可满足性问题，重点介绍了布尔可满足性与可满足性模理论求解技术的基本原理，并且根据算法的类型进行分类阐述，分析了各种算法的优缺点。最后，讨论了目前面临的主要挑战，对今后的研究方向进行了展望。

关键词：布尔可满足问题 可满足性模理论问题 完全方法 不完全方法 

单位：国防科学技术大学计算机学院 湖南长沙410073