Lower bounds for QCDCL via formula gauge
From MaRDI portal
Publication:6053848
DOI10.1007/s10817-023-09683-1MaRDI QIDQ6053848
Olaf Beyersdorff, Benjamin Böhm
Publication date: 24 October 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
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
- Relating size and width in variants of Q-resolution
- Resolution for quantified Boolean formulas
- Lower bounds for QCDCL via formula gauge
- 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 Q-Resolution and CDCL QBF Solving
- Q-Resolution with Generalized Axioms
- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
- QBF Resolution Systems and Their Proof Complexities
- Short proofs are narrow—resolution made simple
- Are Short Proofs Narrow? QBF Resolution Is Not So Simple
- 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
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
This page was built for publication: Lower bounds for QCDCL via formula gauge
