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.