A Structural Approach to Reasoning with Quantified Boolean Formulas

In this paper we approach the problem of reason- ing with quantified Boolean formulas (QBFs) by combining search and resolution, and by switch- ing between them according to structural proper- ties of QBFs. We provide empirical evidence that QBFs which cannot be solved by search or resolu- tion alone, can be solved by combining them, and that our approach makes a proof-of-concept imple- mentation competitive with current QBF solvers.