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.

翻译：实现QCDCL范式的QBF求解器是成功处理众多计算复杂应用的有效算法。然而，我们对这些QCDCL求解器能力与局限性的理论理解仍十分有限。本文提出将QCDCL求解器形式化建模为证明系统。我们定义了可用于决策启发式与单元传播的不同策略，由此产生了若干可靠且完备的QBF证明系统（即新的QCDCL算法）。针对实际QCDCL求解中采用的标准策略，我们证明相应的QCDCL证明系统与文献中经典QBF消解系统Q-resolution（通过指数级分离）不可比较。这与命题逻辑背景下CDCL与消解法已知为p等价的情况形成鲜明对比。这引发了一个问题：哪些公式对标准QCDCL而言是困难的？因为如我们所示，Q-resolution的下界未必适用于QCDCL。为解答此问题，我们证明了QCDCL的若干下界，包括一类大规模随机QBF的指数级下界。我们还引入了对经典QCDCL中决策启发式的强化，该强化不要求严格按前缀顺序选择变量，但仍能学习断言子句。我们表明采用此决策策略后，QCDCL在特定公式上可实现指数级加速。此外，我们构造了一个与Q-resolution p等价的QCDCL证明系统。与经典QCDCL相比，这一新型QCDCL版本同时调整了决策策略与单元传播策略。