Lower bounds for QCDCL via formula gauge

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

zbMATH Keywords

lower boundsresolutionproof complexityQBFQCDCL

Mathematics Subject Classification ID

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)

Lower bounds for QCDCL via formula gauge

Uses Software

• Quaffle
• DepQBF

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