A simple proof of QBF hardness

DOI10.1016/J.IPL.2021.106093MaRDI QIDQ2656352zbMATH OpenOpenAlexFDO

Authors Olaf Beyersdorff, Joshua Blinkhorn

Publication date 11 March 2021

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2021.106093

zbMATH Keywords

computational complexitylower boundsproof complexityQ-resolutionQBF

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A game characterisation of tree-like Q-resolution size
• A Machine-Oriented Logic Based on the Resolution Principle
• Expansion-based QBF solving versus Q-resolution
• Frege systems for quantified Boolean logic
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
• Lower bound techniques for QBF expansion
• New resolution-based QBF calculi and their proof complexity
• On Q-resolution and CDCL QBF solving
• On the power of clause-learning SAT solvers as resolution engines
• On Unification of QBF Resolution-Based Calculi
• Proof Complexity
• Proof complexity of resolution-based QBF calculi
• Q-resolution with generalized axioms
• QBF Resolution Systems and Their Proof Complexities
• Resolution for quantified Boolean formulas
• Short proofs for some symmetric quantified Boolean formulas
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• The Complexity of Propositional Proofs
• The intractability of resolution

Cited in

(7)

• QBF as an alternative to Courcelle's theorem
• QBFFam: a tool for generating QBF families from proof complexity
• Short proofs in QBF expansion
• Are Short Proofs Narrow? QBF Resolution is not Simple.
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple
• scientific article; zbMATH DE number 7278086 (Why is no real title available?)
• Classes of hard formulas for QBF resolution

Describes a project that uses

Uses Software

• Quaffle

This page was built for publication: A simple proof of QBF hardness

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