For quantified Boolean formulas (QBF) there are two main different approaches to solving: QCDCL and expansion solving. In this paper we compare the underlying proof systems and show that expansion systems admit strictly shorter proofs than CDCL systems for formulas of bounded quantifier complexity, thus pointing towards potential advantages of expansion solving techniques over QCDCL solving.

Our first result shows that tree-like expansion systems allow short proofs of QBFs that are a source of hardness for QCDCL, i.e. tree-like Exp+Res is strictly stronger than tree-like Q-Resolution.

In our second result we efficiently transform dag-like Q-Resolution proofs of QBFs with bounded quantifier complexity into Exp+Res proofs. This is theoretical confirmation of experimental findings by Lonsing and Egly, who observed that expansion QBF solvers often outperform QCDCL solvers on instances with few quantifier alternations.