Towards Uniform Certification in QBF
From MaRDI portal
Publication:6151563
DOI10.46298/lmcs-20(1:14)2024arXiv2210.07085v4OpenAlexW3215442047MaRDI QIDQ6151563
Friedrich Slivovsky, Leroy Chew
Publication date: 11 March 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2210.07085v4
Cites Work
- Unnamed Item
- Solving QBF with counterexample guided refinement
- Local soundness for QBF calculi
- A little blocked literal goes a long way
- Understanding cutting planes for QBFs
- Resolution for quantified Boolean formulas
- Building strategies into QBF proofs
- Hardness and optimality in QBF proof systems modulo NP
- Expansion-based QBF solving versus Q-resolution
- Solution validation and extraction for QBF preprocessing
- Efficient certified RAT verification
- Long-distance Q-resolution with dependency schemes
- Unified QBF certification and its applications
- Multi-linear strategy extraction for QBF expansion proofs via local soundness
- 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
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Quantified propositional calculi and fragments of bounded arithmetic
- A First Step Towards a Unified Proof Checker for QBF
- On the correspondence between arithmetic theories and propositional proof systems – a survey
- The relative efficiency of propositional proof systems
- Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
- Proof Complexity
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- Automated Testing and Debugging of SAT and QBF Solvers
- Integrating Dependency Schemes in Search-Based QBF Solvers
- Dependency Learning for QBF
- Frege Systems for Quantified Boolean Logic
- New Resolution-Based QBF Calculi and Their Proof Complexity
- Computational Complexity
This page was built for publication: Towards Uniform Certification in QBF
