On Q-Resolution and CDCL QBF Solving
From MaRDI portal
Publication:2818030
DOI10.1007/978-3-319-40970-2_25zbMath1475.68440OpenAlexW2493091936MaRDI QIDQ2818030
Publication date: 5 September 2016
Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-40970-2_25
Related Items (8)
Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Relating size and width in variants of Q-resolution ⋮ A simple proof of QBF hardness ⋮ A game characterisation of tree-like Q-resolution size ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Lower bounds for QCDCL via formula gauge ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Lower bounds for QCDCL via formula gauge
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 expressive power of stratified logic programs
- Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable
- The intractability of resolution
- Davis-Putnam resolution versus unrestricted resolution
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Resolution for quantified Boolean formulas
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- An application of games to the completeness problem for formalized theories
- Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- A Non-prenex, Non-clausal QBF Solver with Game-State Learning
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
This page was built for publication: On Q-Resolution and CDCL QBF Solving
