基于回归分析和DCM模型的可满足性问题求解算法

摘要

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

目录

声明

东华大学学位论文版权使用授权书

摘要

第1章 可满足性问题的背景

1．1 可满足性问题的定义

1．2 可满足性问题的研究现状

1．3 可满足性问题的应用及意义

第2章 可满足性问题的各种求解算法

2．1 DPLL算法

2．1．1 冲突驱动型DPLL算法

2．1．2 前向型DPLL算法

2．2 局部搜索算法

2．3 轮廓特征求解算法

第3章 基于回归分析的求解算法

3．1 回归分析算法

3．2 回归分析模型求解器的构造

第4章 基于DCM模型的求解算法

4．1 DCM模型结构

4．2 DCM模型求解器的构造

第5章 两种模型混合的求解算法

5．1两种模型混合算法

5．2 两种模型混合求解器的构造

第6章 实验研究

6．1 实验环境

6．2 实验结果分析

第7章 总结展望

7．1 轮廓特征求解算法的总结

7．2 未来研究工作展望

参考文献

附录1 回归分析模型的回归系数

作者在研究生期间的研究成果

致谢