Feasible interpolation for QBF resolution calculi

DOI10.1007/978-3-662-47672-7_15MaRDI QIDQ3448783zbMATH OpenOpenAlexDBLPWikidataFDO

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)

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

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)

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.

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

Cites work

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

Cited in

(7)

• Lifting QBF resolution calculi to DQBF
• scientific article; zbMATH DE number 7228403 (Why is no real title available?)
• Long distance Q-resolution with dependency schemes
• Long-distance Q-resolution with dependency schemes
• A game characterisation of tree-like Q-resolution size
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)
• Feasible interpolation for QBF resolution calculi

Describes a project that uses

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)