SAT+MiniSAT三元可满足性问题的研究与实现
本论文运用两个工具：自行编写的SAT生成器和现成的MiniSAT解决器将SAT通过计算机生成并解答，从而得出解答结果，最后并对解答结果进行验证来进一步确定实验的准确性。
关键字：三元可满足性问题； SAT； MiniSAT；5057
毕业论文设计说明书（论文）外文摘要
Title The study and realization of 3SAT
Abstrack： In computing language,there are a lot of relational operations,and the most popular of which is logic operations.In order to know more about the logic operations,I choose the topic as my essay:Satisfiability.In the process of studying, we can learn to build the test bed of SAT,and we can also learn to solver the SAT with SAT Solver.
There are two tools of this paper:SAT Creater and SAT Solver.In this paper,I use this two tools to create a test bed of SAT and solve them,in the process of creating and solving,by solving the possible situations of them,I get the conclution and I also test the conclution so as to make sure that it is ture.
Keywords: SAT;MiniSAT
目 次
1 绪论 3
1.1 SAT的概念 3
1.2 SAT的应用领域简介 3
1.3 论文结构 4
2 SAT生成器的特性以及运行环境 4
2.1 生成器代码简介 4
2.2 生成器运行环境 5
2.3 生成器操作及结果 8
3 SAT解决器（SAT Solver） 9
3.1 SAT解决器的选择及特点 9
3.2 SAT解决器工作原理 10
4 SAT的可解性研究 12
4.1 前期操作步骤 12
4.2 第一步（确定存在极点） 14
4.3 第二步（缩小极点选择范围） 16
4.4 第三部（确定极点） 17
4.5 第四步（结论） 18
5 SAT解答时间复杂性研究 19
5.1 固定变量个数，研究时间与k的关系 19
5.1.1 假设v=100 19
5.1.2 假设v=200 22
5.1.3 假设v=300 23
5.1.4 三组数据的结果 24
5.2 固定k值，研究时间与变量个数的关系 26
6 补充验证 29
6.1 数据验证 29
6.2 运行环境的验证 30
7 总结 31
8 结 论 33
9 致 谢 34
10 参 考 文 献 35
1 绪论
可满足性（英文：Satisfiability）是用来解决给定的布林方程式，是否存在一组变量赋值，是问题可满足，布林可满足性问题（SAT）是属于决定性问题，是第一个被证明的NP完全问题。在众多的NP完全问题中，SAT被称为其他问题的“种子”。