Document

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

## File

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

## Acknowledgements

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

## Cite As

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

## 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.
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.
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.
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.