The elimination distance to some target graph property ${mathcal{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 ${mathcal{P}}$ expressible by a first order-logic formula Φ ∈ Σ3, that is, of the formegin{equation*}arphi = exists {x_1}exists {x_2} cdots exists {x_r}orall {y_1}orall {y_2} cdots orall {y_s}quad exists {z_1}exists {z_2} cdots exists {z_t},psi ,end{equation*}where ψ is a quantifier-free first-order formula, checking whether the elimination distance of a graph to ${mathcal{P}}$ does not exceed k, is fixed-parameter tractable parameterized by k. Properties of graphs expressible by formulas from Σ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 formulas with even slightly more expressive prefix structure: There are formulas Φ ∈ Π3, for which computing elimination distance is W[2]-hard.
展开▼
