How QBF expansion makes strategy extraction hard
From MaRDI portal
Publication:2096438
DOI10.1007/978-3-030-51074-9_5OpenAlexW2997716221MaRDI QIDQ2096438
Publication date: 9 November 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_5
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the complexity of cutting-plane proofs
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- A little blocked literal goes a long way
- Understanding cutting planes for QBFs
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- Resolution for quantified Boolean formulas
- Short proofs in QBF expansion
- The equivalences of refutational QRAT
- QRAT polynomially simulates \(\forall\)-Exp+Res
- Expansion-based QBF solving versus Q-resolution
- Lower Bounds
- Solving QBF with Counterexample Guided Refinement
- A Unified Proof System for QBF Preprocessing
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
- The relative efficiency of propositional proof systems
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
This page was built for publication: How QBF expansion makes strategy extraction hard
