Olaf Beyersdorff ; Joshua Blinkhorn ; Luke Hinde - Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs

lmcs:4141 - Logical Methods in Computer Science, February 13, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:13)2019
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFsArticle

Authors: Olaf Beyersdorff ; Joshua Blinkhorn ; Luke Hinde

    As a natural extension of the SAT problem, an array of proof systems for quantified Boolean formulas (QBF) have been proposed, many of which extend a propositional proof system to handle universal quantification. By formalising the construction of the QBF proof system obtained from a propositional proof system by adding universal reduction (Beyersdorff, Bonacina & Chew, ITCS `16), we present a new technique for proving proof-size lower bounds in these systems. 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 QBF systems, we are able to use the technique to obtain lower bounds based on cost alone. As applications of the technique, we first prove exponential lower bounds for a new family of simple QBFs representing equality. 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, which apply to the QBF analogues of resolution, Cutting Planes, and Polynomial Calculus. Finally, we employ the technique to give a simple proof of hardness for the prominent formulas of Kleine Büning, Karpinski and Flögel.


    Volume: Volume 15, Issue 1
    Published on: February 13, 2019
    Accepted on: December 11, 2018
    Submitted on: December 12, 2017
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1623 times.
    This article's PDF has been downloaded 435 times.