Hardness and optimality in QBF proof systems modulo NP
From MaRDI portal
Publication:2118289
DOI10.1007/978-3-030-80223-3_8OpenAlexW3185666742MaRDI QIDQ2118289
Publication date: 22 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-80223-3_8
simulationresolutionproof complexityQBFoptimal proof systemsextended Fregestrategy extractionNP oracles
Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The intractability of resolution
- One-way permutations in NC 0
- A little blocked literal goes a long way
- Dual weak pigeonhole principle, Boolean complexity, and derandomization
- Resolution for quantified Boolean formulas
- How QBF expansion makes strategy extraction hard
- QRAT polynomially simulates \(\forall\)-Exp+Res
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- Solving QBF with Counterexample Guided Refinement
- A Unified Proof System for QBF Preprocessing
- Parity, circuits, and the polynomial-time hierarchy
- A First Step Towards a Unified Proof Checker for QBF
- Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
- Approximation and Small-Depth Frege Proofs
- The relative efficiency of propositional proof systems
- Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- Frege Systems for Quantified Boolean Logic
- New Resolution-Based QBF Calculi and Their Proof Complexity
- Computational Complexity
This page was built for publication: Hardness and optimality in QBF proof systems modulo NP
