Submodel Enumeration for CTL Is Hard

Authors: Nicolas Fröhlich, Arne Meier

AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical In this paper, we fill this gap and present a thorough study of the complexity of the submodel enumeration problem in the context of CTL. We will see that in general the problem is complete for the class Del NP; so it is reasonable to consider restrictions that aim for tractable enumeration cases. However, our answer in this direction is on the negative side, showing that any restriction on the CTL operator side does not allow faster enumeration algorithms (assuming P = NP). Finally, we identify some further Boolean restrictions that still allow for Del P algorithms.
Researcher Affiliation Academia Leibniz Universit at Hannover, Institut f ur Theoretische Informatik, Appelstrasse 9a, 30167 Hannover, Germany nicolas.froehlich@thi.uni-hannover.de, meier@thi.uni-hannover.de
Pseudocode No The paper describes algorithms in prose (e.g., "The algorithm deciding EXTSUBMODEL works as follows.") but does not provide structured pseudocode or algorithm blocks.
Open Source Code No The paper does not mention providing open-source code for the described methodology.
Open Datasets No The paper is theoretical and does not involve empirical experiments with datasets; thus, no information on training datasets or their availability is provided.
Dataset Splits No The paper is theoretical and does not involve empirical experiments with datasets; thus, no information on dataset splits for validation is provided.
Hardware Specification No The paper is theoretical and does not describe any specific hardware used for experiments.
Software Dependencies No The paper references general tools like "SAT solvers" but does not specify any software dependencies with version numbers for reproducibility.
Experiment Setup No The paper is theoretical and does not describe any experimental setup details such as hyperparameters or training configurations.