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同时调整了决策策略和单元传播策略。