- 1 Introduction
- 2 Preliminaries
- 2.1 The DPLL Procedure
- 2.2 Proof Systems
- 2.3 Resolution
- 2.4 Clause Learning
- 2.5 Pebbling Formulas
- 2.6 The GTn Formulas
- 3 A Formal Framework for Studying Clause Learning
- 3.1 Unit Propagation and Decision Levels
- 3.2 Branching Sequence
- 3.3 Clause Learning Proofs
- 3.4 Implication Graph and Conflicts
- 3.5 Trivial Resolution and Learned Clauses
- 3.6 Different Learning Schemes
- 3.7 Fast Backtracking and Restarts
- 4 Clause Learning and Proper Natural Refinements of RES
- 4.1 The Proof Trace Extension
- 5 Clause Learning and General Resolution
- 6 From Analysis to Practice
- 6.1 Solving Pebbling Formulas
- 6.2 Solving GTn Formulas
- 6.3 Experimental Results
- 7 Conclusion
- Bibliography