Dependency Quantified Boolean Formulas and Succinct Sat

The satisfiability of Dependency Quantified Boolean Formulas (DQBFs) recently has attracted a lot of attention in SAT community.
Intuitively DQBF is the extension of QBF where for each existentially quantified variable, one can specify its set of dependent variables.

In this talk we will show that a DQBF is simply a CNF formula in an exponentially more succinct representation.
For a positive integer k, let k-DQBF be a DQBF with k existentially quantified variables.
We show the following.
1) k-DQBF is a succinct representation of a k-CNF formula.
2) The satisfiability of 2-DQBFs and 3-DQBFs is PSPACE-complete and NEXP-complete, resp.
3) A parsimonious polynomial time reduction from DQBFs to 3-DQBFs.
4) Natural explicit reductions from well known NEXP-complete problems to the satisfiability of DQBF.

Results (2)--(4) parallel the following well known classical results for SAT.
*) The satisfiability of 2-CNF and 3-CNF formulas is NLOG-complete and NP-complete, resp.
*) A parsimonious polynomial time reduction from arbitrary boolean formulas to 3-CNF formulas.
*) Natural reductions (in the form of Cook-Levin reductions) from NP-complete problems to SA