[Proof Complexity] New preprint

Olaf Beyersdorff O.Beyersdorff at leeds.ac.uk
Thu Apr 16 21:32:14 CEST 2015

Dear Colleagues,

A new preprint 'Feasible Interpolation for QBF Resolution Calculi' by Leroy Chew, Meena Mahajan, Anil Shukla and myself is available at http://eccc.hpi-web.de/report/2015/059/.

Comments and suggestion are very welcome.

Best wishes


Feasible Interpolation for QBF Resolution Calculi


In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. We establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF calculi as well as largely extends the scope of classical feasible interpolation. We apply our technique to obtain new exponential lower bounds to all resolution-based QBF systems for a new class of QBF formulas based on the clique problem. Finally, we show how feasible interpolation relates to the recently established lower bound method based on strategy extraction.

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>

More information about the Proof-Complexity mailing list