Document Open Access Logo

On the Complexity of k-DQBF

Authors Long-Hin Fung, Tony Tan

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.10.pdf
  • Filesize: 0.7 MB
  • 15 pages

Document Identifiers

Author Details

Long-Hin Fung
  • Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan
Tony Tan
  • Department of Computer Science and Information Engineering, National Taiwan University, Taipei, Taiwan

Funding

We acknowledge the generous financial support of Taiwan National Science and Technology Council under grant no. 109-2221-E-002-143-MY3.

Acknowledgements

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.

Cite AsGet BibTex

Long-Hin Fung and Tony Tan. On the Complexity of k-DQBF. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 10:1-10:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.10

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
Keywords
  • Dependency quantified boolean formulas
  • existential variables
  • complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. SAT competition, 2020. URL: http://www.satcompetition.org/.
  2. 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. Google Scholar
  3. V. Balabanov and J.-H. R. Jiang. Reducing satisfiability and reachability to DQBF. In Talk given at QBF, 2015. Google Scholar
  4. A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability. IOS Press, 2009. Google Scholar
  5. R. Bloem, R. Könighofer, and M. Seidl. SAT-based synthesis methods for safety specs. In VMCAI, 2014. Google Scholar
  6. U. Bubeck. Model-based transformations for quantified boolean formulas. PhD thesis, University of Paderborn, 2010. Google Scholar
  7. K. Chatterjee, T. Henzinger, J. Otop, and A. Pavlogiannis. Distributed synthesis for LTL fragments. In FMCAD, 2013. Google Scholar
  8. F.-H. Chen, S.-C. Huang, Y.-C. Lu, and T. Tan. Reducing NEXP-complete problems to DQBF. In FMCAD, 2022. Google Scholar
  9. D. Chistikov, C. Haase, Z. Hadizadeh, and A. Mansutti. Higher-order quantified boolean satisfiability. In MFCS, 2022. Google Scholar
  10. S. Cook. The complexity of theorem proving procedures. In STOC, 1971. Google Scholar
  11. S. Cook. Short propositional formulas represent nondeterministic computations. Inf. Process. Lett., 26(5):269-270, 1988. Google Scholar
  12. A. Fröhlich, G. Kovásznai, and A. Biere. A DPLL algorithm for solving DQBF. In POS-12, Third Pragmatics of SAT workshop, 2012. Google Scholar
  13. 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. Google Scholar
  14. H. Galperin and A. Wigderson. Succinct representations of graphs. Inf. Control., 56(3):183-198, 1983. Google Scholar
  15. A. Ge-Ernst, C. Scholl, and R. Wimmer. Localizing quantifiers for DQBF. In FMCAD, 2019. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. K. Gitina, R. Wimmer, S. Reimer, M. Sauer, C. Scholl, and B. Becker. Solving DQBF through quantifier elimination. In DATE, 2015. Google Scholar
  19. J.-H. R. Jiang. Quantifier elimination via functional composition. In CAV, 2009. Google Scholar
  20. R. Jiang. Second-order quantified boolean logic. In AAAI, 2023. Google Scholar
  21. G. Kovásznai. What is the state-of-the-art in DQBF solving. In Join Conference on Mathematics and Computer Science, 2016. Google Scholar
  22. 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. Google Scholar
  23. O. Kullmann and A. Shukla. Autarkies for DQCNF. In FMCAD, 2019. Google Scholar
  24. L. Levin. Universal search problems (in russian. Problems of Information Transmission, 9(3):115-116, 1973. Google Scholar
  25. C. Papadimitriou and M. Yannakakis. A note on succinct representations of graphs. Inf. Control., 71(3):181-185, 1986. Google Scholar
  26. G. Peterson and J. Reif. Multiple-person alternation. In FOCS, 1979. Google Scholar
  27. F.-X. Reichl and F. Slivovsky. Pedant: A certifying DQBF solver. In SAT, 2022. Google Scholar
  28. F.-X. Reichl, F. Slivovsky, and S. Szeider. Certified DQBF solving by definition extraction. In SAT, 2021. Google Scholar
  29. C. Scholl and B. Becker. Checking equivalence for partial implementations. In DAC, 2001. Google Scholar
  30. 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. Google Scholar
  31. C. Scholl and R. Wimmer. Dependency quantified boolean formulas: An overview of solution methods and applications - extended abstract. In SAT, 2018. Google Scholar
  32. J. Síc and J. Strejcek. DQBDD: an efficient bdd-based DQBF solver. In SAT, 2021. Google Scholar
  33. S. Skyum and L. Valiant. A complexity theory based on boolean algebra. J. ACM, 32(2):484-502, 1985. Google Scholar
  34. L. Stockmeyer and A. Meyer. Word problems requiring exponential time: Preliminary report. In STOC, 1973. Google Scholar
  35. L. Tentrup and M. Rabe. Clausal abstraction for DQBF. In SAT, 2019. Google Scholar
  36. K. Wimmer, R. Wimmer, C. Scholl, and B. Becker. Skolem functions for DQBF. In ATVA, 2016. Google Scholar
  37. R. Wimmer, A. Karrenbauer, R. Becker, C. Scholl, and B. Becker. From DQBF to QBF by dependency elimination. In SAT, 2017. Google Scholar
  38. R. Wimmer, S. Reimer, P. Marin, and B. Becker. HQSpre - an effective preprocessor for QBF and DQBF. In TACAS, 2017. Google Scholar
  39. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact