eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-08-09
10:1
10:15
10.4230/LIPIcs.SAT.2023.10
article
On the Complexity of k-DQBF
Fung, Long-Hin
1
Tan, Tony
1
Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan
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 k-DQBF - is essentially a k-CNF formula in succinct representation. However, beside this and the fact that the satisfiability problem is NEXP-complete, not much is known about DQBF.
In this paper we take a closer look at k-DQBF and show that a number of well known classical results on k-SAT can indeed be lifted to k-DQBF, which shows a strong resemblance between k-SAT and k-DQBF. More precisely, we show the following.
a) The satisfiability problem for 2- and 3-DQBF is PSPACE- and NEXP-complete, respectively.
b) There is a parsimonious polynomial time reduction from arbitrary DQBF to 3-DQBF.
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 2-DQBF with O(s(n)) universal variables.
e) Languages in the class NTIME[t(n)] can be reduced to the satisfiability of 3-DQBF with O(log t(n)) universal variables.
The first result parallels the well known classical results that 2-SAT and 3-SAT are NL- and NP-complete, respectively.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.SAT.2023.10/LIPIcs.SAT.2023.10.pdf
Dependency quantified boolean formulas
existential variables
complexity