Abstract
Many application problems from artificial intelligence, verification, and formal synthesis can be efficiently encoded as quantified Boolean formulas (QBFs). QBF solvers automatically find solutions to the QBF representations of problems. These solutions to the QBF representations can then be mapped to solutions to the respective original problems.
Over the last years much progress has been made concerning the theory and practice of QBF solving technology. In this talk, we review two successful solving paradigms of orthogonal strength and their formal characterizations in terms of proof systems: Search-based QBF solving is based on Q-Resolution and expansion-based QBF solving is founded on the forall-Exp-Res proof system.