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

TL;DR

This paper analyzes the computational complexity of various restricted fragments of second-order Boolean logic, including Horn and Krom forms, revealing their placement within the exponential time hierarchy and identifying NL-complete cases.

Contribution

It classifies the complexity of combined restrictions on second-order Boolean logic, extending understanding of their computational boundaries and identifying NL-complete fragments.

Findings

Most k-quantifier blocks are complete for the kth or (k-1)th exponential hierarchy level.

NL-completeness is established for Krom and core fragments with specific restrictions.

Complexity classifications depend on the type and combination of restrictions applied.

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.