Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs

As a natural extension of the SAT problem, an array of proof systems forquantified Boolean formulas (QBF) have been proposed, many of which extend apropositional proof system to handle universal quantification. By formalisingthe construction of the QBF proof system obtained from a propositional proofsystem by adding universal reduction (Beyersdorff, Bonacina & Chew, ITCS `16),we present a new technique for proving proof-size lower bounds in thesesystems. The technique relies only on two semantic measures: the cost of a QBF,and the capacity of a proof. By examining the capacity of proofs in several QBFsystems, we are able to use the technique to obtain lower bounds based on costalone. As applications of the technique, we first prove exponential lower bounds fora new family of simple QBFs representing equality. The main application is inproving exponential lower bounds with high probability for a class of randomlygenerated QBFs, the first `genuine' lower bounds of this kind, which apply tothe QBF analogues of resolution, Cutting Planes, and Polynomial Calculus.Finally, we employ the technique to give a simple proof of hardness for theprominent formulas of Kleine B\"uning, Karpinski and Fl\"ogel