Research map / Learning theory and algorithms / Combinatorial and search optimization
Submodel Enumeration for CTL Is Hard
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Shows that enumerating satisfying submodels of a Kripke model for a CTL formula is DelNP-complete for every nonempty set of CTL operators, and gives DelP fragments when Boolean connectives are restricted.
Problem
Enumerating submodels of a Kripke structure that satisfy a CTL specification, with the goal of uniform-delay output for debugging/repair; the complexity of this enumeration problem was open.
Approach
Applies the hard-enumeration framework (DelP/DelNP, D-reductions) to CTL submodel enumeration: gives hardness reductions from SAT and Hamiltonian path for each operator fragment, and identifies tractable fragments by restricting Boolean connectives (e.g., existential operators without negation, and AF/AG with a shrinking lemma and a cycle-detection check).
Key results
- Submodel enumeration for CTL is DelNP-complete for every nonempty set of CTL operators in the presence of Boolean connectives.
- CTL submodel enumeration restricted to EX, ER, EU with conjunction and disjunction (no negation) is in DelP.
- CTL submodel enumeration restricted to AF and AG is in DelP.
Surprising findings
- Even a single CTL operator such as AX, AU or AR combined with Boolean connectives already yields DelNP-hardness, so no operator restriction alone gives efficient enumeration.
Limitations
- Results are purely theoretical; no implementation or empirical feasibility study.
- Only some Boolean fragments are classified; the full classification of 7 Boolean fragments times 2^10 operator sets is left open.
Experimental setup
Builds on: Creignou et al. hard enumeration framework Krebs et al. CTL fragment results
Closest papers by meaning
- Formula Synthesis in Propositional Dynamic Logic with Shuffle (AAAI 2022 · similarity 0.87)
- Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · similarity 0.85)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.84)
- Disjoint Partial Enumeration without Blocking Clauses (AAAI 2024 · similarity 0.83)
- An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes (AAAI 2024 · similarity 0.83)
- An Approximate Skolem Function Counter (AAAI 2024 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.