可满足性问题是被广泛研究的基本NP问题之一。电子设计自动化、人工智能、计算机科学、运筹管理等方面的许多问题都可以简化成可满足性问题，可满足性问题的算法上的改进也极大地促进这些相关领域的发展。 本文在研究、探讨可满足性问题算法及其实现技术的基础上，选择目前的主流算法——基于DPLL完全算法，针对其中很重要的组成部分——搜索决策方面作了深入的研究，提出了一种新的、高效的搜索决策策略，采用动静态排序相结合的策略可满足性问题解决器。 具体贡献是： 1)研究了静态排序对算法的贡献，针对静态排序的特点，采用了一种有效地体现实际问题特征的静态分析方法，根据变量正反文字出现次数的乘积，进行初始排序，优先考虑正反文字出现次数较多变量的赋值； 2)权衡比较了多种动态排序策略，采用一种既能及时反映算法过程中问题特征，动态更新排序，又不需耗费大量计算机资源的策略，给冲突子句中的变量活跃性因子增加一个随时间增大的变量，把变量顺序提到比它活跃性因子小的前面，体现了冲突驱动，并动态更新变量顺序，优先考虑发生冲突子句中变量的赋值，尽可能避免当前冲突； 3)把这两种不同的排序方法结合到一起，互相促进，弥补各自的缺陷，成功地提高了算法的速度。 实验表明：与采用其它决策策略的解决器相比，本文的解决器拥有一定的速度优势。