The proof complexity of Quantified Boolean Formulas (QBF) relates to both QBF solving and OBF certification. One method to p-simulate a QBF proof system is by formalising the soundness of its strategy extraction in propositional logic. In this work we illustrate how to use extended QBF Frege to simulate LD-Q(Drrs)-Res, ... more >>>

In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, ... more >>>

We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants - parameterised by different policies for decisions, unit propagations and reductions -- lead to ... more >>>