Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
From MaRDI portal
Publication:6135750
Abstract: QBF solvers implementing the QCDCL paradigm are powerful algorithms that successfully tackle many computationally complex applications. However, our theoretical understanding of the strength and limitations of these QCDCL solvers is very limited. In this paper we suggest to formally model QCDCL solvers as proof systems. We define different policies that can be used for decision heuristics and unit propagation and give rise to a number of sound and complete QBF proof systems (and hence new QCDCL algorithms). With respect to the standard policies used in practical QCDCL solving, we show that the corresponding QCDCL proof system is incomparable (via exponential separations) to Q-resolution, the classical QBF resolution system used in the literature. This is in stark contrast to the propositional setting where CDCL and resolution are known to be p-equivalent. This raises the question what formulas are hard for standard QCDCL, since Q-resolution lower bounds do not necessarily apply to QCDCL as we show here. In answer to this question we prove several lower bounds for QCDCL, including exponential lower bounds for a large class of random QBFs. We also introduce a strengthening of the decision heuristic used in classical QCDCL, which does not necessarily decide variables in order of the prefix, but still allows to learn asserting clauses. We show that with this decision policy, QCDCL can be exponentially faster on some formulas. We further exhibit a QCDCL proof system that is p-equivalent to Q-resolution. In comparison to classical QCDCL, this new QCDCL version adapts both decision and unit propagation policies.
Recommendations
Cites work
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- scientific article; zbMATH DE number 1860652 (Why is no real title available?)
- scientific article; zbMATH DE number 7559123 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 2243370 (Why is no real title available?)
- A Computing Procedure for Quantification Theory
- A game characterisation of tree-like Q-resolution size
- A machine program for theorem-proving
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- Dependency Learning for QBF
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Encodings of bounded synthesis
- Expansion-based QBF solving versus Q-resolution
- Feasible interpolation for QBF resolution calculi
- Frege systems for quantified Boolean logic
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- Improved separations of regular resolution from clause learning proof systems
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- Narrow proofs may be spacious, separating space and width in resolution
- New resolution-based QBF calculi and their proof complexity
- On CDCL-based proof systems with the ordered decision strategy
- On Q-resolution and CDCL QBF solving
- On the power of clause-learning SAT solvers as resolution engines
- Proof Complexity
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- QBF Resolution Systems and Their Proof Complexities
- Reasons for hardness in QBF proof systems
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
- Resolution for quantified Boolean formulas
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- The Complexity of Propositional Proofs
- The intractability of resolution
- The relative efficiency of propositional proof systems
- Towards NP-P via proof complexity and search
- Unified QBF certification and its applications
Cited in
(7)- CAQE and QuAbS: Abstraction Based QBF Solvers
- Lower bounds for QCDCL via formula gauge
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- Strong (D)QBF dependency schemes via tautology-free resolution paths
- Should Decisions in QCDCL Follow Prefix Order?
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
This page was built for publication: Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135750)
