Abstract Branching for Quantified Formulas

We introduce a novel search-based decision procedure for Quantified Boolean Formulas (QBFs), called Abstract Branching. As opposed to standard search-based procedures, it escapes the burdensome need for branching on both children of every universal node in the search tree. This is achieved by branching on existential variables only, while admissible universal assignments are inferred. Running examples and experimental results are reported.