本文提出了基于警示传播的启发式极性决策算法(WPDP)，是一个完全算法，不但能够解决大部分难解可满足性实例，而且能够验证实例的不可满足性。它继承了Zchaff算法的基本特性，如快速布尔约束推理(BCP)、变量状态独立下降和(VSIDS)等，同时引入了变量极性决策，将WP算法得到的近似解作为变量极性决策，引导DPLL算法的搜索。从而有效降低了DPLL算法在搜索过程中的冲突次数，加速了算法的搜索速度，提高了算法的效率，而且本算法还可解决WP算法原本无法解决的难解可满足性实例。在此基础上，接着提出了两个类似的启发式极性决策算法：基于信念传播的启发式极性决策算法和基于聚类排序选择的启发式极性决策算法。基于信念传播的启发式算法，是利用信念传播算法(BP算法)得到一组近似解，作为DPLL算法的变量极性决策，指导DPLL算法的搜索。而基于聚类排序的启发式算法，是利用遗传算法能够快速得到可满足性公式解这一特性，并加入了聚类排序选择算子，得到一组近似解作为DPLL算法的变量极性决策，指导DPLL算法有效搜索。这也是一个完全算法，能够有效给出不可满足性实例无解的证明，弥补了遗传算法不能有效给出不可满足性实例解的缺陷。实验表明，这几种启发式极性决策算法能够解决目前很多算法无法解决的难解实例。而且，其性能明显优于同类算法。本文的主要创新点有：　　1.对大量的已有算法进行分析，在此基础上归纳出了原有算法的不足之处，提出了一个更为有效的解决可满足性问题的完全算法（WPDP）。　　2.提出了WP算法在某些实例集上不收敛时的改进策略，通过定义两次迭代的距离，给出了一个简单的回溯方法，得到一组近似解，作为DPLL算法的启发式变量极性决策。　　3.在WPDP算法的设计基础上，提出了一个基于聚类排序选择的启发式极性决策算法。