Solving Quantified Boolean Formulas with Few Existential Variables
Authors: Leif Eriksson, Victor Lagerkvist, Sebastian Ordyniak, George Osipov, Fahad Panolan, Mateusz Rychlicki
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | A theoretical explanation is that QBF (as well as many other PSPACE-complete problems) lacks natural parameters guaranteeing fixedparameter tractability (FPT). In this paper we tackle this problem and consider a simple but overlooked parameter: the number of existentially quantified variables. Via this parameterization we then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length. We complement this by a W[1]-hardness result for QBF in CNF of unbounded clause length as well as sharper lower bounds for the bounded arity case under the (strong) exponential-time hypothesis. |
| Researcher Affiliation | Academia | 1Department of Computer and Information Science, Link oping University, Link oping, Sweden 2School of Computing, University of Leeds, Leeds, UK |
| Pseudocode | No | The paper describes algorithms and reductions in detail (e.g., the FPT algorithm for QBFSAT, the reduction to CLAUSE-GRAPH INDEPENDENT SET), but it does not present any of these algorithms or procedures in a formal pseudocode block or a clearly labeled algorithm figure. |
| Open Source Code | No | The paper does not provide any specific links to source code repositories (e.g., GitHub, GitLab) or state that the code for the methodology described is being released or is available in supplementary materials. |
| Open Datasets | No | The paper is theoretical, focusing on complexity theory, algorithm design, and lower bounds for QBF problems. It does not involve empirical experiments with datasets, and thus, there is no mention of training data, public availability of datasets, or their sources. |
| Dataset Splits | No | The paper is theoretical, focusing on parameterized complexity and algorithm design, not empirical experimentation. Therefore, it does not involve dataset splits for training, validation, or testing, nor does it specify any methods for data partitioning. |
| Hardware Specification | No | This is a theoretical paper focused on algorithm design and complexity analysis. It does not describe any computational experiments that would require specific hardware, and consequently, no hardware specifications (like CPU, GPU models, or memory details) are mentioned. |
| Software Dependencies | No | This paper is theoretical and does not describe any implemented systems or empirical experiments. Therefore, it does not list any software dependencies with specific version numbers. |
| Experiment Setup | No | The paper is theoretical and discusses algorithms and complexity, not empirical experiments. Thus, there is no description of an experimental setup, hyperparameters, or system-level training settings. |