Logic seminar

Simulations in QBF Proof Complexity

Quantified Boolean Formulas (QBF) extend propositional formulas with Boolean quantifiers. Solving a QBF is PSPACE complete, and QBFSAT is seen as a natural extension of the SAT problem. Just as propositional proof complexity underlies the theory behind SAT solving, QBF proof complexity underlies the theory behind QBF solving. Here we will focus on the relative strengths of QBF proof systems via p-simulation.

On the surface QBF proof systems seem harder to compare to one another since they vary considerably in how they deal with quantification. In particular there's a vast difference between theory systems that generalise from propositional logic, the proof systems that capture the process of CDCL solving and the proof systems that capture the expansion and CEGAR based solvers. And many results do formally show an incomparability in the proof complexity between different systems as we suspect. However, there are a few non-obvious cases where a simulation is possible. In this talk we will examine the landscape of simulation in QBF, looking at the results over the last decade, as well as our own recent work with simulations based on strategy extraction and propositionalisation. We will interpret the theoretical and practical importance of these results.