可满足性(SAT)问题一直是电子设计自动化和人工智能领域的一个热点研究问题,因为它在这些领域有着非常广泛的应用。长期以来,人们对此进行了深入地研究,提出了很多解决可满足性问题的算法,其中最为流行的要数DPLL算法。基于DPLL算法,有很多的解决器被开发出来,ZCHAFF就是其中最著名的解决器之一。在这篇文章中,我们介绍了可满足性问题的应用及其经典算法,并着重研究了DPLL算法的决策过程。本文在决策过程中考虑了给定的CNF描述中子句长短不同的问题,采用子句加权改善决策策略。实验表明,对于那些CNF子句长短不一的SAT问题,子句加权后的决策策略能有效提高解决器的性能。在一些例子上,采用子句加权后的解决器,运行时间比ZCHAFF要快几十到几百倍,甚至能解决一些ZCHAFF当前无法解决的问题。