Tan, Tony 
ORCID: 0009-0005-8341-2004 and Fung, Long-Hin
(2023)
On the complexity of k-DQBF.
In: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023).
|
PDF
LIPIcs.SAT.2023.10.pdf - Other Download (741kB) | Preview |
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 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.
| Item Type: | Conference or Workshop Item (Unspecified) |
|---|---|
| Additional Information: | In this paper we show that DQBF is just SAT in succinct representation. With this result we hope that DQBF can be accepted as the bona fide problem for the class NEXP, just like SAT and QBF are the bona fide problems for the class NP and PSPACE. |
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 15 Jan 2024 14:44 |
| Last Modified: | 15 Jan 2024 14:44 |
| DOI: | 10.4230/LIPIcs.SAT.2023.10 |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3177852 |
Dimensions
Dimensions
