ECCC-Report TR23-053https://eccc.weizmann.ac.il/report/2023/053Comments and Revisions published for TR23-053en-usThu, 20 Apr 2023 08:02:11 +0300
Paper TR23-053
| Proof Simulation via Round-based Strategy Extraction for QBF |
Leroy Chew
https://eccc.weizmann.ac.il/report/2023/053The 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.Thu, 20 Apr 2023 08:02:11 +0300https://eccc.weizmann.ac.il/report/2023/053