Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
From MaRDI portal
Publication:6135750
DOI10.46298/LMCS-19(2:2)2023MaRDI QIDQ6135750FDOQ6135750
Authors: Olaf Beyersdorff, Benjamin Böhm 
Publication date: 26 August 2023
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/2109.04862
Recommendations
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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)
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- Lower bounds for QCDCL via formula gauge
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Should Decisions in QCDCL Follow Prefix Order?
- Strong (D)QBF dependency schemes via tautology-free resolution paths
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)
