Proof Simulation via Round-based Strategy Extraction for QBF
Authors: Leroy Chew
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | By formalising the strategy extraction into circuits we can show new p-simulations. P-simulations are processes that allow you to transform proofs from a weaker proof system to a stronger proof system. Thus we solve an open problem in QBF proof complexity that Extended QBF Frege p-simulates LD-Q(Drrs)-Resolution. |
| Researcher Affiliation | Academia | TU Wien. Vienna, Austria EMAIL |
| Pseudocode | No | The paper describes methods using definitions, theorems, lemmas, and figures (e.g., Figure 1, 2, 3), but does not include explicit pseudocode or algorithm blocks. |
| Open Source Code | No | The ethical statement includes a question 'All source code required for conducting and analyzing the experiments will be made publicly available upon publication of the paper with a license that allows free usage for research purposes. (yes/partial/no)' which implies future availability, not current. |
| Open Datasets | No | The paper is theoretical, focusing on formalizing strategy extraction and p-simulations for QBF proof systems, and does not involve empirical datasets or experiments. |
| Dataset Splits | No | The paper is theoretical and does not use datasets, therefore no dataset splits are discussed. |
| Hardware Specification | No | The paper is theoretical and does not describe any computational experiments, so no hardware specifications are provided. |
| Software Dependencies | No | The paper refers to QBF solvers like Qute (Peitl, Slivovsky, and Szeider 2019a) and proof systems like DRAT and QRAT in the context of the research domain, but does not list specific software dependencies with version numbers used for conducting the work presented. |
| Experiment Setup | No | The paper is theoretical and does not describe any computational experiments, so no experimental setup details or hyperparameters are provided. |