Olaf Beyersdorff ; Leroy Chew ; Meena Mahajan ; Anil Shukla - Feasible Interpolation for QBF Resolution Calculi

lmcs:2198 - Logical Methods in Computer Science, June 8, 2017, Volume 13, Issue 2 - https://doi.org/10.23638/LMCS-13(2:7)2017
Feasible Interpolation for QBF Resolution CalculiArticle

Authors: Olaf Beyersdorff ORCID; Leroy Chew ; Meena Mahajan ORCID; Anil Shukla

    In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper 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 proof systems 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.


    Volume: Volume 13, Issue 2
    Published on: June 8, 2017
    Accepted on: March 27, 2017
    Submitted on: June 8, 2017
    Keywords: Computer Science - Computational Complexity,Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Parameterized Proof Complexity; Funder: UK Research and Innovation; Code: EP/L024233/1

    9 Documents citing this article

    Consultation statistics

    This page has been seen 1533 times.
    This article's PDF has been downloaded 392 times.