Alladi Ramakrishnan Hall

Are Short Proofs Narrow? QBF Resolution is not Simple.

Anil Shukla

IMSc

In this talk, we look at some proof systems (in particular, resolution and QBF resolution) in proof complexity.

First we review the complexity measures size, width, and space for resolution, revisit the literature on resolution for how these complexity measures are related, and present the importance of width in resolution. In particular, Ben-Sasson and Wigderson (J.ACM 2001) showed that linear width lower bounds imply exponential size lower bounds in tree-like resolution.

Next, we define QBF resolution proof systems (Q-Resolution) used to prove the falseness of QBF formulas. Then we define similar complexity measures size, width, and space for Q-Resolution and show that a linear lower bound on width of tree-like Q-Resolution proofs does not imply an exponential size lower bound. In particular, there is a QBF formula (in $O(n^2)$ variables) for which we show an $\Omega(n)$ width lower bound and also give a proof of polynomial size in tree-like Q-Resolution.

This is a joint work with Olaf Beyersdorff, Leroy Chew, and Meena Mahajan.
To appear in STACS 2016.