Computationally Hard Problems Are Hard for QBF Proof Systems Too
Authors: Agnes Schleitzer, Olaf Beyersdorff
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | Our main technical work goes into showing that these formulas are hard for the QBF resolution systems QU-Res and Q-Res. For this we use the semantic size-cost lowerbound technique for QBF calculi, developed by Beyersdorff, Blinkhorn, and Hinde (2019). |
| Researcher Affiliation | Academia | Agnes Schleitzer, Olaf Beyersdorff Institut f ur Informatik, Friedrich-Schiller-Universit at Jena, Germany EMAIL, EMAIL |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. It describes methodologies in narrative text and uses diagrams like Figure 1 to illustrate workflows, but no formal pseudocode is present. |
| Open Source Code | No | The paper does not provide a specific repository link or an explicit statement about making the source code for the described methodology publicly available. It mentions a tool 'QBFFam' in the references but not as their own code release for this paper. |
| Open Datasets | No | The paper focuses on constructing families of hard QBFs from mathematical problems (e.g., graph theory, logic) and then proving their hardness. It does not use or provide access to publicly available datasets in the empirical sense. The graph families described (Gk n, Gn) and logical formulas (φn(Xn, Yn)) are theoretical constructions for analysis, not empirical datasets. |
| Dataset Splits | No | The paper does not describe experiments that would require dataset splits. It focuses on theoretical proofs and constructions of hard QBF formulas, not empirical evaluation on specific datasets with train/test/validation partitions. |
| Hardware Specification | No | The paper is theoretical, presenting methods and proofs for QBF hardness. It does not describe any experimental evaluations or computational runs that would require specific hardware, hence no hardware specifications are provided. |
| Software Dependencies | No | The paper is theoretical and focuses on proof complexity for QBF resolution systems (Q-Res, QU-Res). It does not describe any experimental implementation or analysis that would require specific software dependencies with version numbers. |
| Experiment Setup | No | The paper is theoretical and does not describe any empirical experiments. Therefore, there are no experimental setup details, hyperparameters, or training configurations mentioned in the main text. |