Parallel solving of quantified Boolean formulas

Abstract

Quantified Boolean formulas (QBFs) extend propositional logic by universal and existential quantifiers over the propositional variables. In the same way as the satisfiability problem of propositional logic is the archetypical problem for NP, the satisfiability problem of QBFs is the archetypical problem for PSPACE. Hence, QBFs provide an attractive framework for encoding many applications from verification, artificial intelligence, and synthesis, thus motivating the quest for efficient solving technology. Already in the very early stages of QBF solving history, attempts have been made to parallelize the solving process, either by splitting the search space or by portfolio-based approaches. In this chapter, we review and compare approaches for solving QBFs in parallel.