文摘
英文文摘
Chapter 1. Introduction
1.1 Motivation
1.2 Main work and future work
1.3 Organization of the thesis
Chapter2. SAT Problem
2.1 Propositional logic
2.2 Basic definitions
2.3 The complexity of SAT
2.4 Algorithms for SAT
2.4.1 Introduction
2.4.2 Algorithm for 2-SAT
2.4.3 DPLL algorithm
2.5 Recent research on SAT
Chapter3. Minimal Unsatisfiable Formulas
3.1 Basic definitions
3.2 Important statements on MU formulas
3.3 Representation of formulas in MU(1)
3.4 Four important minimal unsatisfiable formulas
Chapter4. Reducing CNF to 3-CNF
4.1 Several lemmas
4.2 An existing algorithm
4.3 Our new algorithm
4.4 Complexity of the algorithm
Chapter5. Reducing k-CNF to t-CNF (3 ＜ t ＜ k)
5.1 Our algorithm
5.2 Complexity of the algorithm
Acknowledgements
Bibliography
Publications
原创性声明及关于学位论文使用授权的声明
贵州大学;
