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's classical theorem stating that #2-SAT is #P-complete. As a direct application, we show that first-order model counting (FOMC) remains #EXP-complete even when restricted to a PSPACE-decidable fragment of first-order logic and domain size two. Building on recent successes in reducing 2-DQBF satisfiability to symbolic model checking, we develop a dedicated 2-DQBF model counter. Using a diverse set of crafted instances, we experimentally evaluated it against a baseline that expands 2-DQBF formulas into propositional formulas and applies propositional model counting. While the baseline worked well when each existential variable depends on few variables, our implementation scaled significantly better to larger dependency sets.

翻译：依赖量化布尔公式（DQBF）通过显式指定每个存在变量依赖于哪些全称变量，而非依赖线性量词顺序，从而推广了QBF。DQBF的可满足性问题是NEXP完全的，许多困难问题可以简洁地编码为DQBF。近期研究揭示了DQBF与SAT之间的强类比：k-DQBF（具有k个存在变量）是k-SAT的简洁形式，且3-DQBF的可满足性是NEXP完全的，而2-DQBF是PSPACE完全的，这反映了3-SAT（NP完全）与2-SAT（NL完全）之间的复杂性差距。受此类比启发，我们研究了DQBF的模型计数问题，记为#DQBF。我们的主要理论结果是#2-DQBF是#EXP完全的，其中#EXP是#P的指数时间类比。这与Valiant的经典定理（即#2-SAT是#P完全的）相平行。作为直接应用，我们证明即使限制在PSPACE可判定的片段且域大小为二的一阶逻辑中，一阶模型计数（FOMC）仍然是#EXP完全的。基于近期将2-DQBF可满足性约简为符号模型检验的成功，我们开发了一个专用的2-DQBF模型计数器。通过使用一组精心设计的实例，我们将其与将2-DQBF公式展开为命题公式并应用命题模型计数的基线方法进行了实验评估。当每个存在变量依赖的变量较少时，基线方法表现良好，但我们的实现在处理更大依赖集时展现出显著更好的可扩展性。