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