In this talk I will review the recent progress in the solving of Quantified Boolean Formulas (QBF). The initial research on QBF solving focused on extending SAT technology. However, in the recent approaches SAT solvers are used in a black-box fashion and the search space is pruned by stronger constraints than just clauses. The study of QBF has also revealed a number of limitations of the existing technology. Recent results show that some of these limitations can be tackled by applying Machine Learning at the semantic level.