Proof complexity and complete algorithms for NP-hard search problems

The methods of propositional proof complexity, particularly 
those concerning resolution complexity, enable one to prove 
exponential lower bounds on the running time on random inputs 
of complete algorithms for a number of NP-hard search problems.  
We will give an overview the methods underlying these results, 
concentrating on satisfiability, coloring, and independent set 
problems.  Although most of the results apply to random instances 
at densities above the thresholds for which solutions exist with 
non-neglible probability, we will also sketch how these may be 
extended in certain cases to algorithms running on instances 
below these thresholds.