Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
From MaRDI portal
(Redirected from 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
- A Computing Procedure for Quantification Theory
- A game characterisation of tree-like Q-resolution size
- A machine program for theorem-proving
- Building strategies into QBF proofs
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- Dependency Learning for QBF
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- 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
- 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 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 2243370 (Why is no real title available?)
- 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 for quantified Boolean formulas
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
- 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
(13)- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- Strong (D)QBF dependency schemes via tautology-free resolution paths
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Lower bounds for QCDCL via formula gauge
- Should Decisions in QCDCL Follow Prefix Order?
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- The relative strength of \#SAT proof systems
- Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- Hard QBFs for merge resolution
- QCDCL with cube learning or pure literal elimination -- what is best?
- Polynomial calculus for quantified Boolean logic: lower bounds through circuits and degree
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)
