On the Complexity of k-DQBF
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.
Dependency quantified boolean formulas
existential variables
complexity
Theory of computation~Problems, reductions and completeness
10:1-10:15
Regular Paper
We acknowledge the generous financial support of Taiwan National Science and Technology Council under grant no. 109-2221-E-002-143-MY3.
We would like to thank Roland Jiang Jie-Hong for many useful and insightful discussions as well as the anonymous referees for their constructive feedback.
Long-Hin
Fung
Long-Hin Fung
Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan
Tony
Tan
Tony Tan
Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan
10.4230/LIPIcs.SAT.2023.10
SAT competition, 2020. URL: http://www.satcompetition.org/.
http://www.satcompetition.org/
V. Balabanov, H.-J. K. Chiang, and J.-H. R. Jiang. Henkin quantifiers and boolean formulae: A certification perspective of DQBF. Theor. Comput. Sci., 523:86-100, 2014.
V. Balabanov and J.-H. R. Jiang. Reducing satisfiability and reachability to DQBF. In Talk given at QBF, 2015.
A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability. IOS Press, 2009.
R. Bloem, R. Könighofer, and M. Seidl. SAT-based synthesis methods for safety specs. In VMCAI, 2014.
U. Bubeck. Model-based transformations for quantified boolean formulas. PhD thesis, University of Paderborn, 2010.
K. Chatterjee, T. Henzinger, J. Otop, and A. Pavlogiannis. Distributed synthesis for LTL fragments. In FMCAD, 2013.
F.-H. Chen, S.-C. Huang, Y.-C. Lu, and T. Tan. Reducing NEXP-complete problems to DQBF. In FMCAD, 2022.
D. Chistikov, C. Haase, Z. Hadizadeh, and A. Mansutti. Higher-order quantified boolean satisfiability. In MFCS, 2022.
S. Cook. The complexity of theorem proving procedures. In STOC, 1971.
S. Cook. Short propositional formulas represent nondeterministic computations. Inf. Process. Lett., 26(5):269-270, 1988.
A. Fröhlich, G. Kovásznai, and A. Biere. A DPLL algorithm for solving DQBF. In POS-12, Third Pragmatics of SAT workshop, 2012.
A. Fröhlich, G. Kovásznai, A. Biere, and H. Veith. iDQ: Instantiation-based DQBF solving. In POS-14, Fifth Pragmatics of SAT workshop, 2014.
H. Galperin and A. Wigderson. Succinct representations of graphs. Inf. Control., 56(3):183-198, 1983.
A. Ge-Ernst, C. Scholl, and R. Wimmer. Localizing quantifiers for DQBF. In FMCAD, 2019.
Aile Ge-Ernst, Christoph Scholl, Juraj Síc, and Ralf Wimmer. Solving dependency quantified boolean formulas using quantifier localization. Theor. Comput. Sci., 925:1-24, 2022.
K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, and B. Becker. Equivalence checking of partial designs using dependency quantified boolean formulae. In ICCD, 2013.
K. Gitina, R. Wimmer, S. Reimer, M. Sauer, C. Scholl, and B. Becker. Solving DQBF through quantifier elimination. In DATE, 2015.
J.-H. R. Jiang. Quantifier elimination via functional composition. In CAV, 2009.
R. Jiang. Second-order quantified boolean logic. In AAAI, 2023.
G. Kovásznai. What is the state-of-the-art in DQBF solving. In Join Conference on Mathematics and Computer Science, 2016.
A. Kuehlmann, V. Paruthi, F. Krohm, and M. Ganai. Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 21(12):1377-1394, 2002.
O. Kullmann and A. Shukla. Autarkies for DQCNF. In FMCAD, 2019.
L. Levin. Universal search problems (in russian. Problems of Information Transmission, 9(3):115-116, 1973.
C. Papadimitriou and M. Yannakakis. A note on succinct representations of graphs. Inf. Control., 71(3):181-185, 1986.
G. Peterson and J. Reif. Multiple-person alternation. In FOCS, 1979.
F.-X. Reichl and F. Slivovsky. Pedant: A certifying DQBF solver. In SAT, 2022.
F.-X. Reichl, F. Slivovsky, and S. Szeider. Certified DQBF solving by definition extraction. In SAT, 2021.
C. Scholl and B. Becker. Checking equivalence for partial implementations. In DAC, 2001.
C. Scholl, R. J.-H. Jiang, R. Wimmer, and A. Ge-Ernst. A PSPACE subclass of dependency quantified boolean formulas and its effective solving. In AAAI, 2019.
C. Scholl and R. Wimmer. Dependency quantified boolean formulas: An overview of solution methods and applications - extended abstract. In SAT, 2018.
J. Síc and J. Strejcek. DQBDD: an efficient bdd-based DQBF solver. In SAT, 2021.
S. Skyum and L. Valiant. A complexity theory based on boolean algebra. J. ACM, 32(2):484-502, 1985.
L. Stockmeyer and A. Meyer. Word problems requiring exponential time: Preliminary report. In STOC, 1973.
L. Tentrup and M. Rabe. Clausal abstraction for DQBF. In SAT, 2019.
K. Wimmer, R. Wimmer, C. Scholl, and B. Becker. Skolem functions for DQBF. In ATVA, 2016.
R. Wimmer, A. Karrenbauer, R. Becker, C. Scholl, and B. Becker. From DQBF to QBF by dependency elimination. In SAT, 2017.
R. Wimmer, S. Reimer, P. Marin, and B. Becker. HQSpre - an effective preprocessor for QBF and DQBF. In TACAS, 2017.
R. Wimmer, C. Scholl, and B. Becker. The (D)QBF preprocessor hqspre - underlying theory and its implementation. J. Satisf. Boolean Model. Comput., 11(1):3-52, 2019.
Long-Hin Fung and Tony Tan
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode