| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| Chapter 1 Introduction | 第11-16页 |
| ·Research Background | 第11-12页 |
| ·Current Research Statuses | 第12-14页 |
| ·Structure of This Paper | 第14-16页 |
| Chapter 2 Preliminaries | 第16-24页 |
| ·CNF Formula | 第16-17页 |
| ·Directed Hypergraph | 第17-20页 |
| ·Graph Reduction Operations | 第20-21页 |
| ·Hypergraph Reduction Operations | 第21-23页 |
| ·Summary | 第23-24页 |
| Chapter 3 A New Directed hypergraph for CNF Formula | 第24-42页 |
| ·Representation | 第24-29页 |
| ·One-to-one Correspondence | 第29-38页 |
| ·Extended B-graph associated with Horn Formula | 第38-41页 |
| ·Summary | 第41-42页 |
| Chapter 4 Redundancy of CNF formula | 第42-54页 |
| ·Absolute Redundant Variable | 第42-45页 |
| ·Subsumed Clause | 第45-47页 |
| ·Clauses with Strong Resolvent | 第47-53页 |
| ·Summary | 第53-54页 |
| Chapter 5 New Reduction Operations | 第54-62页 |
| ·Reduction Operations | 第54-57页 |
| ·Instantiation | 第57-61页 |
| ·Summary | 第61-62页 |
| Conclusions and Future Work | 第62-63页 |
| Acknowledgements | 第63-64页 |
| Reference | 第64-69页 |
| List of Publication and Research Project | 第69页 |
