Document Open Access Logo

On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic

Authors Miika Hannula , Juha Kontinen , Martin Lück, Jonni Virtema

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.27.pdf
  • Filesize: 0.62 MB
  • 22 pages

Document Identifiers

Author Details

Miika Hannula
  • Department of Mathematics and Statistics, University of Helsinki, Finland
Juha Kontinen
  • Department of Mathematics and Statistics, University of Helsinki, Finland
Martin Lück
  • Institut für Theoretische Informatik, Leibniz Universität Hannover, Germany
Jonni Virtema
  • Faculty of Humanities and Human Sciences, Hokkaido University, Sapporo, Japan

Funding

The first and second authors were supported by grant 308712 of the Academy of Finland. The fourth author was an international research fellow of Japan Society for the Promotion of Science (Postdoctoral Fellowships for Research in Japan (Standard)).

Acknowledgements

We wish to thank the anonymous referees for their very careful and thorough reviews.

Cite As Get BibTex

Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema. On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CSL.2021.27

Abstract

Second-order Boolean logic is a generalization of QBF, whose constant alternation fragments are known to be complete for the levels of the exponential time hierarchy. We consider two types of restriction of this logic: 1) restrictions to term constructions, 2) restrictions to the form of the Boolean matrix. Of the first sort, we consider two kinds of restrictions: firstly, disallowing nested use of proper function variables, and secondly stipulating that each function variable must appear with a fixed sequence of arguments. Of the second sort, we consider Horn, Krom, and core fragments of the Boolean matrix. We classify the complexity of logics obtained by combining these two types of restrictions. We show that, in most cases, logics with k alternating blocks of function quantifiers are complete for the kth or (k-1)th level of the exponential time hierarchy. Furthermore, we establish NL-completeness for the Krom and core fragments, when k = 1 and both restrictions of the first sort are in effect.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • quantified Boolean formulae
  • computational complexity
  • second-order logic
  • Horn and Krom fragment

Metrics

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

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264.
  2. Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett., 8(3):121-123, 1979. URL: https://doi.org/10.1016/0020-0190(79)90002-4.
  3. Herbert Baier and Klaus W. Wagner. The Analytic Polynomial-Time Hierarchy. Mathematical Logic Quarterly, 44(4):529-544, 1998. URL: http://onlinelibrary.wiley.com/doi/10.1002/malq.19980440412/abstract.
  4. Uwe Bubeck and Hans Kleine Büning. Dependency quantified horn formulas: Models and complexity. In SAT, volume 4121 of Lecture Notes in Computer Science, pages 198-211. Springer, 2006. Google Scholar
  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. Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema. On quantified propositional logics and the exponential time hierarchy. In Domenico Cantone and Giorgio Delzanno, editors, Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016, volume 226 of EPTCS, pages 198-212, 2016. URL: https://doi.org/10.4204/EPTCS.226.14.
  7. Juris Hartmanis, Neil Immerman, and Vivian Sewelson. Sparse sets in NP-P: EXPTIME versus NEXPTIME. Information and Control, 65(2/3):158-181, 1985. Google Scholar
  8. Markus Lohrey. Model-checking hierarchical structures. J. Comput. Syst. Sci., 78(2):461-490, 2012. URL: https://doi.org/10.1016/j.jcss.2011.05.006.
  9. Martin Lück. Complete problems of propositional logic for the exponential hierarchy. CoRR, abs/1602.03050, 2016. Google Scholar
  10. Pekka Orponen. Complexity classes of alternating machines with oracles. In Josep Díaz, editor, Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain, July 18-22, 1983, Proceedings, volume 154 of Lecture Notes in Computer Science, pages 573-584. Springer, 1983. URL: https://doi.org/10.1007/BFb0036938.
  11. Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  12. Gary L. Peterson and John H. Reif. Multiple-person alternation. In 20th Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 29-31 October 1979, pages 348-363. IEEE Computer Society, 1979. URL: https://doi.org/10.1109/SFCS.1979.25.
  13. Gary L. Peterson, John H. Reif, and Salman Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. Computers & Mathematics with Applications, 41(7):957-992, 2001. URL: https://doi.org/10.1016/S0898-1221(00)00333-3.
  14. Christoph Scholl and Ralf Wimmer. Dependency quantified boolean formulas: An overview of solution methods and applications - extended abstract. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 3-16. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_1.
  15. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified boolean formulas. In 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2019, Portland, OR, USA, November 4-6, 2019, pages 78-84. IEEE, 2019. URL: https://doi.org/10.1109/ICTAI.2019.00020.
  16. Larry J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3(1):1-22, 1976. URL: https://doi.org/10.1016/0304-3975(76)90061-X.
  17. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 1-9. ACM, 1973. URL: https://doi.org/10.1145/800125.804029.
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 About DROPS Imprint Privacy Contact