期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2020
卷号：2020
页码：1-26
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) by circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems [14], but leaving open the most important case of QBF resolution. Different from the Frege case, our characterisation uses a new version of decision lists as its circuit model, which is stronger than the CNFs the system works with. Our decision list model is well suited to compute countermodels for QBFs. Our characterisation works for both Q-Resolution and QU-Resolution, which we show to be polynomially equivalent for QBFs of bounded quantifier alternation. Using our characterisation we obtain a size-width relation for QBF resolution in the spirit of the celebrated result for propositional resolution [3]. However, our result is not just a replication of the propositional relation – intriguingly ruled out for QBF in previous research [10] – but shows a different dependence between size, width, and quantifier complexity. We demonstrate that our new technique elegantly reproves known QBF hardness results and unifies previous lower-bound techniques in the QBF domain.
