A structural approach to reasoning with quantified Boolean formulas