Document Open Access Logo

Higher-Order Quantified Boolean Satisfiability

Authors Dmitry Chistikov , Christoph Haase , Zahra Hadizadeh, Alessio Mansutti

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.33.pdf
  • Filesize: 0.96 MB
  • 15 pages

Document Identifiers

Author Details

Dmitry Chistikov
  • Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, Coventry, UK
Christoph Haase
  • Department of Computer Science, University of Oxford, Oxford, UK
Zahra Hadizadeh
  • Sharif University of Technology, Tehran, Iran
Alessio Mansutti
  • Department of Computer Science, University of Oxford, Oxford, UK

Funding

This work is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT).

Acknowledgements

We would like to thank the anonymous reviewers for their thoughtful comments, and in particular for pointing us to [Harry G. Mairson, 1992], which uncovered profound connections between our work and the basic language of set theory and typed λ-calculi studied by Statman [Richard Statman, 1979].

Cite AsGet BibTex

Dmitry Chistikov, Christoph Haase, Zahra Hadizadeh, and Alessio Mansutti. Higher-Order Quantified Boolean Satisfiability. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.33

Abstract

The Boolean satisfiability problem plays a central role in computational complexity and is often used as a starting point for showing NP lower bounds. Generalisations such as Succinct SAT, where a Boolean formula is succinctly represented as a Boolean circuit, have been studied in the literature in order to lift the Boolean satisfiability problem to higher complexity classes such as NEXP. While, in theory, iterating this approach yields complete problems for k-NEXP for all k > 0, using such iterations of Succinct SAT is at best tedious when it comes to proving lower bounds. The main contribution of this paper is to show that the Boolean satisfiability problem has another canonical generalisation in terms of higher-order Boolean functions that is arguably more suitable for showing lower bounds beyond NP. We introduce a family of problems HOSAT(k,d), k ≥ 0, d ≥ 1, in which variables are interpreted as Boolean functions of order at most k and there are d quantifier alternations between functions of order exactly k. We show that the unbounded HOSAT problem is TOWER-complete, and that HOSAT(k,d) is complete for the weak k-EXP hierarchy with d alternations for fixed k,d ≥ 1 and d odd. We illustrate the usefulness of HOSAT by characterising the complexity of weak Presburger arithmetic, the first-order theory of the integers with addition and equality but without order. It has been a long-standing open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negation-free fragment and the Horn fragment of weak Presburger arithmetic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Boolean satisfiability problem
  • higher-order Boolean functions
  • weak k-EXP hierarchies
  • non-elementary complexity
  • Presburger arithmetic

Metrics

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

References

  1. László Babai, Lance Fortnow, and Carsten Lund. Non-deterministic exponential time has two-prover interactive protocols. Comput. Complex., 1:3-40, 1991. URL: https://doi.org/10.1007/BF01200056.
  2. José L. Balcázar, Antoni Lozano, and Jacobo Torán. The Complexity of Algorithmic Problems on Succinct Instances, pages 351-377. Springer, 1992. URL: https://doi.org/10.1007/978-1-4615-3422-8_30.
  3. Leonard Berman. The complexity of logical theories. Theor. Comput. Sci., 11(1):71-77, 1980. URL: https://doi.org/10.1016/0304-3975(80)90037-7.
  4. Laura Bozzelli, Alberto Molinari, Angelo Montanari, and Adriano Peron. On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions. In International Symposium on Games, Automata, Logics, and Formal Verification, GandALF, volume 277 of EPTCS, pages 31-45, 2017. URL: https://doi.org/10.4204/EPTCS.256.3.
  5. Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: https://doi.org/10.1145/322234.322243.
  6. Dmitry Chistikov and Christoph Haase. On the Power of Ordering in Linear Arithmetic Theories. In International Colloquium on Automata, Languages, and Programming, ICALP, volume 168 of LIPIcs, pages 119:1-119:15, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.119.
  7. Christian Choffrut and Achille Frigeri. Deciding whether the ordering is necessary in a Presburger formula. Discret. Math. Theor. C., 12(1):21-38, 2010. URL: http://dmtcs.episciences.org/510.
  8. Stephen A. Cook. The complexity of theorem-proving procedures. In Symposium on Theory of Computing, STOC, pages 151-158, 1971. URL: https://doi.org/10.1145/800157.805047.
  9. Adrian W. Dudek. An explicit result for primes between cubes. Functiones et Approximatio Commentarii Mathematici, 55(2):177-197, 2016. Google Scholar
  10. Raul Fervari and Alessio Mansutti. Modal logics and local quantifiers: A zoo in the elementary hierarchy. In Foundations of Software Science and Computation Structures, FoSSaCS, volume 13242 of Lecture Notes in Computer Science, pages 305-324, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_16.
  11. Michael J. Fischer and Michael O. Rabin. Super-exponential complexity of Presburger arithmetic. In Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 122-135, 1998. URL: https://doi.org/10.1007/978-3-7091-9459-1_5.
  12. Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979. Google Scholar
  13. Erich Grädel. Dominoes and the complexity of subclasses of logical theories. Ann. Pure Appl. Log., 43(1):1-30, 1989. URL: https://doi.org/10.1016/0168-0072(89)90023-7.
  14. Christoph Haase and Alessio Mansutti. On deciding linear arithmetic constraints over p-adic integers for all primes. In Mathematical Foundations of Computer Science, MFCS, volume 202 of LIPIcs, pages 55:1-55:20, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.55.
  15. Lane A. Hemachandra. The strong exponential hierarchy collapses. J. Comput. Syst. Sci., 39(3):299-322, 1989. URL: https://doi.org/10.1016/0022-0000(89)90025-1.
  16. Albert E. Ingham. On The Estimation Of N(σ, T). Q. J. Math., os-11(1):201-202, January 1940. URL: https://doi.org/10.1093/qmath/os-11.1.201.
  17. Richard M. Karp. Reducibility among combinatorial problems. In Complexity of Computer Computations, pages 85-103, 1972. URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  18. Dexter Kozen. Theory of Computation. Texts in Computer Science. Springer, 2006. Google Scholar
  19. Markus Lohrey. Model-checking hierarchical structures. J. Comput. Syst. Sci., 78(2):461-490, 2012. Games in Verification. URL: https://doi.org/10.1016/j.jcss.2011.05.006.
  20. Antoni Lozano and José L. Balcázar. The complexity of graph problems fore succinctly represented graphs. In Graph-Theoretic Concepts in Computer Science, WG, volume 411 of Lecture Notes in Computer Science, pages 277-286. Springer, 1990. URL: https://doi.org/10.1007/3-540-52292-1.
  21. Martin Lück. Canonical models and the complexity of modal team logic. In Computer Science Logic, CSL, volume 119 of LIPIcs, pages 30:1-30:23, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.30.
  22. Harry G. Mairson. A simple proof of a theorem of Statman. Theor. Comput. Sci., 103(2):387-394, 1992. URL: https://doi.org/10.1016/0304-3975(92)90020-G.
  23. Alessio Mansutti. Notes on kAExp(pol) problems for deterministic machines. CoRR, abs/2110.05630, 2021. URL: http://arxiv.org/abs/2110.05630.
  24. Albert R. Meyer. The inherent computational complexity of theories of ordered sets. In Proceedings of the International Congress of Mathematicians, volume 2, pages 477-482, 1974. Google Scholar
  25. Alberto Molinari. Model checking: the interval way. PhD thesis, Università degli Studi di Udine, 2019. http://arxiv.org/abs/1901.03880.
  26. Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  27. Christos H. Papadimitriou and Mihalis Yannakakis. A note on succinct representations of graphs. Inf. Control., 71(3):181-185, 1986. URL: https://doi.org/10.1016/S0019-9958(86)80009-2.
  28. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, 1929. In Comptes Rendus du I Congrès des Mathématiciens des Pays Slaves, pages 92-101. Google Scholar
  29. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  30. Richard Statman. The typed λ-calculus is not elementary recursive. Theor. Comput. Sci., 9(1):73-81, 1979. URL: https://doi.org/10.1016/0304-3975(79)90007-0.
  31. user4625. Complexity class NEXP^NP. Theoretical Computer Science Stack Exchange, 2011. URL: https://cstheory.stackexchange.com/q/6001.
  32. Helmut Veith. Succinct representation, leaf languages, and projection reductions. Inf. Comput., 142(2):207-236, 1998. URL: https://doi.org/10.1006/inco.1997.2696.
  33. Celia Wrathall. Complete sets and the polynomial-time hierarchy. Theor. Comput. Sci., 3(1):23-33, 1976. URL: https://doi.org/10.1016/0304-3975(76)90062-1.
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