Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR23-053 | 19th April 2023 12:28

Proof Simulation via Round-based Strategy Extraction for QBF


Authors: Leroy Chew
Publication: 20th April 2023 08:02
Downloads: 52


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.

ISSN 1433-8092 | Imprint