Existential Second-Order Logic Over Graphs: Parameterized Complexity

TL;DR

This paper characterizes the parameterized complexity of problems definable by existential second-order logic over graphs, revealing new complexity boundaries based on quantifier sequences and parameter bounds.

Contribution

It provides a complete classification of the parameterized complexity for problems described by specific quantifier sequences in ESO logic over graphs.

Findings

Identifies the dividing line between tractable and intractable problems based on quantifier sequences.

Shows the complexity boundary depends on whether the parameter bounds the quantified set from above, below, or exactly.

Reveals a different complexity landscape compared to classical descriptive complexity results.

Abstract

By Fagin's Theorem, NP contains precisely those problems that can be described by formulas starting with an existential second-order quantifier, followed by only first-order quantifiers (ESO formulas). Subsequent research refined this result, culminating in powerful theorems that characterize for each possible sequence of first-order quantifiers how difficult the described problem can be. We transfer this line of inquiry to the parameterized setting, where the size of the set quantified by the second-order quantifier is the parameter. Many natural parameterized problems can be described in this way using simple sequences of first-order quantifiers: For the clique or vertex cover problems, two universal first-order quantifiers suffice ("for all pairs of vertices ... must hold"); for the dominating set problem, a universal followed by an existential quantifier suffice ("for all vertices, there is a vertex such that ..."); and so on. We present a complete characterization that states for each possible sequence of first-order quantifiers how high the parameterized complexity of the described problems can be. The uncovered dividing line between quantifier sequences that lead to tractable versus intractable problems is distinct from that known from the classical setting, and it depends on whether the parameter is a lower bound on, an upper bound on, or equal to the size of the quantified set.