Alladi Ramakrishnan Hall

Pebble Games, Resolution and Some Lower Bounds

Aditi Dudeja

IMSc

In this thesis, we study a simple proof system called resolution, that is complete and sound for the language of all unsatisfiable CNF formulas.

We first explore the motivations behind the study of proof complexity and resolution. We then discuss pebble games and give a lower bound on the pebbling price of a special class of graphs. The rest of the thesis discusses some important lower bound and trade-off results in resolution that use pebble games as an important tool. Finally, we survey a non-trivial upper bound on the size of tree-like resolution.