Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
From MaRDI portal
Publication:6135750
DOI10.46298/LMCS-19(2:2)2023arXiv2109.04862MaRDI 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
Cites Work
- Resolution for quantified Boolean formulas
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- Title not available (Why is that?)
- Dependency Learning for QBF
- Title not available (Why is that?)
- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
- QBF Resolution Systems and Their Proof Complexities
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- The relative efficiency of propositional proof systems
- The intractability of resolution
- On the power of clause-learning SAT solvers as resolution engines
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
- Towards NP-P via proof complexity and search
- Title not available (Why is that?)
- The Complexity of Propositional Proofs
- Encodings of Bounded Synthesis
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- Narrow proofs may be spacious
- Frege Systems for Quantified Boolean Logic
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- A game characterisation of tree-like Q-resolution size
- Title not available (Why is that?)
- Proof Complexity
- Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
- New Resolution-Based QBF Calculi and Their Proof Complexity
- Title not available (Why is that?)
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Improved Separations of Regular Resolution from Clause Learning Proof Systems
- On Q-Resolution and CDCL QBF Solving
- Title not available (Why is that?)
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- On CDCL-based proof systems with the ordered decision strategy
- Reasons for Hardness in QBF Proof Systems
Cited In (6)
- 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
- 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)
