ABSTRACT. Recent decades have seen significant advances in the solution of computationally hard problems, in particular the decision problem for the NP-complete language SAT [Cook71]. Quantified Boolean formulas (QBF) extend propositional logic with existential and universal quantification, forming the prototypical PSPACE-complete language [StockmeyerM73]. Despite the higher complexity, QBF solvers are beginning to rival SAT solvers in certain application areas [FaymonvilleFRT17], and appear to be reaching the point of industrial applicability.

Alongside the development of solvers, there has been much interest in associated proof systems and their relative proof complexities [Buss12]. A host of QBF proof systems have been proposed, many of which extend some propositional system P to handle universal quantification [BeyersdorffCJ15]. A natural way to do this is to add a universal reduction rule, yielding the system P+$\forall$red [BeyersdorffBC16].

We present a new technique for proving proof-size lower bounds in P+$\forall$red. The technique relies only on two semantic measures: the cost of a QBF, and the capacity of a proof. Our central result, the Size-Cost-Capacity Theorem, states that proof-size in P+$\forall$red is at least the ratio of cost to capacity. By examining the capacity of proofs in several concrete systems (the universal reduction extensions of Resoution, Cutting Planes and Polynomial Calculus) we obtain lower bounds based solely on cost. Our technique provides genuine lower bounds in the sense that they continue to hold if P+$\forall$red is given access to an NP oracle [BeyersdorffHP17].

As applications of the technique, we first prove exponential lower bounds for the equality formulas, a new QBF family based on a simple two-player game. The main application is in proving exponential lower bounds with high probability for a class of randomly generated QBFs, the first genuine lower bounds of this kind. Finally, we employ the technique to give a simple proof of hardness for the prominent formulas of Kleine B\"{u}ning, Karpinski and Fl\"{o}gel [BuningKF95].