Recently Dependency Quantified Boolean Formula (DQBF) has attracted a lot of attention in the SAT community. Intuitively, a DQBF is a natural extension of quantified boolean formula where for each existentially quantified variable, one can specify its set of dependent variables. However, beside the fact that the satisfiability problem is NEXP-complete, not much is known about DQBF.

In this paper we show that surprisingly there is a strong resemblance between DQBF and CNF boolean formulas. More precisely, we show that a DQBF is just a succinctly represented CNF boolean formula in which the information about each clause is encoded inside the matrix of the DQBF and that the number of existentially quantified variables in a DQBF corresponds precisely to the width of the clauses in the CNF formula. Thus, solving DQBF instances is essentially solving SAT instances in CNF. We then present a thorough study on DQBF and show that indeed many classical results on SAT can be lifted up to DQBF, only with exponential blow-up in complexity.