Lower bounds for QCDCL via formula gauge
From MaRDI portal
Publication:2118284
DOI10.1007/978-3-030-80223-3_5OpenAlexW3186139236MaRDI QIDQ2118284
Benjamin Böhm, Olaf Beyersdorff
Publication date: 22 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-80223-3_5
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
- 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
- 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
- Proof Complexity
- Dependency Learning for QBF
- 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
This page was built for publication: Lower bounds for QCDCL via formula gauge
