| Abstract | 第1-5页 |
| 摘要 | 第5-13页 |
| 1.Introduction | 第13-17页 |
| ·Background and motivation | 第14-15页 |
| ·Main work and future work | 第15-16页 |
| ·Organization of the thesis | 第16-17页 |
| 2.Preliminaries | 第17-27页 |
| ·Basic definitions and lemmas | 第17-19页 |
| ·DPLL algorithm | 第19-22页 |
| ·Resolution | 第22-24页 |
| ·Minimal unsatisfiable formulas | 第24-27页 |
| 3.Some NP-complete Instances in(r,s)-SAT | 第27-37页 |
| ·Constructions of minimal unsatisfiable instances in(r,s)-SAT | 第27-32页 |
| ·Tree-resolution proof of MU(k) formulas | 第28-31页 |
| ·Some minimal unsatisfiable instances in(r,s)-SAT | 第31-32页 |
| ·Some NP-complete Instances in(r,s)-SAT | 第32-36页 |
| ·Forcing of minimal unsatisfiable formulas | 第32-34页 |
| ·NP-completeness of (3,4)-SAT | 第34-36页 |
| ·Conclusion | 第36-37页 |
| 4.Transforming DPLL to (1,1)-resolution | 第37-47页 |
| ·Transforming DPLL to resolution | 第38-40页 |
| ·Transforming resolution to (1,1)-resolution | 第40-46页 |
| ·Conclusion | 第46-47页 |
| Acknowledgements | 第47-48页 |
| Bibliography | 第48-52页 |
| Publications | 第52-53页 |
| 原创性声明 | 第53页 |
| 关于学位论文使用授权的声明 | 第53页 |
