2026-07-20T05:02:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23744 2025-11-12T13:00:02Z ddc:004 open_access

Fine-Grained Complexity Analysis of Dependency Quantified Boolean Formulas Cheng, Che Fung, Long-Hin Jiang, Jie-Hong Roland Slivovsky, Friedrich Tan, Tony Dependency quantified Boolean formulas complexity completeness conjunctive normal form disjunctive normal form Dependency Quantified Boolean Formulas (DQBF) extend Quantified Boolean Formulas by allowing each existential variable to depend on an explicitly specified subset of the universal variables. The satisfiability problem for DQBF is NEXP-complete in general, with only a few tractable fragments known to date. We investigate the complexity of DQBF with k existential variables (k-DQBF) under structural restrictions on the matrix - specifically, when it is in Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF) - as well as under constraints on the dependency sets. For DNF matrices, we obtain a clear classification: 2-DQBF is PSPACE-complete, while 3-DQBF is NEXP-hard, even with disjoint dependencies. For CNF matrices, the picture is more nuanced: we show that the complexity of k-DQBF ranges from NL-complete for 2-DQBF with disjoint dependencies to NEXP-complete for 6-DQBF with arbitrary dependencies. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Che Cheng and Long-Hin Fung and Jie-Hong Roland Jiang and Friedrich Slivovsky and Tony Tan 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.10 urn:nbn:de:0030-drops-237441 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.10 eng https://creativecommons.org/licenses/by/4.0/legalcode