Quantified Boolean Formulas: Proof Complexity and Models of Solving