可满足性问题(简称SAT问题)是NP-hard问题，它是当前运筹学、人工智能和计算机科学的热点领域，解决SAT问题具有突出的理论价值和应用价值。解决SAT问题的传统算法往往要占用很长时间和大量的内存，而最后往往还不能得到满意的结果。为了提高SAT问题解决算法的性能，本文对于SAT问题做了对已有算法的分析研究、约束规划算法分析、约束规划算法的UML建模和约束规划算法来求解SAT问题的实验分析等方面的探讨，主要的内容有：对SAT问题已有的主要算法及存在的问题进行了研究，总结了提高算法性能和跳出局部陷井所用的策略或机制。对局部搜索算法的实验分析，针对局部搜索算法的灵活性、随机性和参数化等特点，深入探讨了相应的算法实验分析所涉及的算法性能度量、性能比较和参数调优等基本问题。提出了综合人工智能中一致性算法和启发式搜索算法，采用约束推理的方法的约束规划算法。本文通过对约束规划算法事件触发机制的分析和UML的建模，从而提高了搜索效率，提出了解决SAT问题。结合SAT问题特殊知识，提出了在启发式算法和一致性算法的基础上，采用整数有限域的优化和搜索策略，对非线性约束问题在其内部制作二叉树进行搜索的约束规划算法，描述了first_fail的分支策略设计和算法描述，提供了性能比较、参数优化等等多种目的的实验结果。实验结果表明约束规划算法能有效解决SAT问题和显著提高性能。