Abstract
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 existential variable, one can specify the set of universal variables it depends on. It has been observed that a DQBF with k existential variables  henceforth denoted by kDQBF  is essentially a kCNF formula in succinct representation. However, beside this and the fact that the satisfiability problem is NEXPcomplete, not much is known about DQBF.
In this paper we take a closer look at kDQBF and show that a number of well known classical results on kSAT can indeed be lifted to kDQBF, which shows a strong resemblance between kSAT and kDQBF. More precisely, we show the following.
a) The satisfiability problem for 2 and 3DQBF is PSPACE and NEXPcomplete, respectively.
b) There is a parsimonious polynomial time reduction from arbitrary DQBF to 3DQBF.
c) Many polynomial time projections from SAT to languages in NP can be lifted to polynomial time reductions from the satisfiability of DQBF to languages in NEXP.
d) Languages in the class NSPACE[s(n)] can be reduced to the satisfiability of 2DQBF with O(s(n)) universal variables.
e) Languages in the class NTIME[t(n)] can be reduced to the satisfiability of 3DQBF with O(log t(n)) universal variables.
The first result parallels the well known classical results that 2SAT and 3SAT are NL and NPcomplete, respectively.
BibTeX  Entry
@InProceedings{fung_et_al:LIPIcs.SAT.2023.10,
author = {Fung, LongHin and Tan, Tony},
title = {{On the Complexity of kDQBF}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {10:110:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772860},
ISSN = {18688969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18472},
URN = {urn:nbn:de:0030drops184729},
doi = {10.4230/LIPIcs.SAT.2023.10},
annote = {Keywords: Dependency quantified boolean formulas, existential variables, complexity}
}
Keywords: 

Dependency quantified boolean formulas, existential variables, complexity 
Collection: 

26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) 
Issue Date: 

2023 
Date of publication: 

09.08.2023 