On QBF Algorithms and Calculi

The immense success of SAT solvers motivates us to investigate solving of even harder decision problems. In this sense, Quantified Boolean Formula (QBFs) can be seen as a natural successor of SAT. QBFs, as a PSPACE-complete problem, provide us with a much stronger formalism but at the same time, represent a much more difficult computational challenge. In this talk we will look at QBF from both practical and theoretical perspective. First we will discuss an algorithm that solves QBF by a gradual expansion to SAT and invokes a SAT solver in a blackbox fashion. In the second part of the talk we will look at a calculus that corresponds to this solver and calculi that represent different existing solving techniques. We will show that these calculi can be exponentially separated while reusing some well-known results from circuit complexity.