[Proof Complexity] new preprint on QBF proof complexity

[Olaf Beyersdorff]

Dear Colleagues,

A new preprint 'Proof Complexity of Resolution-based QBF Calculi' of Leroy Chew, Mikolas Janota and myself is available at http://eccc.hpi-web.de/report/2014/120/.
Comments and suggestions are welcome.

Best wishes
Olaf



Title: Proof Complexity of Resolution-based QBF Calculi

Abstract:

Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important
QBF solvers.  However, the proof complexity of these proof systems is currently not well understood and in particular
lower bound techniques are missing.  In this paper we exhibit a new and elegant proof technique for showing lower bounds
in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to
lengths of proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for
Q-resolution.  Variants of the formulas are hard for even stronger systems as long-distance and universal Q-resolution.
With a completely different lower bound argument we show the hardness of the prominent formulas of Kleine Büning et
al. for the strong expansion-based calculus IR-calc, thus also confirming the hardness of the formulas for Q-resolution.
Our lower bounds imply new exponential separations between two different types of resolution-based QBF calculi: proof
systems for DPLL-based solvers (Q-resolution, long-distance Q-resolution) and proof systems for expansion-based solvers
($\forall$Exp+Res and its generalizations IR-calc and IRM-calc). The relations between proof systems from the two
different classes were not known before.


--
Dr Olaf Beyersdorff
School of Computing
University of Leeds, Leeds, LS2 9JT, UK.
Phone: +44 113 343 8319
Email: O.Beyersdorff at leeds.ac.uk<mailto:O.Beyersdorff at leeds.ac.uk>
http://www.engineering.leeds.ac.uk/people/computing/staff/o.beyersdorff