Classes of Hard Formulas for QBF Resolution
Authors: Agnes Schleitzer, Olaf Beyersdorff
JAIR 2023 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | The main objective in proof complexity is to study the size of proofs in different formal proof systems. Proof complexity has its origins in computational complexity (Cook & Reckhow, 1979) with many important connections to other fields, in particular to logic (Kraj ıˇcek, 2019; Cook & Nguyen, 2010) and solving (Buss & Nordstr om, 2021). For the latter, proof complexity provides the main theoretical tool to assess the strength of modern solving methods. The main objective in proof complexity and often also the most challenging is to show lower bounds to the size of proofs and to obtain separations between different calculi. For this, specific formula families are needed on which the lower bounds are demonstrated. Our Contributions. Our contributions can be summarised as follows. (1) Hard QBFs for Q-Res and QU-Res. We introduce a generic construction to obtain large classes of QBFs that are hard for Q-Res and QU-Res. (2) Separations between Q-Res and LD-Q-Res. (3) Separations between Q-Res and QU-Res. |
| Researcher Affiliation | Academia | Agnes Schleitzer EMAIL Olaf Beyersdorff EMAIL Friedrich-Schiller-Universit at Jena, Fakult at f ur Mathematik und Informatik, Institut f ur Informatik, Ernst-Abbe-Platz 1, 07743 Jena, Deutschland |
| Pseudocode | No | The paper does not contain any sections explicitly labeled "Pseudocode" or "Algorithm", nor does it present structured, code-like steps for a method. Figures are diagrams explaining concepts or proof structures. |
| Open Source Code | No | The paper mentions: "A track of crafted formulas was introduced into QBFEval 2020 and a tool to generate the mentioned QBF families was presented by Beyersdorff, Pulina, Seidl, and Shukla (2021b)." This refers to a tool that generates *other* QBF families by different authors, not a direct statement or link for the source code of the methodology described in *this* paper. |
| Open Datasets | No | The paper is theoretical and focuses on constructing new classes of hard formulas and separations for QBF resolution systems. It does not describe experiments performed on specific datasets, nor does it provide access information for any open datasets. |
| Dataset Splits | No | The paper is theoretical and does not perform empirical evaluations using datasets, therefore, no dataset splits are provided. |
| Hardware Specification | No | The paper is theoretical and focuses on proof complexity and formula construction. It does not describe any experimental setup that would require specific hardware, thus no hardware specifications are mentioned. |
| Software Dependencies | No | The paper is theoretical and discusses QBF resolution systems and proof complexity. It does not describe an implementation or experiments that would require specific software dependencies with version numbers. |
| Experiment Setup | No | The paper is theoretical and describes constructions and proofs in proof complexity. It does not include any experimental results, and therefore no experimental setup details such as hyperparameters or system-level training settings are provided. |