A simple proof of QBF hardness

DOI10.1016/j.ipl.2021.106093OpenAlexW3119804017MaRDI QIDQ2656352

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 complexityQBFQ-resolution

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Related Items (1)

QBFFam: a tool for generating QBF families from proof complexity

Uses Software

• Quaffle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the power of clause-learning SAT solvers as resolution engines
• The intractability of resolution
• Short proofs for some symmetric quantified Boolean formulas
• Resolution for quantified Boolean formulas
• Lower bound techniques for QBF expansion
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• Expansion-based QBF solving versus Q-resolution
• A game characterisation of tree-like Q-resolution size
• On Q-Resolution and CDCL QBF Solving
• Q-Resolution with Generalized Axioms
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• On Unification of QBF Resolution-Based Calculi
• QBF Resolution Systems and Their Proof Complexities
• Proof Complexity
• Frege Systems for Quantified Boolean Logic
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• New Resolution-Based QBF Calculi and Their Proof Complexity
• The Complexity of Propositional Proofs
• A Machine-Oriented Logic Based on the Resolution Principle

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