Model Counting for Dependency Quantified Boolean Formulas
Long-Hin Fung, Che Cheng, Jie-Hong Roland Jiang, Friedrich Slivovsky, Tony Tan
Abstract
Dependency Quantified Boolean Formulas (DQBF) generalize QBF by explicitly specifying which universal variables each existential variable depends on, instead of relying on a linear quantifier order. The satisfiability problem of DQBF is NEXP-complete, and many hard problems can be succinctly encoded as DQBF. Recent work has revealed a strong analogy between DQBF and SAT: k-DQBF (with k existential variables) is a succinct form of k-SAT, and satisfiability is NEXP-complete for 3-DQBF but PSPACE-complete for 2-DQBF, mirroring the complexity gap between 3-SAT (NP-complete) and 2-SAT (NL-complete). Motivated by this analogy, we study the model counting problem for DQBF, denoted #DQBF. Our main theoretical result is that #2-DQBF is #EXP-complete, where #EXP is the exponential-time analogue of #P. This parallels Valiant
BibTeX
@inproceedings{aaai2026_modelcountingfor,
title = {Model Counting for Dependency Quantified Boolean Formulas},
author = {Long-Hin Fung and Che Cheng and Jie-Hong Roland Jiang and Friedrich Slivovsky and Tony Tan},
booktitle = {AAAI 2026},
year = {2026}
}