可满足性问题是第一个NP完全问题,在计算机辅助设计、人工智能、密钥攻击、电子设计自动化、规划等领域有着广泛的应用。目前还没有一个SAT求解器可以有效求解所有SAT问题,仍有大量的问题未被解决。SAT求解器大致可以分为两大类：一类是基于DPLL的；另一类是基于局域搜索的。基于DPLL的SAT求解器又可以进一步分成前向型和冲突驱动型两种。其中前向型在求解随机类不可满足性问题和手工类问题上表现出色,冲突驱动型在求解应用类问题上占据主导,而基于局域搜索的在求解大的随机类可满足性问题上表现很好。由于不同求解器擅长求解不同的问题,本文引入了轮廓特征的策略。希望通过模型寻找最优求解器的思路构造出一种通用性的SAT求解器。其中回归分析模型建立了实例特征和求解器执行时间的关系,计算出待解问题的特征就可以估算出其执行时间,进而选择执行时间最短的求解器作为最优求解器去求解。DCM模型以求解器的行为作对象,执行输出作特征,求解出每个求解器的执行概率,从而选择执行概率最大的求解器作为最优求解器去求解。最后将回归分析模型和DCM模型相结合,先由回归分析模型粗选出一组较优求解器,再由DCM模型细选出其中执行概率最大的作为最优求解器去求解。实验表明轮廓特征算法可明显提高了SAT求解器的解题数量。求解问题数量上混合模型大于DCM模型,DCM模型大于回归分析模。再从执行时间上看,对于简单的问题,混合模型和回归分析模型相当,都优于DCM模型,对于复杂的问题,混合模型和DCM模型相当,都优于回归分析模型。总体上讲混合模型集成了两种模型的优点,无论从解题数量还是执行时间上看,它都略胜于前面两者。