Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
From MaRDI portal
Publication:6135750
DOI10.46298/lmcs-19(2:2)2023arXiv2109.04862MaRDI QIDQ6135750
Olaf Beyersdorff, Benjamin Böhm
Publication date: 26 August 2023
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2109.04862
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Towards NP-P via proof complexity and search
- On the power of clause-learning SAT solvers as resolution engines
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- The intractability of resolution
- Resolution for quantified Boolean formulas
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Expansion-based QBF solving versus Q-resolution
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- A game characterisation of tree-like Q-resolution size
- Unified QBF certification and its applications
- On CDCL-based proof systems with the ordered decision strategy
- On Q-Resolution and CDCL QBF Solving
- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
- Narrow proofs may be spacious
- QBF Resolution Systems and Their Proof Complexities
- Encodings of Bounded Synthesis
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
- The relative efficiency of propositional proof systems
- Proof Complexity
- Dependency Learning for QBF
- Reasons for Hardness in QBF Proof Systems
- 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
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Improved Separations of Regular Resolution from Clause Learning Proof Systems
- The Complexity of Propositional Proofs
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
This page was built for publication: Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
