Model Counting for Dependency Quantified Boolean Formulas

TL;DR

The paper identifies the counting analogue of Dependency Quantified Boolean Formulas (#DQBF) and proves a central result: $\#2$-DQBF is $\#EXP$-complete, underscoring the intrinsic hardness of model counting in dependency-labeled quantified Boolean frameworks. It introduces a BDD-based, two-phase model counter for $\#2$-DQBF that leverages symbolic reachability and component decomposition, circumventing explicit Skolem-function enumeration. The work further connects $\#DQBF$ to First-Order Model Counting (FOMC), showing $\#EXP$-hardness even in restricted FO fragments and tiny domain sizes, thereby explaining the challenges in scalable FO counting. Empirical evaluation shows that the proposed sharp2DQR method outperforms naive expansion-based baselines on instances with large dependency sets, indicating practical viability for structured DQBF problems and motivating future work toward $3$-DQBF and broader FO applications.

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'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.

Figures (5)

• Figure 1: The two figures on the left show the performance of the solvers on the PEC instances, the horizontal axis corresponds to the running time (s), and the vertical axis to the number of solved instances. The figure on the right shows the performance of the solvers on the 2-colorability instances; the horizontal axis corresponds to the number of bits of the graph in the instance, and the vertical axis to the running time (s).
• Figure 2: Pairwise comparison between sharp2DQR and Exp+ganak.
• Figure 3: Performance of sharp2DQR and Exp+ganak on the counting the numbers of 2-colorings over $G_{n, k}$. The horizontal axis represents the number of bits in the graph, i.e. $n$.
• Figure 4: Time used on expansion and counting for Exp+ganak on 2-colorability instances.
• Figure 5: Performance of sharp2DQR and Exp+ganak on the counting the numbers of independent sets over $G_{n, k}$. The horizontal axis represents the number of bits in the graph, i.e. $n$.

Theorems & Definitions (17)

• Theorem 1
• Lemma 2
• Lemma 3
• proof
• Lemma 4
• proof
• Lemma 5
• Theorem 6
• Corollary 7
• Theorem 8