Feasible interpolation for QBF resolution calculi

DOI10.1007/978-3-662-47672-7_15zbMATH Open1440.68320DBLPconf/icalp/BeyersdorffCMS15arXiv1611.01328OpenAlexW756639098WikidataQ61835453 ScholiaQ61835453MaRDI QIDQ3448783FDOQ3448783

Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil K. Shukla 

Publication date: 27 October 2015

Published in: Automata, Languages, and Programming (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1611.01328

Recommendations

• Feasible interpolation for QBF resolution calculi
• Proof complexity of resolution-based QBF calculi
• New resolution-based QBF calculi and their proof complexity
• Lower bound techniques for QBF proof systems
• Lower bounds: from circuits to QBF proof systems

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• Unified QBF certification and its applications
• On Unification of QBF Resolution-Based Calculi
• Proof complexity of resolution-based QBF calculi
• Title not available (Why is that?)
• Contributions to the theory of practical quantified Boolean formula solving
• QBF Resolution Systems and Their Proof Complexities
• Some consequences of cryptographical conjectures for \(S_2^1\) and EF
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• The monotone circuit complexity of Boolean functions
• On lengths of proofs in non-classical logics
• Short proofs are narrow—resolution made simple
• Proofs as Games
• Non-automatizability of bounded-depth Frege proofs
• Title not available (Why is that?)
• On Interpolation and Automatization for Frege Systems
• Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity
• Conformant planning as a case study of incremental QBF solving
• A game characterisation of tree-like Q-resolution size
• Unified Characterisations of Resolution Hardness Measures

Cited In (7)

• Feasible interpolation for QBF resolution calculi
• Lifting QBF resolution calculi to DQBF
• A game characterisation of tree-like Q-resolution size
• Title not available (Why is that?)
• Long-distance Q-resolution with dependency schemes
• Title not available (Why is that?)
• Long distance Q-resolution with dependency schemes

Uses Software

• Quaffle

This page was built for publication: Feasible interpolation for QBF resolution calculi

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3448783)