Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness

DOI10.4230/LIPICS.ICALP.2016.94MaRDI QIDQ4598235zbMATH OpenOpenAlexFDO

Authors Hubie Chen

Publication date 19 December 2017

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

zbMATH Keywords

polynomial hierarchyproof complexityquantified propositional logic

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Abstract: We present and study a framework in which one can present alternation-based lower bounds on proof length in proof systems for quantified Boolean formulas. A key notion in this framework is that of proof system ensemble, which is (essentially) a sequence of proof systems where, for each, proof checking can be performed in the polynomial hierarchy. We introduce a proof system ensemble called relaxing QU-res which is based on the established proof system QU-resolution. Our main results include an exponential separation of the tree-like and general versions of relaxing QU-res, and an exponential lower bound for relaxing QU-res; these are analogs of classical results in propositional proof complexity.

Recommendations

• Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness
• scientific article; zbMATH DE number 1222560
• Polynomial algorithms that prove an NP-hard hypothesis implies an NP-hard conclusion
• Hardness and optimality in QBF proof systems modulo NP
• scientific article; zbMATH DE number 2086404
• Proof complexity lower bounds from algebraic circuit complexity
• scientific article; zbMATH DE number 7471587
• scientific article; zbMATH DE number 1348481
• scientific article; zbMATH DE number 1916823
• scientific article; zbMATH DE number 7388145

Cited in

(9)

• Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness
• scientific article; zbMATH DE number 7561747 (Why is no real title available?)
• Hardness and optimality in QBF proof systems modulo NP
• Towards Uniform Certification in QBF
• A game characterisation of tree-like Q-resolution size
• Understanding cutting planes for QBFs
• On Q-resolution and CDCL QBF solving
• scientific article; zbMATH DE number 7228403 (Why is no real title available?)
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)

This page was built for publication: Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness

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