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, a proof system that combines conflict driven clause learning with dependency schemes, using such a method.
The round-based technique is the most common way to show a QBF proof system has strategy extraction, originally shown for Q-resolution and later used for LD-Q-Resolution, LQU-Resolution, expansion based systems and dependency-scheme based systems. Many of these proof systems were already shown to be simulated by extended QBF Frege, but simulation had to use a specialised local strategy extraction technique. Here we simulate the remaining systems, by formalising the soundness of LD-Q(Drrs)-Res's round-based strategy extraction in propositional logic. This is a positive result for certification, and further suggests the feasibility of using Extended QU-Resolution or QRAT to certify QCDCL solvers.