LIPIcs.CSL.2021.27.pdf
- Filesize: 0.62 MB
- 22 pages
Document
On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic
Authors
Miika Hannula 
,
Juha Kontinen ,
Jonni Virtema
-
Part of:
Volume:
29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2021-01-13
File
Document Identifiers
Author Details
Acknowledgements
We wish to thank the anonymous referees for their very careful and thorough reviews.
Cite AsGet 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
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)
0PDF Downloads
References
- Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. URL: http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521424264.
- 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.
- 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.
-
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.
- 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.
- 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.
-
Juris Hartmanis, Neil Immerman, and Vivian Sewelson. Sparse sets in NP-P: EXPTIME versus NEXPTIME. Information and Control, 65(2/3):158-181, 1985.
- 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.
-
Martin Lück. Complete problems of propositional logic for the exponential hierarchy. CoRR, abs/1602.03050, 2016.
- 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.
-
Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.