Parameterized Complexity of Elimination Distance to First-Order Logic Properties

The elimination distance to some target graph property P is a general graph modification parameter introduced by Bulian and Dawar. We initiate the study of elimination distances to graph properties expressible in first-order logic. We delimit the problem's fixed-parameter tractability by identifying sufficient and necessary conditions on the structure of prefixes of first-order logic formulas. Our main result is the following meta-theorem: For every graph property P expressible by a first order-logic formula phi is an element of Sigma(3), that is, of the form phi = there exists x(1)there exists x(2) ... there exists x(r) for all y(1)for all y(2) ... for all y(s) there exists z(1)there exists z(2) ... there exists z(t) psi, where psi is a quantifier-free first-order formula, checking whether the elimination distance of a graph to P does not exceed k, is fixed-parameter tractable parameterized by k. Properties of graphs expressible by formulas from Sigma(3) include being of bounded degree, excluding a forbidden subgraph, or containing a bounded dominating set. We complement this theorem by showing that such a general statement does not hold for formulaswith even slightly more expressive prefix structure: There are formulas phi epsilon Pi(3), for which computing elimination distance is W[2]-hard.