Chapter 30. Reasoning with Quantified Boolean Formulas