On the Interplay of Cube Learning and Dependency Schemes in QCDCL Proof Systems
Abhimanyu Choudhury, Meena Mahajan
TL;DR
The paper addresses how cube-learning and dependency schemes interact in QCDCL-based QBF proof systems. It formalises a broad family of systems ${\mathtt{QCDCL}}^{D\!\text{-}\!\mathrm{ORD}}({\mathtt{ClausePol}},{\mathtt{CubePol}})$, proving soundness and refutational completeness under normal schemes and showing that $D^{\mathrm{std}}$ and $D^{\mathrm{rrs}}$ in the decision policy can provably shorten refutations. It provides a taxonomy of strength relations, including strict advantages of dependency-ordered systems over level-ordered ones and a variety of incomparabilities between different dependency schemes and cube-learning variants, supported by new formula families (DoubleLongEq, PreRRSTrapdoor, StdDepTrap) and refined simulations. The results emphasize that, while dependency schemes can accelerate refutations in some contexts, in others they offer no advantage or even hinder progress, highlighting open questions about optimal combinations and long-distance resolution with dependencies. Overall, the work advances theoretical understanding of when and how dependency analysis and cube-learning improve QBF solving practice, guiding future solver design and formal analysis.
Abstract
Quantified Conflict Driven Clause Leaning (QCDCL) is one of the main approaches to solving Quantified Boolean Formulas (QBF). Cube-learning is employed in this approach to ensure that true formulas can be verified. Dependency Schemes help to detect spurious dependencies that are implied by the variable ordering in the quantifier prefix of QBFs but are not essential for constructing (counter)models. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The simplest underlying proof system [BeyersdorffBöhm-LMCS2023], formalises the reasoning in the QCDCL approach on false formulas, when neither cube learning nor dependency schemes is used. The work of [BöhmPeitlBeyersdorff-AI2024] further incorporates cube-learning. The work of [ChoudhuryMahajan-JAR2024] incorporates a limited use of dependency schemes, but without cube-learning. In this work, proof systems underlying the reasoning of QCDCL solvers which use cube learning, and which use dependency schemes at all stages, are formalised. Sufficient conditions for soundness and completeness are presented, and it is shown that using the standard and reflexive resolution path dependency schemes ($D^{std}$ and $D^{rrs}$) to relax the decision order provably shortens refutations. When the decisions are restricted to follow quantification order, but dependency schemes are used in propagation and learning, in conjunction with cube-learning, the resulting proof systems using the dependency schemes $D^{std}$ and $D^{rrs}$ are investigated in detail and their relative strengths are analysed.