Contents

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